% For HTML
detect110: THEORY
BEGIN
IMPORTING components, quantifier_rules
t: VAR time
e, a, l1, l2, l3, q4, l5, l6, q7: VAR signal[bool]
detect110_spec(e, a): bool =
(FORALL t: a(t+2) = (NOT e(t+2) & e(t+1) & e(t)))
detect110_imp(e, a): bool =
(EXISTS (l1, l2, l3, q4, l5, l6, q7):
(FORALL t: NOTp(e(t), l1(t)) &
NOTp(l5(t), l6(t)) &
ANDp(e(t), l5(t), l2(t)) &
ANDp(e(t), l6(t), l3(t)) &
DELAY(l2, q4) &
DELAY(l3, q7) &
ANDp(l1(t), q4(t), a(t)) &
ORp(q4(t), q7(t), l5(t))))
detect110_correct: LEMMA
detect110_imp(e, a) IMPLIES detect110_spec(e, a)
END detect110