proposition: Lemma codeSysPrfNCorrect2 : forall (f : fol.Formula L) (A : fol.Formulas L), (exists g : fol.Formula L, In g A /\ ~ mem _ U g) -> forall p : Prf L A (notH f), SysPrf T (notH (substF (substF codeSysPrfNot 0 (natToTerm (codeFormula f))) 1 (natToTerm (codePrf A (notH f) p)))).
proof: Proof. intros f A H p; unfold codeSysPrfNot in |- *. rewrite (subFormulaExist LNN). induction (eq_nat_dec 2 0). discriminate a. induction (In_dec eq_nat_dec 2 (freeVarT (natToTerm (codeFormula f)))). elim (closedNatToTerm _ _ a). clear b b0. rewrite (subFormulaExist LNN). induction (eq_nat_dec 2 1). discriminate a. induction (In_dec eq_nat_dec 2 (freeVarT (natToTerm (codePrf A (notH f) p)))). elim (closedNatToTerm _ _ a). clear b b0. apply nExist. apply impE with (notH (substF (substF codeSysPrf 0 (natToTerm (codeFormula (notH f)))) 1 (natToTerm (codePrf A (notH f) p)))). apply sysExtend with NN. apply TextendsNN. apply impI. apply forallI. unfold not in |- *; intros. induction H0 as (x, H0); induction H0 as (H0, H1). induction H1 as [x H1| x H1]. apply (closedNN 2). exists x. auto. induction H1. SimplFreeVar. elim (Compat815.le_not_lt 2 1). apply freeVarCodeSysPrf. apply H1. apply Nat.lt_succ_diag_r. repeat rewrite (subFormulaAnd LNN). apply nAnd. apply orSym. unfold orH. apply impTrans with (substF (substF (primRecFormula 1 (proj1_sig codeNotIsPR)) 1 (natToTerm (codeFormula f))) 0 (var 2)). apply sysWeaken. apply impTrans with (substF (substF (substF (substF (primRecFormula 1 (proj1_sig codeNotIsPR)) 0 (var 2)) 1 (var 0)) 0 (natToTerm (codeFormula f))) 1 (natToTerm (codePrf A (notH f) p))). apply impI. apply nnE. apply Axm; right; constructor. apply iffE1. apply iffTrans with (substF (substF (substF (primRecFormula 1 (proj1_sig codeNotIsPR)) 0 (var 2)) 1 (natToTerm (codeFormula f))) 1 (natToTerm (codePrf A (notH f) p))). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaTrans LNN). unfold not in |- *; intros; SimplFreeVar. discriminate H1. apply iffTrans with (substF (substF (primRecFormula 1 (proj1_sig codeNotIsPR)) 0 (var 2)) 1 (natToTerm (codeFormula f))). apply (subFormulaNil LNN). unfold not in |- *; intros; SimplFreeVar. apply (subFormulaExch LNN). discriminate. unfold not in |- *; intros; SimplFreeVar. discriminate H1. unfold not in |- *; intros; SimplFreeVar. set (B := primRecFormula 1 (proj1_sig codeNotIsPR)) in *. assert (rep : Representable NN 1 codeNot B) by (unfold B in |- *; apply primRecRepresentable). induction rep as (H0, H1). unfold RepresentableHelp in H1. apply impTrans with (substF (equal (var 0) (natToTerm (codeNot (codeFormula f)))) 0 (var 2)). apply iffE1. apply sysWeaken. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply H1. rewrite (subFormulaEqual LNN). rewrite (subTermVar1 LNN). rewrite (subTermNil LNN). rewrite (codeNotCorrect L) with (a := f). apply impI. rewrite <- (subFormulaId LNN (notH (substF (substF (substF codeSysPrf 0 (var 2)) 0 (natToTerm (codeFormula f))) 1 (natToTerm (codePrf A (notH f) p)))) 2) . apply impE with (substF (notH (substF (substF (substF codeSysPrf 0 (var 2)) 0 (natToTerm (codeFormula f))) 1 (natToTerm (codePrf A (notH f) p)))) 2 (natToTerm (codeFormula (notH f)))). eapply (subWithEquals LNN). apply eqSym. apply Axm; right; constructor. apply sysWeaken. rewrite (subFormulaNot LNN). apply impE with (notH (substF (substF codeSysPrf 0 (natToTerm (codeFormula (notH f)))) 1 (natToTerm (codePrf A (notH f) p)))). apply cp2. apply sysWeaken. apply iffE1. apply iffTrans with (substF (substF (substF codeSysPrf 0 (var 2)) 1 (natToTerm (codePrf A (notH f) p))) 2 (natToTerm (codeFormula (notH f)))). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaNil LNN). unfold not in |- *; intros; SimplFreeVar. discriminate. apply iffTrans with (substF (substF (substF codeSysPrf 0 (var 2)) 2 (natToTerm (codeFormula (notH f)))) 1 (natToTerm (codePrf A (notH f) p))). apply (subFormulaExch LNN). discriminate. apply closedNatToTerm. apply closedNatToTerm. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaTrans LNN). unfold not in |- *; intros; SimplFreeVar. elim (Compat815.le_not_lt 2 1). apply freeVarCodeSysPrf. apply H3. auto with arith. apply Axm; right; constructor. apply closedNatToTerm. apply codeSysPrfCorrect2. assumption. Qed.
imports: Coq(Ensembles) Coq(List) hydras.Ackermann(checkPrf) hydras.Ackermann(code) hydras.Ackermann(Languages) hydras.Ackermann(folProp) hydras.Ackermann(folProof) hydras.Ackermann(folLogic3) hydras.Ackermann(folReplace) Goedel(PRrepresentable) hydras.Ackermann(expressible) hydras.Ackermann(primRec) Coq(Arith Lia) hydras.Ackermann(PA) hydras.Ackermann(NNtheory) hydras.Ackermann(codeList) hydras.Ackermann(subProp) hydras.Ackermann(ListExt) hydras.Ackermann(cPair) hydras.Ackermann(wellFormed) hydras.Ackermann(prLogic) hydras(Compat815)