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. - destruct Hrecx as [H0| H0]. + induction (H a) as [H1 | H1]. * left; intros g [H2 | H2]. -- now subst. -- auto. * right; exists a; split. -- auto with datatypes. -- assumption. + right. destruct H0 as [x0 [H0 H1]]. exists x0; split. * auto with datatypes. * assumption. 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) Goedel(fixPoint) Goedel(codeSysPrf) hydras.Ackermann(NNtheory) hydras.Ackermann(code) Goedel(PRrepresentable) hydras.Ackermann(expressible) hydras.Ackermann(checkPrf) hydras.Ackermann(codeNatToTerm) hydras(Compat815)