proposition: Lemma codeSysPrfNCorrect1 : forall (f : fol.Formula L) (A : fol.Formulas L) (p : Prf L A (notH f)), (forall g : fol.Formula L, In g A -> mem _ U g) -> SysPrf T (substF (substF codeSysPrfNot 0 (natToTerm (codeFormula f))) 1 (natToTerm (codePrf A (notH f) p))).
proof: Proof. intros f A p H; unfold codeSysPrfNot;rewrite (subFormulaExist LNN). induction (eq_nat_dec 2 0) as [a | b]. - 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) as [a | ?]. * discriminate a. * induction (In_dec eq_nat_dec 2 (freeVarT (natToTerm (codePrf A (notH f) p)))). -- elim (closedNatToTerm _ _ a). -- clear b b0. apply existI with (natToTerm (codeFormula (notH f))). repeat rewrite (subFormulaAnd LNN). apply andI. apply impE with (substF (substF codeSysPrf 0 (natToTerm (codeFormula (notH f)))) 1 (natToTerm (codePrf A (notH f) p))). apply sysExtend with NN. apply TextendsNN. apply iffE2. 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. induction (freeVarSubFormula3 _ _ _ _ _ H0). apply (in_remove_neq _ _ _ _ _ H1). reflexivity. simpl in H1. decompose sum H1. discriminate H2. 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. elim (Compat815.le_not_lt 2 1). apply freeVarCodeSysPrf. eapply in_remove. apply H0. eapply Compat815.lt_n_S. apply Nat.lt_0_succ. apply codeSysPrfCorrect1. assumption. apply sysExtend with NN. apply TextendsNN. set (B := primRecFormula 1 (proj1_sig codeNotIsPR)) in *. assert (rep : Representable NN 1 codeNot B) by (unfold B in |- *; apply primRecRepresentable). apply impE with (substF (substF B 1 (natToTerm (codeFormula f))) 0 (natToTerm (codeFormula (notH f)))). apply iffE2. apply iffTrans with (substF (substF (substF (substF B 0 (var 2)) 1 (natToTerm (codeFormula f))) 1 (natToTerm (codePrf A (notH f) p))) 2 (natToTerm (codeFormula (notH f)))). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaTrans LNN). unfold not in |- *; intros. assert (H1: In 0 (freeVarF (substF B 0 (var 2)))) by eapply in_remove, H0. induction (freeVarSubFormula3 _ _ _ _ _ H1). elim (in_remove_neq _ _ _ _ _ H2). reflexivity. induction H2 as [H2| H2]. discriminate H2. apply H2. apply iffTrans with (substF (substF (substF B 0 (var 2)) 1 (natToTerm (codeFormula f))) 2 (natToTerm (codeFormula (notH f)))). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaNil LNN). unfold not in |- *; intros. induction (freeVarSubFormula3 _ _ _ _ _ H0). elim (in_remove_neq _ _ _ _ _ H1). reflexivity. elim (closedNatToTerm _ _ H1). apply iffTrans with (substF (substF (substF B 1 (natToTerm (codeFormula f))) 0 (var 2)) 2 (natToTerm (codeFormula (notH f)))). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaExch LNN). discriminate. unfold not in |- *; intros. simpl in H0. decompose sum H0. discriminate H1. apply closedNatToTerm. apply (subFormulaTrans LNN). unfold not in |- *; intros. assert (H1: In 2 (freeVarF (substF B 1 (natToTerm (codeFormula f))))) by eapply in_remove, H0. induction (freeVarSubFormula3 _ _ _ _ _ H1). induction rep as (H3, H4). apply (Compat815.le_not_lt 2 1). apply H3. eapply in_remove. apply H2. apply Compat815.lt_n_S. apply Nat.lt_0_succ. apply (closedNatToTerm _ _ H2). induction rep as (H0, H1). unfold RepresentableHelp in H1. apply impE with (substF (equal (var 0) (natToTerm (codeNot (codeFormula f)))) 0 (natToTerm (codeFormula (notH f)))). apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply H1. rewrite (subFormulaEqual LNN). rewrite (subTermVar1 LNN). rewrite (subTermNil LNN). rewrite (codeNotCorrect L cL). apply eqRefl. apply closedNatToTerm. 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)