proposition: Theorem appTraceCorrect : forall (S1 S2 S3 : State) (T1 T2 : Trace), evalTrace S1 T1 S2 -> evalTrace S2 T2 S3 -> evalTrace S1 (appTrace T1 T2) S3.
proof: Proof. intros S1 S2 S3 T1 T2 H' H'0; inversion_clear H'; inversion_clear H'0; simpl in |- *; auto with stalmarck. apply evalTraceEq with (S1 := S2) (S2 := S3); auto with stalmarck. apply evalTraceEq with (S1 := S2) (S2 := S3); auto with stalmarck. apply tripletTraceEval with (S2 := S4); auto with stalmarck. apply evalTraceEq with (S1 := S2) (S2 := S3); auto with stalmarck. apply seqTraceEval with (S2 := S4); auto with stalmarck. apply evalTraceEq with (S1 := S2) (S2 := S3); auto with stalmarck. apply dilemmaTraceEval with (S2 := S4) (S3 := S5); auto with stalmarck. apply evalTraceEq with (S1 := S1) (S2 := S4); auto with stalmarck. apply tripletTraceEval with (S2 := S4); auto with stalmarck. apply eqStateTrans with S2; auto with stalmarck. apply seqTraceEval with (S2 := S4); auto with stalmarck. apply tripletTraceEval with (S2 := S4); auto with stalmarck. apply evalTraceEq with (S1 := S2) (S2 := S5); auto with stalmarck. apply tripletTraceEval with (S2 := S5); auto with stalmarck. apply seqTraceEval with (S2 := S4); auto with stalmarck. apply tripletTraceEval with (S2 := S4); auto with stalmarck. apply seqTraceEval with (S2 := S5); auto with stalmarck. apply evalTraceEq with (S1 := S2) (S2 := S5); auto with stalmarck. apply seqTraceEval with (S2 := S2); auto with stalmarck. apply tripletTraceEval with (S2 := S4); auto with stalmarck. apply dilemmaTraceEval with (S2 := S5) (S3 := S6); auto with stalmarck. apply seqTraceEval with (S2 := S4); auto with stalmarck. apply evalTraceEq with (S1 := S4) (S2 := S2); auto with stalmarck. apply seqTraceEval with (S2 := S2); auto with stalmarck. apply seqTraceEval with (S2 := S4); auto with stalmarck. apply tripletTraceEval with (S2 := S5); auto with stalmarck. apply seqTraceEval with (S2 := S2); auto with stalmarck. apply seqTraceEval with (S2 := S4); auto with stalmarck. apply seqTraceEval with (S2 := S5); auto with stalmarck. apply seqTraceEval with (S2 := S2); auto with stalmarck. apply seqTraceEval with (S2 := S4); auto with stalmarck. apply dilemmaTraceEval with (S2 := S5) (S3 := S6); auto with stalmarck. apply dilemmaTraceEval with (S2 := S4) (S3 := S5); auto with stalmarck. apply eqStateTrans with S2; auto with stalmarck. apply seqTraceEval with (S2 := S2); auto with stalmarck. apply dilemmaTraceEval with (S2 := S4) (S3 := S5); auto with stalmarck. apply tripletTraceEval with (S2 := S6); auto with stalmarck. apply seqTraceEval with (S2 := S2); auto with stalmarck. apply dilemmaTraceEval with (S2 := S4) (S3 := S5); auto with stalmarck. apply seqTraceEval with (S2 := S6); auto with stalmarck. apply seqTraceEval with (S2 := S2); auto with stalmarck. apply dilemmaTraceEval with (S2 := S4) (S3 := S5); auto with stalmarck. apply dilemmaTraceEval with (S2 := S6) (S3 := S7); auto with stalmarck. Qed.