proposition: Lemma decideAxioms : (forall x : Formula, mem _ T x \/ ~ mem _ T x) -> forall x : Formulas, (forall g : Formula, In g x -> mem _ T g) \/ (exists g : Formula, In g x /\ ~ mem _ T g).
proof: Proof. intros H x; induction x as [| a x Hrecx]. - left; intros g H0; elim H0. - induction Hrecx as [H0| H0]. + induction (H a). * left; intros g [H2| H2]. -- now rewrite <- H2. -- auto. * right; exists a; split. -- auto with datatypes. -- assumption. + right. induction H0 as [x0 H0]. exists x0. induction H0 as [H0 H1]. auto with datatypes. Qed.
imports: Coq(Ensembles) Coq(List) Coq(Arith Lia) hydras.Ackermann(folProp) hydras.Ackermann(folProof) hydras.Ackermann(folReplace) hydras.Ackermann(folLogic3) hydras.Ackermann(subProp) hydras.Ackermann(ListExt) hydras.Ackermann(NNtheory) hydras.Ackermann(NN2PA) Goedel(fixPoint) Goedel(codeSysPrf) hydras.Ackermann(PAtheory) hydras.Ackermann(code) Goedel(PRrepresentable) hydras.Ackermann(expressible) hydras.Ackermann(checkPrf) hydras.Ackermann(codeNatToTerm) hydras(Compat815)