proposition: Lemma codeSysPrfCorrect2 : 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 f, SysPrf T (notH (substF (substF codeSysPrf 0 (natToTerm (codeFormula f))) 1 (natToTerm (codePrf A f p)))).
proof: Proof. intros. unfold codeSysPrf in |- *. set (nvl := 2 :: 1 :: 0 :: v0 :: nil) in *. set (nv := newVar nvl) in *. assert (H0: nv <> 0). { unfold nv, not in |- *; intros; elim (newVar1 nvl). rewrite H0; unfold nvl in |- *. simpl in |- *; auto. } assert (H1: nv <> 1). { unfold nv, not in |- *; intros; elim (newVar1 nvl). rewrite H1; unfold nvl in |- *. simpl in |- *; auto. } assert (H2: nv <> 2). { unfold nv, not in |- *; intros; elim (newVar1 nvl). rewrite H2; unfold nvl in |- *. simpl in |- *; auto. } assert (H3: nv <> v0). { unfold nv, not in |- *; intros; elim (newVar1 nvl). rewrite H3; unfold nvl in |- *. simpl in |- *; auto. } set (F := primRecFormula 2 (proj1_sig (checkPrfIsPR L cL codeArityF codeArityR codeArityFIsPR codeArityRIsPR))) in *. set (J := primRecFormula 2 (proj1_sig codeInIsPR)) in *. rewrite (subFormulaExist LNN). induction (eq_nat_dec nv 0). elim H0; assumption. induction (In_dec eq_nat_dec nv (freeVarT (natToTerm (codeFormula f)))). elim (closedNatToTerm _ _ a). clear b b0. rewrite (subFormulaExist LNN). induction (eq_nat_dec nv 1). elim H1; assumption. induction (In_dec eq_nat_dec nv (freeVarT (natToTerm (codePrf A f p)))). elim (closedNatToTerm _ _ a). clear b b0. repeat rewrite (subFormulaAnd LNN). apply nExist. set (n := codePrf A f p) in *. apply impE with (forallH nv (notH (andH (equal (Succ (var nv)) (natToTerm (checkPrf L cL codeArityF codeArityR (codeFormula f) n))) (substF (substF (forallH (S nv) (impH (LT (var (S nv)) (var nv)) (orH (substF (substF (substF J 2 (var (S nv))) 1 (var nv)) 0 Zero) (substF fU v0 (var (S nv)))))) 0 (natToTerm (codeFormula f))) 1 (natToTerm n))))). apply sysExtend with NN. assumption. apply iffE2. apply (reduceForall LNN). apply closedNN. apply (reduceNot LNN). apply (reduceAnd LNN). apply iffTrans with (substF (substF (substF F 2 (natToTerm (codeFormula f))) 1 (natToTerm n)) 0 (Succ (var nv))). apply iffTrans with (substF (substF (substF F 0 (Succ (var nv))) 2 (natToTerm (codeFormula f))) 1 (natToTerm n)). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaTrans LNN). unfold not in |- *; intros. assert (H5 : In 0 (freeVarF (substF F 0 (Succ (var nv))))) by eapply in_remove, H4. induction (freeVarSubFormula3 _ _ _ _ _ H5). elim (in_remove_neq _ _ _ _ _ H6). reflexivity. simpl in H6. decompose sum H6. apply H0; assumption. apply iffTrans with (substF (substF (substF F 2 (natToTerm (codeFormula f))) 0 (Succ (var nv))) 1 (natToTerm n)). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaExch LNN). discriminate. unfold not in |- *; intros. simpl in H4. decompose sum H4. apply H2; assumption. apply closedNatToTerm. apply (subFormulaExch LNN). discriminate. unfold not in |- *; intros. simpl in H4. decompose sum H4. apply H1; assumption. apply closedNatToTerm. assert (H4: Representable NN 2 (checkPrf L cL codeArityF codeArityR) (primRecFormula 2 (proj1_sig (checkPrfIsPR L cL codeArityF codeArityR codeArityFIsPR codeArityRIsPR)))) by apply primRecRepresentable. fold F in H4; induction H4 as (H4, H5); simpl in H5. apply iffTrans with (substF (equal (var 0) (natToTerm (checkPrf L cL codeArityF codeArityR (codeFormula f) n))) 0 (Succ (var nv))). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply H5. rewrite (subFormulaEqual LNN). rewrite (subTermVar1 LNN). rewrite (subTermNil LNN). apply iffRefl. apply closedNatToTerm. apply iffRefl. unfold n in |- *. rewrite checkPrfCorrect1. decompose record H /r; intros x H5 H6. apply impE with (notH (substF fU v0 (natToTerm (codeFormula x)))). apply sysExtend with NN. assumption. apply impI. assert (H4: forall v : nat, ~ In v (freeVarF (notH (substF fU v0 (natToTerm (codeFormula x)))))). { unfold not in |- *; intros. induction (freeVarSubFormula3 _ _ _ _ _ H4). absurd (v = v0). eapply in_remove_neq. apply H7. apply freeVarfU. eapply in_remove. apply H7. apply (closedNatToTerm _ _ H7). } assert (H7: forall v : nat, ~ In_freeVarSys LNN v (Ensembles.Add (fol.Formula LNN) NN (notH (substF fU v0 (natToTerm (codeFormula x)))))). { unfold not in |- *; intros. induction H7 as (x0, H7); induction H7 as (H7, H8). induction H8 as [x0 H8| x0 H8]. elim (closedNN v). exists x0. auto. induction H8. apply (H4 v). assumption. } apply forallI. apply H7. apply nAnd. unfold orH at 1 in |- *. apply impTrans with (equal (Succ (var nv)) (natToTerm (S (codeList (map (codeFormula) A))))). apply impI. apply nnE. apply Axm; right; constructor. apply impI. rewrite <- (subFormulaId LNN (notH (substF (substF (forallH (S nv) (impH (LT (var (S nv)) (var nv)) (orH (substF (substF (substF J 2 (var (S nv))) 1 (var nv)) 0 Zero) (substF fU v0 (var (S nv)))))) 0 (natToTerm (codeFormula f))) 1 (natToTerm (codePrf A f p)))) nv) . apply impE with (substF (notH (substF (substF (forallH (S nv) (impH (LT (var (S nv)) (var nv)) (orH (substF (substF (substF J 2 (var (S nv))) 1 (var nv)) 0 Zero) (substF fU v0 (var (S nv)))))) 0 (natToTerm (codeFormula f))) 1 (natToTerm (codePrf A f p)))) nv (natToTerm (codeList (map (codeFormula) A)))). apply (subWithEquals LNN). apply eqSym. apply impE with (equal (Succ (var nv)) (natToTerm (S (codeList (map (codeFormula) A))))). apply sysWeaken. simpl in |- *. apply sysWeaken. apply nn2. apply Axm; right; constructor. apply sysWeaken. assert (H8: S nv <> 1). { intros H8; elim (Compat815.le_not_lt (S nv) 1). - rewrite H8. apply le_n. - apply Nat.lt_lt_succ_r; unfold nv; apply newVar2. unfold nvl; simpl; auto. } assert (H9: S nv <> 2). { intros H9; elim (Compat815.le_not_lt (S nv) 2). - rewrite H9; apply le_n. - apply Nat.lt_lt_succ_r; unfold nv; apply newVar2. unfold nvl; simpl; auto. } assert (H10 :S nv <> nv) by lia. rewrite (subFormulaForall LNN). induction (eq_nat_dec (S nv) 0). discriminate a. induction (In_dec eq_nat_dec (S nv) (freeVarT (natToTerm (codeFormula f)))). elim (closedNatToTerm _ _ a). clear b b0. rewrite (subFormulaForall LNN). induction (eq_nat_dec (S nv) 1). elim H8; assumption. induction (In_dec eq_nat_dec (S nv) (freeVarT (natToTerm (codePrf A f p)))). elim (closedNatToTerm _ _ a). clear b b0. rewrite (subFormulaNot LNN). rewrite (subFormulaForall LNN). induction (eq_nat_dec (S nv) nv). elim H10; assumption. induction (In_dec eq_nat_dec (S nv) (freeVarT (natToTerm (codeList (map (codeFormula) A))))). elim (closedNatToTerm _ _ a). clear b b0. apply nForall. apply existI with (natToTerm (codeFormula x)). rewrite (subFormulaNot LNN). repeat rewrite (subFormulaImp LNN). apply nImp. apply andI. assert (H11: forall (t1 t2 s : Term) (v : nat), substF (t1 < t2)%fol v s = (substT t1 v s < substT t2 v s)%fol) by reflexivity. repeat rewrite H11. repeat rewrite (subTermVar1 LNN) || rewrite (subTermVar2 LNN); try unfold not in |- *; intros. rewrite (subTermNil LNN). apply sysWeaken. apply natLT. cut (In x A). generalize x A. intros x0 A0 H12; induction A0 as [| a A0 HrecA0]. elim H12. induction H12 as [H12| H12]. rewrite H12. simpl in |- *. apply Compat815.le_lt_n_Sm. apply cPairLe1. apply Nat.lt_le_trans with (codeList (map (codeFormula) A0)). auto. simpl in |- *. apply le_S. apply cPairLe2. assumption. apply closedNatToTerm. apply H1; auto. apply H0; auto. apply H10; auto. apply H8; auto. discriminate H12. repeat rewrite (subFormulaOr LNN). apply nOr. apply andI. apply sysWeaken. assert (H11: Representable NN 2 codeIn J) by ( unfold J in |- *; apply primRecRepresentable). induction H11 as (H11, H12). apply impE with (notH (substF (substF (substF J 2 (natToTerm (codeFormula x))) 1 (natToTerm (codeList (map (codeFormula) A)))) 0 Zero)). apply cp2. apply iffE1. apply iffTrans with (substF (substF (substF (substF (substF (substF J 2 (var (S nv))) 1 (var nv)) 0 Zero) 1 (natToTerm (codePrf A f p))) nv (natToTerm (codeList (map (codeFormula) A)))) (S nv) (natToTerm (codeFormula x))). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaNil LNN). unfold not in |- *; intros. induction (freeVarSubFormula3 _ _ _ _ _ H13). elim (in_remove_neq _ _ _ _ _ H14). reflexivity. apply H14. apply iffTrans with (substF (substF (substF (substF (substF (substF J 2 (var (S nv))) 1 (var nv)) 1 (natToTerm (codePrf A f p))) 0 Zero) nv (natToTerm (codeList (map (codeFormula) A)))) (S nv) (natToTerm (codeFormula x))). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaExch LNN). discriminate. auto. apply closedNatToTerm. apply iffTrans with (substF (substF (substF (substF (substF J 2 (var (S nv))) 1 (var nv)) 0 Zero) nv (natToTerm (codeList (map (codeFormula) A)))) (S nv) (natToTerm (codeFormula x))). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaNil LNN). unfold not in |- *; intros. induction (freeVarSubFormula3 _ _ _ _ _ H13). elim (in_remove_neq _ _ _ _ _ H14). reflexivity. simpl in H14. decompose sum H14. apply H1; assumption. apply iffTrans with (substF (substF (substF (substF (substF J 2 (var (S nv))) 1 (var nv)) nv (natToTerm (codeList (map (codeFormula) A)))) 0 Zero) (S nv) (natToTerm (codeFormula x))). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaExch LNN). intros H13; apply H0; symmetry in |- *; assumption. auto. apply closedNatToTerm. apply iffTrans with (substF (substF (substF (substF J 2 (var (S nv))) 1 (natToTerm (codeList (map (codeFormula) A)))) 0 Zero) (S nv) (natToTerm (codeFormula x))). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaTrans LNN). unfold not in |- *; intros. assert (H14: In nv (freeVarF (substF J 2 (var (S nv))))) by eapply in_remove, H13. induction (freeVarSubFormula3 _ _ _ _ _ H14). apply (Compat815.le_not_lt nv 2). apply H11. eapply in_remove. apply H15. destruct nv as [| n0]. elim H0; reflexivity. destruct n0. elim H1; reflexivity. destruct n0. elim H2; reflexivity. lia. simpl in H15. decompose sum H15. apply H10; assumption. apply iffTrans with (substF (substF (substF (substF J 2 (var (S nv))) 1 (natToTerm (codeList (map (codeFormula) A)))) (S nv) (natToTerm (codeFormula x))) 0 Zero). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaExch LNN). discriminate. auto. apply closedNatToTerm. apply iffTrans with (substF (substF (substF (substF J 2 (var (S nv))) (S nv) (natToTerm (codeFormula x))) 1 (natToTerm (codeList (map (codeFormula) A)))) 0 Zero). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaExch LNN). unfold not in |- *; intros. apply H8; symmetry in |- *; assumption. apply closedNatToTerm. apply closedNatToTerm. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaTrans LNN). unfold not in |- *; intros. apply (Compat815.le_not_lt (S nv) 2). apply H11. eapply in_remove. apply H13. destruct nv as [| n0]. elim H8; reflexivity. destruct n0. elim H9; reflexivity. repeat apply Compat815.lt_n_S. apply Nat.lt_0_succ. simpl in H12. apply impE with (notH (substF (equal (var 0) (natToTerm (codeIn (codeFormula x) (codeList (map (codeFormula) A))))) 0 Zero)). apply cp2. apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply H12. rewrite (subFormulaEqual LNN). rewrite (subTermVar1 LNN). rewrite (subTermNil LNN). rewrite codeInCorrect. induction (In_dec eq_nat_dec (codeFormula x) (map (codeFormula) A)). replace Zero with (natToTerm 0). apply natNE. discriminate. reflexivity. elim b. cut (In x A). generalize A x. intros A0 x0 H13; induction A0 as [| a A0 HrecA0]. elim H13. induction H13 as [H13| H13]. rewrite H13. simpl in |- *. auto. simpl in |- *. auto. assumption. apply closedNatToTerm. apply impE with (notH (substF fU v0 (natToTerm (codeFormula x)))). apply sysWeaken. apply cp2. apply iffE1. assert (H11: forall v : nat, ~ In v (List.remove eq_nat_dec v0 (freeVarF fU))). { unfold not in |- *; intros. absurd (v = v0). eapply in_remove_neq. apply H11. apply freeVarfU. eapply in_remove. apply H11. } apply iffTrans with (substF (substF (substF (substF fU v0 (var (S nv))) 1 (natToTerm (codePrf A f p))) nv (natToTerm (codeList (map (codeFormula) A)))) (S nv) (natToTerm (codeFormula x))). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaNil LNN). unfold not in |- *; intros. induction (freeVarSubFormula3 _ _ _ _ _ H12). apply (H11 0). assumption. simpl in H13. decompose sum H13. discriminate H14. apply iffTrans with (substF (substF (substF fU v0 (var (S nv))) nv (natToTerm (codeList (map (codeFormula) A)))) (S nv) (natToTerm (codeFormula x))). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaNil LNN). unfold not in |- *; intros. induction (freeVarSubFormula3 _ _ _ _ _ H12). apply (H11 1). assumption. simpl in H13. decompose sum H13. apply H8; assumption. apply iffTrans with (substF (substF fU v0 (var (S nv))) (S nv) (natToTerm (codeFormula x))). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaNil LNN). unfold not in |- *; intros. induction (freeVarSubFormula3 _ _ _ _ _ H12). apply (H11 nv). assumption. simpl in H13. decompose sum H13. apply H10; assumption. apply (subFormulaTrans LNN). apply H11. apply Axm; right; constructor. apply expressU2. assumption. assumption. 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)