proposition: Theorem dTCorrect : forall (t1 t2 : Trace) (a b : rZ) (S1 S2 S3 S4 : State), evalTrace (addEq (a, b) S1) t1 S2 -> evalTrace (addEq (a, rZComp b) S1) t2 S3 -> eqState (interState S2 S3) S4 -> evalTrace S1 (dT a b t1 t2) S4.
proof: Proof. intros t1; case t1; simpl in |- *; auto with stalmarck. intros t1'; case t1'; simpl in |- *; auto with stalmarck. intros a b S1 S2 S3 S4 H' H'0 H'1. apply emptyTraceEval; auto with stalmarck. apply eqStateTrans with (2 := H'1). inversion_clear H'. inversion_clear H'0. apply eqStateTrans with (interState (addEq (a, b) S1) (addEq (a, rZComp b) S1)). apply CompInterR; auto with stalmarck. apply interStateEq; auto with stalmarck. intros t a b S1 S2 S3 S4 H' H'0 H'1. apply dilemmaTraceEval with (S2 := S2) (S3 := S3); auto with stalmarck. intros t t0 a b S1 S2 S3 S4 H' H'0 H'1. apply dilemmaTraceEval with (S2 := S2) (S3 := S3); auto with stalmarck. intros r r0 t t0 a b S1 S2 S3 S4 H' H'0 H'1. apply dilemmaTraceEval with (S2 := S2) (S3 := S3); auto with stalmarck. intros t t2 a b S1 S2 S3 S4 H' H'0 H'1. apply dilemmaTraceEval with (S2 := S2) (S3 := S3); auto with stalmarck. intros t t0 t2 a b S1 S2 S3 S4 H' H'0 H'1. apply dilemmaTraceEval with (S2 := S2) (S3 := S3); auto with stalmarck. intros r r0 t t0 t2 a b S1 S2 S3 S4 H' H'0 H'1. apply dilemmaTraceEval with (S2 := S2) (S3 := S3); auto with stalmarck. Qed.