proposition: Theorem runCorrect : forall (m : nat) (e : Expr), match run m e with | quatuor Ar' false L T => True | quatuor Ar' true L T => Tautology e end.
proof: Proof. intros m e; unfold run in |- *. CaseEq (makeTriplets (norm e)). intros l r r0 H'; unfold letP in |- *. generalize (stalCorrect (getT (buildL l)) l (getTCorrect l) (nat_of_P (valRz r)) m (rArrayInit vM (fun _ : rNat => class nil)) r rZFalse nil rIwF initCorrect). case (stal (getT (buildL l)) (nat_of_P (valRz r)) m (rArrayInit vM (fun _ : rNat => class nil)) r rZFalse); auto with stalmarck. intros Ar1 b1 L1 T1; case b1; auto with stalmarck. intros H'0; Elimc H'0; intros S' E; Elimc E; intros H'0 H'1; Elimc H'1; intros H'1 H'2. case (TautoRTauto e). intros H'3 H'4; apply H'4. case (rTautotTauto (norm e)). intros H'5 H'6; apply H'6; auto with stalmarck. red in |- *; rewrite H'. apply stalmarckGivesValidEquation with (S := S'); auto with stalmarck. Qed.
imports: Coq(ZArith)