proposition: Lemma searchProof : (forall x : Formula, mem _ T x \/ ~ mem _ T x) -> forall (a b : Formula) (A : Formulas) (p : Prf LNN A a), (exists B : Formulas, (exists q : Prf LNN B b, codePrf _ _ q < S (codePrf _ _ p) /\ (forall x : Formula, In x B -> mem _ T x))) \/ (forall (B : Formulas) (q : Prf LNN B b), codePrf _ _ q < S (codePrf _ _ p) -> exists g : Formula, In g B /\ ~ mem _ T g).
proof: Proof. intros H a b A p. induction (S (codePrf A a p)). - right; intros B q H0; lia. - induction IHn as [H0| H0]. + left; decompose record H0 /r; intros x x0 H1 H3; exists x, x0; auto. + induction (eq_nat_dec (checkPrf LNN LcodeLNN codeArityLNTF codeArityLNNR (codeFormula b) n) 0) as [a0 | b0]. * right; intros B q H1; induction (proj1 (Nat.lt_eq_cases _ _) (proj1 (Nat.lt_succ_r _ _) H1)). -- eauto. -- rewrite <- H2 in a0. rewrite (checkPrfCorrect1 LNN LcodeLNN codeArityLNTF codeArityLNNR codeArityLNTFIsCorrect1 codeArityLNNRIsCorrect1) in a0. discriminate a0. * decompose record (checkPrfCorrect2 LNN LcodeLNN codeArityLNTF codeArityLNNR codeArityLNTFIsCorrect1 codeArityLNTFIsCorrect2 codeArityLNNRIsCorrect1 codeArityLNNRIsCorrect2 _ _ b0) /r; intros x H2 x0 x1 H3. assert (H1: x = b). { eapply codeFormulaInj. assumption. } rewrite <- H1. induction (decideAxioms H x0) as [H4 | ?]. -- left; exists x0, x1. unfold codePrf; rewrite H3; auto. -- right; intros B q H5. induction (proj1 (Nat.lt_eq_cases _ _) (proj1 (Nat.lt_succ_r _ _) H5)) as [H6 | H6]. ++ rewrite <- H1 in H0; eauto. ++ assert (H7: B = x0). { eapply (codePrfInjAxm LNN). - transitivity n. + unfold codePrf in H6; apply H6. + symmetry; apply H3. } now rewrite H7. 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)