proposition: Theorem doTripletsRealizeStateEval : forall (f : rNat -> bool) (S1 S2 : State) (L : list triplet), realizeState f S1 -> doTripletsP S1 L S2 -> realizeTriplets f L -> f zero = true -> realizeState f S2.
proof: Proof. intros f S1 S2 L H' H'0; generalize H'; elim H'0; auto with stalmarck. intros S3 S4 L0 H'1 H'2 H'3 H'4. apply realizeStateIncl with (S1 := S3); auto with stalmarck; inversion H'1; auto with stalmarck. intros S3 S4 S5 L0 t H'1 H'2 H'3 H'4 H'5 H'6 H'7. apply H'4; auto with stalmarck. apply realizeStateEval with (2 := H'2); auto with stalmarck. Qed.
imports: Stalmarck(PolyListAux)