proposition: Lemma checkPrfCorrect2 (n m : nat): checkPrf n m <> 0 -> exists f : Formula, codeFormula f = n /\ (exists l : list Formula, (exists p : Prf l f, codePrf l f p = m)).
proof: Proof. revert n m; assert (multLemma1 : forall a b : nat, a * b <> 0 -> a <> 0). { intros a b H H0; apply H; rewrite H0; reflexivity. } assert (multLemma2 : forall a b : nat, a * b <> 0 -> b <> 0). { intros a b H H0; rewrite Nat.mul_comm in H. now apply (multLemma1 b a). } assert (H: forall m n : nat, n < m -> checkPrf (car n) (cdr n) <> 0 -> exists f : Formula, (exists l : list Formula, (exists p : Prf l f, cPair (codeFormula f) (codePrf l f p) = n))). { intro m; induction m as [| m Hrecm]. - intros n H H0; elim (Nat.nlt_0_r _ H). - intros n H H0; assert (H': n <= m) by lia. rewrite Nat.lt_eq_cases in H'; destruct H' as [H1 | H1]. + apply Hrecm; assumption. + unfold checkPrf in H0. assert (H2: wellFormedFormula (car n) <> 0). { destruct (wellFormedFormula (car n)). assumption. discriminate. } induction (wellFormedFormulaCorrect2 L cL codeArityF codeArityFIsCorrect1 codeArityFIsCorrect2 codeArityR codeArityRIsCorrect1 codeArityRIsCorrect2 _ H2) as [x H3]. exists x. destruct (wellFormedFormula (car n)). * now elim H2. * simpl in H0; clear H2; unfold checkPrfHelp in H0. set (A := fun p recs : nat => switchPR (car (cdr p)) (switchPR (pred (car (cdr p))) (switchPR (pred (pred (car (cdr p)))) (switchPR (pred (pred (pred (car (cdr p))))) (switchPR (pred (pred (pred (pred (car (cdr p)))))) (switchPR (pred (pred (pred (pred (pred (car (cdr p))))))) (switchPR (pred (pred (pred (pred (pred (pred (car (cdr p)))))))) (switchPR (pred (pred (pred (pred (pred (pred (pred (car (cdr p))))))))) (switchPR (pred (pred (pred (pred (pred (pred (pred (pred (car (cdr p)))))))))) (switchPR (pred (pred (pred (pred (pred (pred (pred (pred (pred (car (cdr p))))))))))) (switchPR (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred (car (cdr p)))))))))))) (switchPR (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred (car (cdr p))))))))))))) (switchPR (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred (car (cdr p)))))))))))))) (switchPR (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred (car (cdr p))))))))))))))) 0 (checkPrfEQ5 p recs)) (checkPrfEQ4 p recs)) (checkPrfEQ3 p recs)) (checkPrfEQ2 p recs)) (checkPrfEQ1 p recs)) (checkPrfFA3 p recs)) (checkPrfFA2 p recs)) (checkPrfFA1 p recs)) (checkPrfCP p recs)) (checkPrfIMP2 p recs)) (checkPrfIMP1 p recs)) (checkPrfGEN p recs)) (checkPrfMP p recs)) (checkPrfAXM p recs)) in *. unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList in H0; rewrite computeEvalStrongRecHelp in H0; unfold compose2, evalComposeFunc, evalOneParamList, evalList in H0; simpl in H0. rewrite cPairProjections1 in H0. assert (H2: cPair (car (cdr n)) (cdr (cdr n)) = cdr n) by apply cPairProjections. unfold A at 1 in H0. repeat first [ rewrite cPairProjections1 in H0 | rewrite cPairProjections2 in H0 ]. destruct (car (cdr n)). -- simpl in H0. unfold checkPrfAXM in H0. repeat first [ rewrite cPairProjections1 in H0 | rewrite cPairProjections2 in H0 ]. rewrite <- H3 in H0. induction (eq_nat_dec (cdr (cdr n)) (codeFormula x)) as [a | ?]. ++ exists (x :: nil). exists (AXM L x). rewrite H3. simpl in |- *. rewrite a in H2. rewrite H2. apply cPairProjections. ++ elim H0. unfold charFunction in |- *. rewrite nat_eqb_false. reflexivity. assumption. -- destruct n1. ++ simpl in H0. unfold checkPrfMP in H0. repeat first [ rewrite cPairProjections1 in H0 | rewrite cPairProjections2 in H0 ]. assert (H4: cdr (cdr n) < n). { apply Nat.lt_le_trans with (cPair 1 (cdr (cdr n))); [ idtac | rewrite H2; apply cPairLe2A ]. apply cPairLt2. } assert (H5: car (cdr (cdr n)) < n). { apply Nat.le_lt_trans with (cdr (cdr n)). apply cPairLe1A. assumption. } assert (H6: cdr (cdr (cdr n)) < n). { apply Nat.le_lt_trans with (cdr (cdr n)). apply cPairLe2A. assumption. } rewrite evalStrongRecHelp1 in H0. ** rewrite evalStrongRecHelp1 in H0. assert (wellFormedFormula (car (cdr (cdr (cdr n)))) <> 0). { intro H7; apply H0; now rewrite H7. } induction (eq_nat_dec (car (car (cdr (cdr n)))) (codeImp (car (cdr (cdr (cdr n)))) (car n))). induction (wellFormedFormulaCorrect2 L cL codeArityF codeArityFIsCorrect1 codeArityFIsCorrect2 codeArityR codeArityRIsCorrect1 codeArityRIsCorrect2 _ H7). assert (H9: checkPrf (car (car (cdr (cdr n)))) (cdr (car (cdr (cdr n)))) <> 0). { unfold checkPrf in |- *. rewrite a. rewrite <- H3. rewrite <- H8. rewrite codeImpCorrect. rewrite (wellFormedFormulaCorrect1 L cL codeArityF codeArityFIsCorrect1 codeArityR codeArityRIsCorrect1). simpl; unfold checkPrfHelp in |- *; fold A in |- *. rewrite H8. rewrite H3. replace (cPair 1 (cPair (car (cdr (cdr (cdr n)))) (car n))) with (car (car (cdr (cdr n)))). { rewrite cPairProjections. destruct (evalStrongRec 0 A (car (cdr (cdr n)))). rewrite Nat.mul_comm in H0. rewrite (Nat.mul_comm (charFunction 2 Nat.eqb (car (car (cdr (cdr n)))) (codeImp (car (cdr (cdr (cdr n)))) (car n)))) in H0. simpl in H0. assumption. discriminate. } } assert (H10: checkPrf (car (cdr (cdr (cdr n)))) (cdr (cdr (cdr (cdr n)))) <> 0). { unfold checkPrf; rewrite <- H8. rewrite (wellFormedFormulaCorrect1 L cL codeArityF codeArityFIsCorrect1 codeArityR codeArityRIsCorrect1). simpl; unfold checkPrfHelp; fold A. rewrite H8. rewrite cPairProjections. destruct (evalStrongRec 0 A (cdr (cdr (cdr n)))). - rewrite Nat.mul_comm in H0. rewrite (Nat.mul_comm (charFunction 2 Nat.eqb (car (car (cdr (cdr n)))) (codeImp (car (cdr (cdr (cdr n)))) (car n)))) in H0. rewrite (Nat.mul_comm (evalStrongRec 0 A (car (cdr (cdr n))))) in H0. simpl in H0. assumption. - discriminate. } assert (H11: car (cdr (cdr n)) < m). { apply Nat.lt_le_trans with n. assumption. rewrite H1; apply le_n. } assert (H12: cdr (cdr (cdr n)) < m). { apply Nat.lt_le_trans with n. assumption. rewrite H1; apply le_n. } induction (Hrecm _ H11 H9). induction (Hrecm _ H12 H10). induction H13 as (x3, H13). induction H13 as (x4, H13). induction H14 as (x5, H14). induction H14 as (x6, H14). exists (x3 ++ x5). rewrite <- H13 in a. rewrite <- H14 in a. repeat rewrite cPairProjections1 in a. rewrite <- H3 in a. rewrite codeImpCorrect in a. assert (H15: x1 = impH x2 x). { eapply (codeFormulaInj ). assumption. } cut (cPair (codeFormula x1) (codePrf x3 x1 x4) = car (cdr (cdr n))). { generalize x4; clear H13 x4; rewrite H15. intros x4 H13; exists (MP L x3 x5 x2 x x4 x6). rewrite <- (cPairProjections n). rewrite H3. simpl in |- *. rewrite <- H2. replace (cPair 1 (cPair (codeFormula x2) (codeFormula x))) with (codeFormula x1). { rewrite H14; rewrite H15; rewrite H13. rewrite cPairProjections; reflexivity. } } assumption. unfold charFunction in H0; rewrite nat_eqb_false in H0. rewrite Nat.mul_comm in H0. simpl in H0; elim H0. reflexivity. assumption. rewrite cPairProjections; assumption. ** rewrite cPairProjections; assumption. ++ destruct n1. ** simpl in H0. unfold checkPrfGEN in H0. repeat first [ rewrite cPairProjections1 in H0 | rewrite cPairProjections2 in H0 ]. assert (cdr (cdr (cdr n)) < n). eapply Nat.le_lt_trans. apply cPairLe2A. apply Nat.lt_le_trans with (cPair 2 (cdr (cdr n))); [ idtac | rewrite H2; apply cPairLe2A ]. apply cPairLt2. rewrite evalStrongRecHelp1 in H0. induction (eq_nat_dec (cPair 3 (cPair (car (cdr (cdr n))) (car (cdr (cdr (cdr n)))))) (car n)). rewrite <- a in H3. destruct x as [t t0| r t| f f0| f| n1 f]; simpl in H3; try match goal with | H:(cPair ?X1 _ = cPair ?X2 _) |- _ => cut (X1 = X2); [ intro I; discriminate I | eapply cPairInj1; apply H ] end. assert (H5: n1 = car (cdr (cdr n))). { eapply cPairInj1. eapply cPairInj2. apply H3. } assert (H6: codeFormula f = car (cdr (cdr (cdr n)))). { eapply cPairInj2. eapply cPairInj2. apply H3. } assert (H7: checkPrf (car (cdr (cdr (cdr n)))) (cdr (cdr (cdr (cdr n)))) <> 0). { unfold checkPrf; rewrite <- H6. rewrite (wellFormedFormulaCorrect1 L cL codeArityF codeArityFIsCorrect1 codeArityR codeArityRIsCorrect1). simpl; unfold checkPrfHelp; fold A; rewrite H6. rewrite cPairProjections. destruct (evalStrongRec 0 A (cdr (cdr (cdr n)))). rewrite Nat.mul_comm in H0. simpl in H0. assumption. discriminate. } assert (H8: cdr (cdr (cdr n)) < m). { apply Nat.lt_le_trans with n. assumption. rewrite H1; apply le_n. } induction (Hrecm _ H8 H7)as [x H9]. induction H9 as (x0, H9). induction H9 as (x1, H9). exists x0. rewrite <- H5 in H0. rewrite <- H9 in H0. assert (H10: checkPrf (codeFormula x) (codePrf x0 x x1) = S (codeList (map (codeFormula) x0))) by apply checkPrfCorrect1. unfold checkPrf in H10. rewrite (wellFormedFormulaCorrect1 L cL codeArityF codeArityFIsCorrect1 codeArityR codeArityRIsCorrect1) in H10. simpl in H10; unfold checkPrfHelp in H10; fold A in H10. rewrite H10 in H0. unfold pred in H0. rewrite codeFreeVarListFormulaCorrect in H0. rewrite codeInCorrect in H0. induction (In_dec eq_nat_dec n1 (freeVarListFormula L x0)). rewrite (Nat.mul_comm (S (codeList (map (codeFormula) x0)))) in H0. rewrite Nat.mul_comm in H0. simpl in H0. elim H0; reflexivity. rewrite <- H9 in H6. rewrite cPairProjections1 in H6. cut (cPair (codeFormula x) (codePrf x0 x x1) = cdr (cdr (cdr n))). { generalize x1. clear H10 H0 x1 H9. replace x with f. - intros x1 H0; exists (GEN L x0 f n1 b x1). simpl; rewrite H3. rewrite a. rewrite H0. rewrite H5. rewrite cPairProjections. rewrite H2. apply cPairProjections. - eapply (codeFormulaInj). eauto. } assumption. unfold charFunction in H0. rewrite nat_eqb_false in H0. elim H0. simpl; reflexivity. assumption. rewrite cPairProjections. assumption. ** destruct n1. *** simpl in H0. unfold checkPrfIMP1 in H0. repeat first [ rewrite cPairProjections1 in H0 | rewrite cPairProjections2 in H0 ]. exists (nil (A:=Formula)). rewrite <- H3 in H0. induction (eq_nat_dec (cPair 1 (cPair (car (cdr (cdr n))) (cPair 1 (cPair (cdr (cdr (cdr n))) (car (cdr (cdr n))))))) (codeFormula x)). destruct x as [t t0| r t| f f0| f| n1 f]; simpl in a; try match goal with | H:(cPair ?X1 _ = cPair ?X2 _) |- _ => cut (X1 = X2); [ intro I; discriminate I | eapply cPairInj1; apply H ] end. assert (H4: car (cdr (cdr n)) = codeFormula f). { eapply cPairInj1. eapply cPairInj2. apply a. } assert (H5: cPair 1 (cPair (cdr (cdr (cdr n))) (car (cdr (cdr n)))) = codeFormula f0). { eapply cPairInj2. eapply cPairInj2. apply a. } clear a. destruct f0 as [t t0| r t| f0 f1| f0| n1 f0]; simpl in H5; try match goal with | H:(cPair ?X1 _ = cPair ?X2 _) |- _ => cut (X1 = X2); [ intro I; discriminate I | eapply cPairInj1; apply H ] end. assert (H6:cdr (cdr (cdr n)) = codeFormula f0). { eapply cPairInj1; eapply cPairInj2. apply H5. } assert (H7: car (cdr (cdr n)) = codeFormula f1). { eapply cPairInj2. eapply cPairInj2. apply H5. } assert (H8: f1 = f). { eapply (codeFormulaInj). transitivity (car (cdr (cdr n))). symmetry in |- *. assumption. assumption. } rewrite H8; rewrite H8 in H3. exists (IMP1 L f f0). rewrite H3. simpl in |- *. rewrite <- H4. rewrite <- H6. rewrite cPairProjections. rewrite H2. apply cPairProjections. elim H0. unfold charFunction in |- *. rewrite nat_eqb_false. reflexivity. assumption. *** destruct n1. simpl in H0. unfold checkPrfIMP2 in H0. repeat first [ rewrite cPairProjections1 in H0 | rewrite cPairProjections2 in H0 ]. exists (nil (A:=Formula)). clear A. rewrite <- H3 in H0. rename x into f. induction (eq_nat_dec (cPair 1 (cPair (cPair 1 (cPair (car (cdr (cdr n))) (cPair 1 (cPair (car (cdr (cdr (cdr n)))) (cdr (cdr (cdr (cdr n)))))))) (cPair 1 (cPair (cPair 1 (cPair (car (cdr (cdr n))) (car (cdr (cdr (cdr n)))))) (cPair 1 (cPair (car (cdr (cdr n))) (cdr (cdr (cdr (cdr n)))))))))) (codeFormula f)). repeat match goal with | H:(cPair ?X1 (cPair ?X2 ?X3) = cPair ?X1 (cPair ?X4 ?X5)) |- _ => assert (X2 = X4); [ eapply cPairInj1; eapply cPairInj2; apply H | assert (X3 = X5); [ eapply cPairInj2; eapply cPairInj2; apply H | clear H ] ] | H:(cPair ?X1 (cPair _ _) = codeFormula ?X2) |- _ => destruct X2; simpl in H; try match goal with | J:(cPair ?X1 _ = cPair ?X2 _) |- _ => cut (X1 = X2); [ intro I; discriminate I | eapply cPairInj1; apply J ] end end. rewrite H3. replace f2_2_1 with f1_1. replace f1_2_2 with f2_2_2. replace f1_2_1 with f2_1_2. replace f2_1_1 with f1_1. exists (IMP2 L f1_1 f2_1_2 f2_2_2). simpl in |- *. rewrite <- H9. rewrite <- H8. rewrite cPairProjections. rewrite <- H6. rewrite cPairProjections. rewrite H2. apply cPairProjections. eapply (codeFormulaInj). transitivity (car (cdr (cdr n))); [ symmetry in |- *; assumption | assumption ]. eapply codeFormulaInj. transitivity (car (cdr (cdr (cdr n)))); [ symmetry in |- *; assumption | assumption ]. eapply (codeFormulaInj). transitivity (cdr (cdr (cdr (cdr n)))); [ symmetry in |- *; assumption | assumption ]. eapply (codeFormulaInj). transitivity (car (cdr (cdr n))); [ symmetry in |- *; assumption | assumption ]. elim H0. unfold charFunction in |- *. rewrite nat_eqb_false. reflexivity. assumption. destruct n1. simpl in H0. unfold checkPrfCP in H0. clear A. repeat first [ rewrite cPairProjections1 in H0 | rewrite cPairProjections2 in H0 ]. exists (nil (A:=Formula)). rewrite <- H3 in H0. rename x into f. induction (eq_nat_dec (cPair 1 (cPair (cPair 1 (cPair (cPair 2 (car (cdr (cdr n)))) (cPair 2 (cdr (cdr (cdr n)))))) (cPair 1 (cPair (cdr (cdr (cdr n))) (car (cdr (cdr n))))))) (codeFormula f)). repeat match goal with | H:(cPair 1 (cPair ?X2 ?X3) = cPair 1 (cPair ?X4 ?X5)) |- _ => assert (X2 = X4); [ eapply cPairInj1; eapply cPairInj2; apply H | assert (X3 = X5); [ eapply cPairInj2; eapply cPairInj2; apply H | clear H ] ] | H:(cPair 2 ?X2 = cPair 2 ?X4) |- _ => assert (X2 = X4); [ eapply cPairInj2; apply H | clear H ] | H:(cPair ?X1 _ = codeFormula ?X2) |- _ => destruct X2; simpl in H; try match goal with | J:(cPair ?X1 _ = cPair ?X2 _) |- _ => cut (X1 = X2); [ intro I; discriminate I | eapply cPairInj1; apply J ] end end. rewrite H3. replace f2_2 with f1_1. replace f1_2 with f2_1. exists (CP L f1_1 f2_1). simpl in |- *. rewrite <- H8. rewrite <- H6. rewrite cPairProjections. rewrite H2. apply cPairProjections. eapply codeFormulaInj. transitivity (cdr (cdr (cdr n))); [ symmetry in |- *; assumption | assumption ]. eapply codeFormulaInj. transitivity (car (cdr (cdr n))); [ symmetry in |- *; assumption | assumption ]. elim H0. unfold charFunction in |- *. rewrite nat_eqb_false. reflexivity. assumption. destruct n1. simpl in H0. unfold checkPrfFA1 in H0. clear A. repeat first [ rewrite cPairProjections1 in H0 | rewrite cPairProjections2 in H0 ]. exists (nil (A:=Formula)). rewrite <- H3 in H0. rename x into f. induction (eq_nat_dec (cPair 1 (cPair (cPair 3 (cPair (car (cdr (cdr (cdr n)))) (car (cdr (cdr n))))) (codeSubFormula (car (cdr (cdr n))) (car (cdr (cdr (cdr n)))) (cdr (cdr (cdr (cdr n))))))) (codeFormula f)). repeat match goal with | H:(cPair 1 (cPair ?X2 ?X3) = cPair 1 (cPair ?X4 ?X5)) |- _ => assert (X2 = X4); [ eapply cPairInj1; eapply cPairInj2; apply H | assert (X3 = X5); [ eapply cPairInj2; eapply cPairInj2; apply H | clear H ] ] | H:(cPair 3 (cPair ?X2 ?X3) = cPair 3 (cPair ?X4 ?X5)) |- _ => assert (X2 = X4); [ eapply cPairInj1; eapply cPairInj2; apply H | assert (X3 = X5); [ eapply cPairInj2; eapply cPairInj2; apply H | clear H ] ] | H:(cPair ?X1 _ = codeFormula ?X2) |- _ => destruct X2; simpl in H; try match goal with | J:(cPair ?X1 _ = cPair ?X2 _) |- _ => cut (X1 = X2); [ intro I; discriminate I | eapply cPairInj1; apply J ] end end. rewrite H3. rewrite H6 in H5. rewrite H7 in H5. assert (H4: wellFormedTerm (cdr (cdr (cdr (cdr n)))) <> 0). { eapply multLemma1. apply H0. } induction (wellFormedTermCorrect2 L cL codeArityF codeArityFIsCorrect1 codeArityFIsCorrect2 _ H4). rewrite <- H8 in H5. rewrite codeSubFormulaCorrect in H5. replace f2 with (substF f1 n1 x). exists (FA1 L f1 n1 x). simpl in |- *. rewrite <- H7. rewrite <- H6. rewrite H8. repeat rewrite cPairProjections. rewrite H2. apply cPairProjections. eapply codeFormulaInj. assumption. elim H0. unfold charFunction in |- *. rewrite nat_eqb_false. rewrite Nat.mul_comm. reflexivity. assumption. destruct n1. simpl in H0. unfold checkPrfFA2 in H0. clear A. repeat first [ rewrite cPairProjections1 in H0 | rewrite cPairProjections2 in H0 ]. exists (nil (A:=Formula)). rewrite <- H3 in H0. rename x into f. induction (eq_nat_dec (cPair 1 (cPair (car (cdr (cdr n))) (cPair 3 (cPair (cdr (cdr (cdr n))) (car (cdr (cdr n))))))) (codeFormula f)). repeat match goal with | H:(cPair 1 (cPair ?X2 ?X3) = cPair 1 (cPair ?X4 ?X5)) |- _ => assert (X2 = X4); [ eapply cPairInj1; eapply cPairInj2; apply H | assert (X3 = X5); [ eapply cPairInj2; eapply cPairInj2; apply H | clear H ] ] | H:(cPair 3 (cPair ?X2 ?X3) = cPair 3 (cPair ?X4 ?X5)) |- _ => assert (X2 = X4); [ eapply cPairInj1; eapply cPairInj2; apply H | assert (X3 = X5); [ eapply cPairInj2; eapply cPairInj2; apply H | clear H ] ] | H:(cPair ?X1 _ = codeFormula ?X2) |- _ => destruct X2; simpl in H; try match goal with | J:(cPair ?X1 _ = cPair ?X2 _) |- _ => cut (X1 = X2); [ intro I; discriminate I | eapply cPairInj1; apply J ] end end. rewrite H3. replace f2 with f1. rewrite H6 in H0. rewrite H4 in H0. rewrite codeFreeVarFormulaCorrect in H0. rewrite codeInCorrect in H0. induction (In_dec eq_nat_dec n1 (freeVarF f1)). elim H0. reflexivity. exists (FA2 L f1 n1 b). simpl in |- *. rewrite <- H4. rewrite <- H6. rewrite cPairProjections. rewrite H2. apply cPairProjections. eapply codeFormulaInj. transitivity (car (cdr (cdr n))); [ symmetry in |- *; assumption | assumption ]. elim H0. unfold charFunction in |- *. rewrite nat_eqb_false. rewrite Nat.mul_comm. reflexivity. assumption. destruct n1. simpl in H0. unfold checkPrfFA3 in H0. clear A. repeat first [ rewrite cPairProjections1 in H0 | rewrite cPairProjections2 in H0 ]. exists (nil (A:=Formula)). rewrite <- H3 in H0. rename x into f. induction (eq_nat_dec (cPair 1 (cPair (cPair 3 (cPair (cdr (cdr (cdr (cdr n)))) (cPair 1 (cPair (car (cdr (cdr n))) (car (cdr (cdr (cdr n)))))))) (cPair 1 (cPair (cPair 3 (cPair (cdr (cdr (cdr (cdr n)))) (car (cdr (cdr n))))) (cPair 3 (cPair (cdr (cdr (cdr (cdr n)))) (car (cdr (cdr (cdr n)))))))))) (codeFormula f)). repeat match goal with | H:(cPair 1 (cPair ?X2 ?X3) = cPair 1 (cPair ?X4 ?X5)) |- _ => assert (X2 = X4); [ eapply cPairInj1; eapply cPairInj2; apply H | assert (X3 = X5); [ eapply cPairInj2; eapply cPairInj2; apply H | clear H ] ] | H:(cPair 3 (cPair ?X2 ?X3) = cPair 3 (cPair ?X4 ?X5)) |- _ => assert (X2 = X4); [ eapply cPairInj1; eapply cPairInj2; apply H | assert (X3 = X5); [ eapply cPairInj2; eapply cPairInj2; apply H | clear H ] ] | H:(cPair ?X1 _ = codeFormula ?X2) |- _ => destruct X2; simpl in H; try match goal with | J:(cPair ?X1 _ = cPair ?X2 _) |- _ => cut (X1 = X2); [ intro I; discriminate I | eapply cPairInj1; apply J ] end end. rewrite H3. replace f2_1 with f1_1. replace f1_2 with f2_2. replace n3 with n1. replace n2 with n1. exists (FA3 L f1_1 f2_2 n1). simpl in |- *. rewrite <- H4. rewrite <- H8. rewrite <- H5. repeat rewrite cPairProjections. rewrite H2. apply cPairProjections. transitivity (cdr (cdr (cdr (cdr n)))); [ symmetry in |- *; assumption | assumption ]. transitivity (cdr (cdr (cdr (cdr n)))); [ symmetry in |- *; assumption | assumption ]. eapply codeFormulaInj. transitivity (car (cdr (cdr (cdr n)))); [ symmetry in |- *; assumption | assumption ]. eapply codeFormulaInj. transitivity (car (cdr (cdr n))); [ symmetry in |- *; assumption | assumption ]. elim H0. unfold charFunction in |- *. rewrite nat_eqb_false. reflexivity. assumption. destruct n1. simpl in H0. unfold checkPrfEQ1 in H0. clear A. exists (nil (A:=Formula)). rewrite <- H3 in H0. induction (eq_nat_dec (codeFormula (equal (var 0) (var 0))) (codeFormula x)). rewrite H3. replace x with (@equal L (var 0) (var 0)). exists (EQ1 L). simpl in |- *. induction (eq_nat_dec (cdr (cdr n)) 0). rewrite a0 in H2. rewrite H2. apply cPairProjections. elim H0. unfold charFunction in |- *. rewrite nat_eqb_false. reflexivity. rewrite cPairProjections2. assumption. eapply codeFormulaInj. assumption. elim H0. unfold charFunction in |- *. rewrite (nat_eqb_false (codeFormula (equal (var 0) (var 0)))). rewrite Nat.mul_comm. reflexivity. rewrite cPairProjections1. assumption. destruct n1. simpl in H0. unfold checkPrfEQ2 in H0. clear A. exists (nil (A:=Formula)). rewrite <- H3 in H0. induction (eq_nat_dec (codeFormula (impH (equal (var 0) (var 1)) (equal (var 1) (var 0)))) (codeFormula x)). rewrite H3. replace x with (@impH L (equal (var 0) (var 1)) (equal (var 1) (var 0))). exists (EQ2 L). simpl in |- *. induction (eq_nat_dec (cdr (cdr n)) 0). rewrite a0 in H2. rewrite H2. apply cPairProjections. elim H0. unfold charFunction in |- *. rewrite nat_eqb_false. reflexivity. rewrite cPairProjections2. assumption. eapply codeFormulaInj. assumption. elim H0. unfold charFunction in |- *. rewrite (nat_eqb_false (codeFormula (v#0 = v#1 -> v#1 = v#0)%fol)). rewrite Nat.mul_comm. reflexivity. rewrite cPairProjections1. assumption. repeat rewrite <- pred_Sn in H0. assert (H4 : forall n2 p q : nat, switchPR (S n2) p q = p). simple destruct n2; trivial. repeat rewrite H4 in H0. clear H4. destruct n1. simpl in H0. unfold checkPrfEQ3 in H0. clear A. exists (nil (A:=Formula)). rewrite <- H3 in H0. induction (eq_nat_dec (codeFormula (impH (equal (var 0) (var 1)) (impH (equal (var 1) (var 2)) (equal (var 0) (var 2))))) (codeFormula x)). rewrite H3. replace x with (@impH L (equal (var 0) (var 1)) (impH (equal (var 1) (var 2)) (equal (var 0) (var 2)))). exists (EQ3 L). simpl in |- *. rewrite cPairProjections2 in H0. rewrite cPairProjections1 in H0. induction (eq_nat_dec (cdr (cdr n)) 0). rewrite a0 in H2. rewrite H2. apply cPairProjections. elim H0. unfold charFunction in |- *. rewrite nat_eqb_false. reflexivity. assumption. eapply codeFormulaInj. assumption. elim H0. unfold charFunction in |- *. rewrite (nat_eqb_false (codeFormula (impH (equal (var 0) (var 1)) (impH (equal (var 1) (var 2)) (equal (var 0) (var 2)))))) . rewrite Nat.mul_comm. reflexivity. rewrite cPairProjections1. assumption. destruct n1. simpl in H0. unfold checkPrfEQ4 in H0. clear A. repeat rewrite cPairProjections2 in H0. repeat rewrite cPairProjections1 in H0. exists (nil (A:=Formula)). rewrite <- H3 in H0. assert (codeArityR (cdr (cdr n)) <> 0). unfold notZero in H0. unfold not in |- *; intros. rewrite H4 in H0. apply H0. reflexivity. induction (codeArityRIsCorrect2 _ H4). rewrite <- H5 in H0. rewrite codeArityRIsCorrect1 in H0. simpl in H0. induction (codeNVarsCorrect (arityR L x0)). rewrite H6 in H0. rewrite H7 in H0. clear H6 H7. assert (codeIff (cPair (S (S (S (S (cr x0))))) (codeTerms (fst (nVars L (arityR L x0))))) (cPair (S (S (S (S (cr x0))))) (codeTerms (snd (nVars L (arityR L x0))))) = codeIff (codeFormula (atomic x0 (fst (nVars L (arityR L x0))))) (codeFormula (atomic x0 (snd (nVars L (arityR L x0)))))). reflexivity. rewrite H6 in H0. clear H6. rewrite codeIffCorrect in H0. assert (AxmEq4 L x0 = x). clear H5. unfold AxmEq4 in |- *. induction (nVars L (arityR L x0)). simpl in |- *. unfold fst, snd in H0. cut ((if Nat.eqb (codeAxmEqHelp (arityR L x0) (codeFormula (iffH (atomic x0 a) (atomic x0 b)))) (codeFormula x) then 1 else 0) + 0 <> 0). { generalize (iffH (atomic x0 a) (atomic x0 b)). intros f H5. clear H0. clear a b. cut (codeAxmEqHelp (arityR L x0) (codeFormula f) = codeFormula x). { generalize x. clear H5. induction (arityR L x0); simpl in |- *; intros. eapply codeFormulaInj; assumption. rename x1 into f0. repeat match goal with | H:(cPair 1 (cPair ?X2 ?X3) = cPair 1 (cPair ?X4 ?X5)) |- _ => assert (X2 = X4); [ eapply cPairInj1; eapply cPairInj2; apply H | assert (X3 = X5); [ eapply cPairInj2; eapply cPairInj2; apply H | clear H ] ] | H:(cPair 0 (cPair ?X2 ?X3) = cPair 0 (cPair ?X4 ?X5)) |- _ => assert (X2 = X4); [ eapply cPairInj1; eapply cPairInj2; apply H | assert (X3 = X5); [ eapply cPairInj2; eapply cPairInj2; apply H | clear H ] ] | H:(cPair ?X1 _ = codeFormula ?X2) |- _ => destruct X2; simpl in H; try match goal with | J:(cPair ?X1 _ = cPair ?X2 _) |- _ => cut (X1 = X2); [ intro I; discriminate I | eapply cPairInj1; apply J ] end end. rewrite (IHn1 f0_2). destruct t. replace n2 with (n1 + n1). destruct t0. replace n3 with (S (n1 + n1)). reflexivity. apply cPairInj2 with 0 0. apply H7. elim O_S with (cf f0). apply cPairInj1 with (S (n1 + n1)) (codeTerms t). apply H7. apply cPairInj2 with 0 0. apply H0. elim O_S with (cf f0). apply cPairInj1 with (n1 + n1) (codeTerms t). apply H0. assumption. } induction (eq_nat_dec (codeAxmEqHelp (arityR L x0) (codeFormula f)) (codeFormula x)). assumption. elim H5. rewrite nat_eqb_false. reflexivity. assumption. } assumption. rewrite H3. rewrite <- H6. exists (EQ4 L x0). simpl in |- *. unfold codeR. rewrite H5. rewrite H2. apply cPairProjections. destruct n1. simpl in H0. unfold checkPrfEQ5 in H0. clear A. repeat rewrite cPairProjections2 in H0. repeat rewrite cPairProjections1 in H0. exists (nil (A:=Formula)). rewrite <- H3 in H0. assert (codeArityF (cdr (cdr n)) <> 0). unfold notZero in H0. unfold not in |- *; intros. rewrite H4 in H0. apply H0. reflexivity. induction (codeArityFIsCorrect2 _ H4). rewrite <- H5 in H0. rewrite codeArityFIsCorrect1 in H0. simpl in H0. induction (codeNVarsCorrect (arityF L x0)). rewrite H6 in H0. rewrite H7 in H0. clear H6 H7. assert (cPair 0 (cPair (cPair (S (cf x0)) (codeTerms (fst (nVars L (arityF L x0))))) (cPair (S (cf x0)) (codeTerms (snd (nVars L (arityF L x0)))))) = codeFormula (equal (apply x0 (fst (nVars L (arityF L x0)))) (apply x0 (snd (nVars L (arityF L x0)))))). reflexivity. rewrite H6 in H0. clear H6. assert (AxmEq5 L x0 = x). clear H5. unfold AxmEq5 in |- *. induction (nVars L (arityF L x0)). simpl in |- *. unfold fst, snd in H0. cut ((if Nat.eqb (codeAxmEqHelp (arityF L x0) (codeFormula (equal (apply x0 a) (apply x0 b)))) (codeFormula x) then 1 else 0) + 0 <> 0). { generalize (equal (apply x0 a) (apply x0 b)). intros. clear H0. clear a b. cut (codeAxmEqHelp (arityF L x0) (codeFormula f) = codeFormula x). generalize x. clear H5. induction (arityF L x0); simpl in |- *; intros. eapply codeFormulaInj. assumption. repeat match goal with | H:(cPair 1 (cPair ?X2 ?X3) = cPair 1 (cPair ?X4 ?X5)) |- _ => assert (X2 = X4); [ eapply cPairInj1; eapply cPairInj2; apply H | assert (X3 = X5); [ eapply cPairInj2; eapply cPairInj2; apply H | clear H ] ] | H:(cPair 0 (cPair ?X2 ?X3) = cPair 0 (cPair ?X4 ?X5)) |- _ => assert (X2 = X4); [ eapply cPairInj1; eapply cPairInj2; apply H | assert (X3 = X5); [ eapply cPairInj2; eapply cPairInj2; apply H | clear H ] ] | H:(cPair ?X1 _ = codeFormula ?X2) |- _ => destruct X2; simpl in H; try match goal with | J:(cPair ?X1 _ = cPair ?X2 _) |- _ => cut (X1 = X2); [ intro I; discriminate I | eapply cPairInj1; apply J ] end end. rewrite (IHn1 x1_2). destruct t. replace n2 with (n1 + n1). destruct t0. replace n3 with (S (n1 + n1)). reflexivity. apply cPairInj2 with 0 0. apply H7. elim O_S with (cf f0). apply cPairInj1 with (S (n1 + n1)) (codeTerms t). apply H7. apply cPairInj2 with 0 0. apply H0. elim O_S with (cf f0). apply cPairInj1 with (n1 + n1) (codeTerms t). apply H0. assumption. induction (eq_nat_dec (codeAxmEqHelp (arityF L x0) (codeFormula f)) (codeFormula x)). assumption. elim H5. rewrite nat_eqb_false. reflexivity. assumption. } { assumption. } rewrite H3. rewrite <- H6. exists (EQ5 L x0). simpl in |- *. unfold codeF. rewrite H5. rewrite H2. apply cPairProjections. elim H0. simpl in |- *. reflexivity. } intros n m H0. assert (H1: exists f : Formula, (exists l : list Formula, (exists p : Prf l f, cPair (codeFormula f) (codePrf l f p) = cPair n m))). { eapply H. apply Nat.lt_succ_diag_r. rewrite cPairProjections1. rewrite cPairProjections2. assumption. } decompose record H1 /r; intros x x0 x1 H2; exists x; split. - eapply cPairInj1. apply H2. - exists x0, x1; eapply cPairInj2; apply H2. Qed.
imports: Coq(Arith Lia) hydras.Ackermann(primRec codeFreeVar codeSubFormula cPair code folProp extEqualNat wellFormed folProof prLogic) hydras(Compat815)