proposition: Theorem stalmarckComplete : forall e : Expr, Tautology e -> match makeTriplets (norm e) with | tRC l s n => ex (fun S : State => stalmarckP (addEq (s, rZFalse) nil) l S /\ contradictory S) end.
proof: Proof. intros e; generalize (refl_equal (makeTriplets (norm e))); pattern (makeTriplets (norm e)) at -2 in |- *; case (makeTriplets (norm e)). intros l r r0 H H1. elim (DilemmaContrad (addEq (r, rZFalse) nil) l r rZTrue); auto with stalmarck. intros S HS; exists S; auto with stalmarck. elim (TautoRTauto e); intros Thm1 Thm2. elim (rTautotTauto (norm e)); intros Thm3 Thm4. generalize Thm3; unfold tTautology in |- *; rewrite <- H; simpl in |- *; auto with stalmarck. Qed.
imports: Stalmarck(PolyListAux) Stalmarck(makeTriplet) Coq(Arith)