proposition: Theorem extendEvalMakeTripletsFun : forall (e : rExpr) (l l' : list triplet) (n n' : rNat) (s' : rZ), makeTripletsFun l n e = tRC l' s' n' -> forall f : rNat -> bool, rlt (maxVar e) n -> rlt (maxVarTriplets l) n -> realizeTriplets f l -> exists g : rNat -> bool, equalBefore n f g /\ realizeTriplets g l' /\ rEval f e = rZEval g s'.
proof: Proof. RecExpr; intros f H'4 H'5 H'6. exists f; split; [ idtac | split ]; auto with stalmarck; try rewrite <- H0; red in |- *; auto with stalmarck. rewrite H0 in A. elim (H' l l' n r1 r0 A f); auto with stalmarck. intros g E; elim E; intros H'15 H'16; elim H'16; intros H'17 H'18; clear H'16 E. rewrite H'18; exists g; split; [ idtac | split ]; simpl in |- *; auto with stalmarck. case r0; simpl in |- *; auto with stalmarck. intros r2; case (g r2); auto with stalmarck. cut (rlt (maxVar r0) n); [ intros Rlt1 | apply rmaxRltLeft with (p := maxVar r1); auto with stalmarck ]. cut (rlt (maxVar r1) n); [ intros Rlt2 | apply rmaxRltRight with (m := maxVar r0); auto with stalmarck ]. cut (rlt n (rnext r3)); [ intros Rlt3 | eauto with stalmarck ]. cut (rlt (rmax (maxVar r0) (maxVar r1)) r3); [ intros Rllt0 | apply rltTransRnext2 with (m := n); auto with stalmarck ]. elim (H' l l0 n r3 r2 B f); auto with stalmarck. intros g E; elim E; intros H'17 H'18; elim H'18; intros H'19 H'20; clear H'18 E. elim (A l0 l2 r3 r5 r4 C g); auto with stalmarck. intros g0 E; elim E; intros H'18 H'21; elim H'21; intros H'22 H'23; clear H'21 E. 2: apply rltTransRnext2 with (m := n); auto with stalmarck. 2: apply maxVarTripletsRlt with (1 := B); auto with stalmarck. cut (rlt r3 (rnext r5)); [ intros Rlt4 | eauto with stalmarck ]. exists (extendFun r5 g0 (rBoolOpFun r (rEval f r0) (rEval g r1))); split; [ idtac | split ]; auto with stalmarck. apply (equalBeforeTrans n) with (y := g); auto with stalmarck. apply equalBeforeLt with (m := r3); auto with stalmarck. apply (equalBeforeTrans r3) with (y := g0); auto with stalmarck. red in |- *; simpl in |- *; auto with stalmarck. intros t H'7; elim H'7; [ intros H'8; rewrite <- H'8; clear H'7 | intros H'8; clear H'7 ]; auto with stalmarck. unfold tEval in |- *. rewrite (extendFunrZEval g0 r5 r2 (rBoolOpFun r (rEval f r0) (rEval g r1))); auto with stalmarck. rewrite (extendFunrZEval g0 r5 r4 (rBoolOpFun r (rEval f r0) (rEval g r1))); auto with stalmarck. rewrite extendFunrZEvalExact; auto with stalmarck. rewrite H'20; rewrite H'23; auto with stalmarck; auto with stalmarck. rewrite <- (equalBeforerZEval g g0 r3 r2); auto with stalmarck. case (rBoolOpFun r (rZEval g r2) (rZEval g0 r4)); auto with stalmarck. eapply makeTripletsFunMax; eauto with stalmarck. eapply makeTripletsFunMax; eauto with stalmarck. eapply rmaxRltRight; eauto with stalmarck. red in |- *; apply rltTransRnext2 with (m := r3); auto with stalmarck. change (rVlt r2 r3) in |- *. apply makeTripletsFunMax with (e := r0) (l := l) (l' := l0) (n := n); auto with stalmarck. cut (realizeTriplets (extendFun r5 g0 (rBoolOpFun r (rEval f r0) (rEval g r1))) l2); auto with stalmarck. apply supportTriplets with (f := g0); auto with stalmarck. apply equalBeforeExtend; auto with stalmarck. apply rnextMono; auto with stalmarck. eapply maxVarTripletsRlt; eauto with stalmarck. eapply rmaxRltRight; eauto with stalmarck. eapply maxVarTripletsRlt; eauto with stalmarck. rewrite extendFunrZEvalExact; auto with stalmarck. rewrite (equalBeforeREval f g r1); auto with stalmarck. apply equalBeforeLt with (m := n); auto with stalmarck. Qed.