proposition: Theorem equalBeforeMakeTripletsFun : forall (e : rExpr) (l l' : list triplet) (n n' : rNat) (s' : rZ), makeTripletsFun l n e = tRC l' s' n' -> forall f g : rNat -> bool, rlt (maxVar e) n -> rlt (maxVarTriplets l) n -> equalBefore n f g -> realizeTriplets f l' -> realizeTriplets g l' -> equalBefore n' f g.
proof: Proof. RecExpr; intros f g H'4 H'5 H'6 H'7 H'8. apply H' with (l := l) (l' := l') (n := n) (s' := r0); auto with stalmarck. rewrite <- H0; rewrite <- H2; auto with stalmarck. cut (rlt n (rnext r3)); [ intros Rle0 | eapply makeTripletsFunIncr; eauto with stalmarck ]. cut (equalBefore r5 f g); [ intros eB0 | idtac ]. apply equalBeforeNext; auto with stalmarck. cut (tEval f (Triplet r (rZPlus r5) r2 r4) = true); [ simpl in |- * | idtac ]. cut (tEval g (Triplet r (rZPlus r5) r2 r4) = true); [ simpl in |- * | idtac ]. rewrite (equalBeforerZEval f g r5 r4); auto with stalmarck. rewrite (equalBeforerZEval f g r5 r2); auto with stalmarck. case (f r5); auto with stalmarck; case (g r5); auto with stalmarck; case (rBoolOpFun r (rZEval g r2) (rZEval g r4)); auto with stalmarck. red in |- *; apply rltTransRnext2 with (m := r3); auto with stalmarck. change (rVlt r2 r3) in |- *. eapply makeTripletsFunMax; eauto with stalmarck. apply rmaxRltLeft with (p := maxVar r1); auto with stalmarck. eapply makeTripletsFunIncr; eauto with stalmarck. eapply makeTripletsFunMax; eauto with stalmarck. apply rmaxRltRight with (m := maxVar r0); auto with stalmarck. apply rltTransRnext2 with (m := n); auto with stalmarck. apply H'8; auto with datatypes stalmarck. apply H'7; auto with datatypes stalmarck. rewrite H0 in H'7. rewrite H0 in H'8. apply A with (1 := C); auto with stalmarck. apply rmaxRltRight with (m := maxVar r0); auto with stalmarck. apply rltTransRnext2 with (m := n); auto with stalmarck. eapply maxVarTripletsRlt; eauto with stalmarck. apply rmaxRltLeft with (p := maxVar r1); auto with stalmarck. apply H' with (1 := B); auto with stalmarck. apply rmaxRltLeft with (p := maxVar r1); auto with stalmarck. apply realizeTripletIncl with (L1 := l'); auto with stalmarck. rewrite <- H0; auto with stalmarck. apply incl_tran with (m := l2); auto with datatypes stalmarck. eapply makeTripletsFunIncl; eauto with stalmarck. apply realizeTripletIncl with (L1 := l'); auto with stalmarck. rewrite <- H0; auto with stalmarck. apply incl_tran with (m := l2); auto with datatypes stalmarck. eapply makeTripletsFunIncl; eauto with stalmarck. apply realizeTripletIncl with (L1 := l'); auto with stalmarck. rewrite <- H0; auto with datatypes stalmarck. apply realizeTripletIncl with (L1 := l'); auto with stalmarck. rewrite <- H0; auto with datatypes stalmarck. Qed.