proposition: Lemma equalBeforeTEval : forall (f g : rNat -> bool) (t : triplet), equalBefore (rnext (maxVarTriplet t)) f g -> tEval f t = tEval g t.
proof: Proof. intros f g t; case t; simpl in |- *; auto with stalmarck. intros r r0 r1 r2 H'; red in H'. cut (rZEval f r0 = rZEval g r0); [ intros Eq1; rewrite Eq1 | idtac ]; auto with stalmarck. cut (rZEval f r1 = rZEval g r1); [ intros Eq2; rewrite Eq2 | idtac ]; auto with stalmarck. cut (rZEval f r2 = rZEval g r2); [ intros Eq3; rewrite Eq3 | idtac ]; auto with stalmarck. generalize H'; case r2; simpl in |- *; auto with stalmarck; intros r3 H'0; rewrite H'0; simpl in |- *; auto with stalmarck. generalize H'; case r1; simpl in |- *; auto with stalmarck; intros r3 H'0; rewrite H'0; simpl in |- *; auto with stalmarck. apply rltTransRnext1 with (m := rmax (valRz r0) r3); auto with stalmarck. apply rltTransRnext1 with (m := rmax (valRz r0) r3); auto with stalmarck. generalize H'; case r0; simpl in |- *; auto with stalmarck; intros r3 H'0; rewrite H'0; simpl in |- *; auto with stalmarck. apply rltTransRnext1 with (m := rmax r3 (valRz r1)); auto with stalmarck. apply rltTransRnext1 with (m := rmax r3 (valRz r1)); auto with stalmarck. Qed.
imports: Coq(Relation_Definitions)