proposition: Lemma codeSysPrfCorrect3 : forall (f : fol.Formula L) (n : nat), (forall (A : list (fol.Formula L)) (p : Prf L A f), n <> codePrf A f p) -> SysPrf T (notH (substF (substF codeSysPrf 0 (natToTerm (codeFormula f))) 1 (natToTerm n))).
proof: Proof. intros f n H; unfold codeSysPrf. 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) as [? | b]. - elim H0; assumption. - induction (In_dec eq_nat_dec nv (freeVarT (natToTerm (codeFormula f)))) as [a | b0]. + 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 n))). elim (closedNatToTerm _ _ a). clear b b0. repeat rewrite (subFormulaAnd LNN). apply nExist. apply sysExtend with NN. assumption. apply forallI. apply closedNN. apply nAnd. apply orI1. apply impE with (notH (substF (substF (substF F 2 (natToTerm (codeFormula f))) 1 (natToTerm n)) 0 (Succ (var nv)))). apply cp2. apply iffE1. 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). intros H4. 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 impE with (notH (substF (equal (var 0) (natToTerm (checkPrf L cL codeArityF codeArityR (codeFormula f) n))) 0 (Succ (var nv)))). apply cp2. apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply H5. rewrite (subFormulaEqual LNN). rewrite (subTermVar1 LNN). rewrite (subTermNil LNN). induction (eq_nat_dec (checkPrf L cL codeArityF codeArityR (codeFormula f) n) 0). rewrite a. apply nn1. decompose record (checkPrfCorrect2 L cL codeArityF codeArityR codeArityFIsCorrect1 codeArityFIsCorrect2 codeArityRIsCorrect1 codeArityRIsCorrect2 (codeFormula f) n b) /r; intros x H7 x0 x1 H8. assert (H6: x = f). { eapply codeFormulaInj; assumption. } rewrite <- H6 in H. elim (H x0 x1). symmetry in |- *. assumption. 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)