proposition: Remark primRecSigmaRepresentable : forall (n : nat) (A : Formula) (g : naryFunc n), Representable n g A -> forall (B : Formula) (h : naryFunc (S (S n))), Representable n.+2 h B -> Representable (S n) (evalPrimRecFunc n g h) (primRecSigmaFormula n A B).
proof: Proof. assert (H: forall (n : nat) (A : Formula) (g : naryFunc n), Representable n g A -> forall (B : Formula) (h : naryFunc (S (S n))), Representable (S (S n)) h B -> RepresentableHelp (S n) (evalPrimRecFunc n g h) (primRecSigmaFormula n A B)). { induction n as [| n Hrecn]. - simpl; intros A g H B h H0. unfold primRecSigmaFormula. intros a. rewrite (subFormulaExist LNN). induction (In_dec eq_nat_dec 2 (freeVarT (n2t a))) as [a0 | b]. + elim (closedNatToTerm _ _ a0). + simpl. clear b. assert (repBeta : Representable 2 β βR). { apply betaRepresentable. } rewrite (subFormulaAnd LNN). repeat rewrite (subFormulaId LNN). apply iffTrans with (existH 2 (andH (minimize (substF (primRecSigmaFormulaHelp 0 A B) 1 (n2t a)) (substF (primRecPiFormulaHelp 0 A B) 1 (n2t a)) 2 4) (substF βR 1 (n2t a)))). * apply (reduceExist LNN). -- apply closedNN. -- apply (reduceAnd LNN). ++ apply subFormulaMinimize; first [ discriminate | apply closedNatToTerm ]. ++ apply iffRefl. * set (f := evalPrimRecFunc 0 g h) in *. destruct (betaTheorem1 (S a) f) as [x p]. destruct x as (a0, b). simpl in p. set (P := fun c : nat => forall z : nat, z < S a -> f z = β c z) in *. assert (H1: forall c : nat, decidable (P c)). { intros c. unfold decidable, P. set (Q := fun z : nat => f z <> β c z) in *. assert (H1: forall z : nat, decidable (Q z)). { intros. unfold decidable, Q. destruct (eq_nat_dec (f z) (β c z)); auto. } destruct (boundedCheck Q H1 (S a)) as [H2 | H2]. - left. unfold Q in H2. intros z H3. destruct (eq_nat_dec (f z) (β c z)). + auto. + elim (H2 z); auto. - right. intro H3. destruct H2 as (x, H2). destruct H2 as (H2, H4). elim H4. apply H3; auto. } induction (smallestExists P H1 (cPair b a0)). -- destruct H2 as (H2, H3). clear H1 p b a0. apply iffTrans with (existH 2 (andH (equal (var 2) (n2t x)) (substF βR 1 (n2t a)))). ++ apply (reduceExist LNN). ** apply closedNN. ** apply (reduceAnd LNN). --- assert (subExistSpecial : forall (F : Formula) (a b c : nat), b <> c -> substF (existH b F) c (n2t a) = existH b (substF F c (n2t a))). { intros F a0 b c H1. rewrite (subFormulaExist LNN). destruct (eq_nat_dec b c) as [e | e]. - elim H1. auto. - destruct (In_dec eq_nat_dec b (freeVarT (n2t a0))) as [H4 | H4]. + elim (closedNatToTerm _ _ H4). + reflexivity. } assert (subForallSpecial : forall (F : Formula) (a b c : nat), b <> c -> substF (forallH b F) c (n2t a) = forallH b (substF F c (n2t a))). { intros F a0 b c H1. rewrite (subFormulaForall LNN). destruct (eq_nat_dec b c) as [e | e]. - elim H1. auto. - destruct (In_dec eq_nat_dec b (freeVarT (n2t a0))) as [e0 | e0]. + elim (closedNatToTerm _ _ e0). + reflexivity. } apply minimize1. +++ discriminate. +++ intro H1. destruct (freeVarSubFormula3 _ _ _ _ _ H1) as [H4 | H4]. *** assert (H5: In 4 (freeVarF (primRecPiFormulaHelp 0 A B))). { eapply in_remove. apply H4. } decompose sum (freeVarPrimRecPiFormulaHelp1 _ _ _ _ H5) /r. ---- intro H6; destruct H as (H, H7). elim (proj1 (Nat.le_ngt 4 0)). ++++ apply H. apply H6. ++++ repeat constructor. ---- intro H7; destruct H0 as (H0, H6). elim (proj1 (Nat.le_ngt 4 2)). ++++ apply H0. apply H7. ++++ repeat constructor. ---- discriminate 1. ---- discriminate 1. *** elim (closedNatToTerm _ _ H4). +++ unfold primRecSigmaFormulaHelp. repeat first [ rewrite subExistSpecial; [| discriminate ] | rewrite subForallSpecial; [| discriminate ] | rewrite (subFormulaAnd LNN) | rewrite (subFormulaImp LNN) ]. rewrite (subFormulaExist LNN). simpl. repeat first [ rewrite subExistSpecial; [| discriminate ] | rewrite subForallSpecial; [| discriminate ] | rewrite (subFormulaAnd LNN) | rewrite (subFormulaImp LNN) ]. apply andI. *** apply existI with (n2t (f 0)). rewrite (subFormulaAnd LNN). apply andI. ---- unfold f, evalPrimRecFunc. destruct H as (H, H1). simpl in H1. apply impE with (substF A 0 (n2t g)). ++++ apply iffE2. apply (reduceSub LNN). **** apply closedNN. **** apply iffTrans with (substF A 2 (n2t x)). apply (reduceSub LNN). { apply closedNN. } { apply (subFormulaNil LNN). intro H4. elim (proj1 (Nat.le_ngt 1 0)). - apply H; auto. - auto. } { apply (subFormulaNil LNN). intro H4. elim (proj1 (Nat.le_ngt 2 0)). - apply H; auto. - auto. } ++++ apply impE with (substF (equal (var 0) (n2t g)) 0 (n2t g)). **** apply iffE2. apply (reduceSub LNN). { apply closedNN. } { auto. } **** rewrite (subFormulaEqual LNN). simpl. rewrite (subTermNil LNN). { apply eqRefl. } { apply closedNatToTerm. } ---- destruct repBeta as (H1, H4). simpl in H4. rewrite (subFormulaId LNN). apply impE with (substF3 βR 1 Zero 2 (n2t x) 0 (n2t (f 0))). ++++ apply iffE2; apply (reduceSub LNN). **** apply closedNN. **** apply (reduceSub LNN). { apply closedNN. } { apply (subFormulaNil LNN). intro H5. destruct (freeVarSubFormula3 _ _ _ _ _ H5) as [H6 | H6]. - elim (in_remove_neq _ _ _ _ _ H6). reflexivity. - elim H6. } ++++ apply impE with (substF (v#0 = n2t (β x 0))%fol 0 (n2t (f 0))). **** apply iffE2, (reduceSub LNN). { apply closedNN. } { apply iffTrans with (substF2 βR 2 (n2t x) 1 (n2t 0)). - apply (subFormulaExch LNN). + discriminate. + apply closedNatToTerm. + apply closedNatToTerm. - apply H4. } **** rewrite (subFormulaEqual LNN). simpl; rewrite (subTermNil LNN). { rewrite H2; [apply eqRefl | apply Nat.lt_0_succ]. } { apply closedNatToTerm. } *** apply forallI. ---- apply closedNN. ---- apply impTrans with (v#3 < n2t a)%fol. ++++ unfold LT at 1. repeat rewrite (subFormulaRelation LNN). simpl. rewrite (subTermNil LNN). **** apply impRefl. **** apply closedNatToTerm. ++++ apply boundedLT. intros n H1. repeat rewrite (subFormulaId LNN). repeat first [ rewrite subExistSpecial; [| discriminate ] | rewrite subForallSpecial; [| discriminate ] | rewrite (subFormulaAnd LNN) | rewrite (subFormulaImp LNN) ]. apply existI with (n2t (f (S n))). repeat first [ rewrite subExistSpecial; [| discriminate ] | rewrite subForallSpecial; [| discriminate ] | rewrite (subFormulaAnd LNN) | rewrite (subFormulaImp LNN) ]. apply existI with (n2t (f n)). repeat first [ rewrite subExistSpecial; [| discriminate ] | rewrite subForallSpecial; [| discriminate ] | rewrite (subFormulaAnd LNN) | rewrite (subFormulaImp LNN) ]. apply andI. **** destruct repBeta as (H4, H5). simpl in H5. apply impE with (substF6 βR 1 (var 3) 2 (n2t x) 0 (var 1) 3 (n2t n) 0 (n2t (f n.+1)) 1 (n2t (f n))). { apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). - discriminate. - apply closedNatToTerm. - intro H6. induction H6 as [H6 | H6]. + discriminate H6. + elim H6. } { apply impE with (substF6 βR 1 (var 3) 2 (n2t x) 3 (n2t n) 0 (var 1) 0 (n2t (f n.+1)) 1 (n2t (f n))). - apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). + discriminate. + apply closedNatToTerm. + intros [H6 | H6]. * discriminate H6. * elim H6. - apply impE with (substF5 βR 1 (var 3) 2 (n2t x) 3 (n2t n) 0 (var 1) 1 (n2t (f n))). + apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN). intro H6. destruct (freeVarSubFormula3 _ _ _ _ _ H6) as [H7 | H7]. * elim (in_remove_neq _ _ _ _ _ H7). reflexivity. * destruct H7 as [H7 | H7]. -- discriminate H7. -- elim H7. + apply impE with (substF5 βR 2 (n2t x) 1 (var 3) 3 (n2t n) 0 (var 1) 1 (n2t (f n))). * apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). -- discriminate. -- intro H6. destruct H6 as [H6 | H6]. ++ discriminate H6. ++ elim H6. -- apply closedNatToTerm. * apply impE with (substF4 βR 2 (n2t x) 1 (n2t n) 0 (var 1) 1 (n2t (f n))). -- apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN). intro H6. assert (H7: In 3 (freeVarF (substF βR 2 (n2t x)))). { eapply in_remove. apply H6. } destruct (freeVarSubFormula3 _ _ _ _ _ H7) as [H8 | H8]. ++ elim (proj1 (Nat.le_ngt 3 2)). ** apply H4. eapply in_remove. apply H8. ** repeat constructor. ++ elim (closedNatToTerm _ _ H8). -- apply impE with (substF2 (v#0 = n2t (β x n))%fol 0 (var 1) 1 (n2t (f n))). ++ apply iffE2;repeat (apply (reduceSub LNN); [ apply closedNN |]). apply H5. ++ repeat rewrite (subFormulaEqual LNN). simpl. repeat rewrite (subTermNil LNN (n2t (β x n))). ** rewrite H2. apply eqRefl. apply Nat.lt_lt_succ_r. apply H1. ** apply closedNatToTerm. ** apply closedNatToTerm. } **** apply andI. { destruct H0 as (H0, H4). simpl in H4. apply impE with (substF4 B 2 (var 3) 3 (n2t n) 0 (n2t (f (S n))) 1 (n2t (f n))). - apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN). intro H5. destruct (freeVarSubFormula3 _ _ _ _ _ H5) as [H6 | [H6 | H6]]. + elim (in_remove_neq _ _ _ _ _ H6). reflexivity. + discriminate H6. + elim H6. - apply impE with (substF3 B 2 (n2t n) 0 (n2t (f (S n))) 1 (n2t (f n))). + apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN). intro H5. elim (proj1 (Nat.le_ngt 3 2)). * apply H0. eapply in_remove. apply H5. * repeat constructor. + apply impE with (substF3 B 2 (n2t n) 1 (n2t (f n)) 0 (n2t (f (S n)))). * apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). -- discriminate. -- apply closedNatToTerm. -- apply closedNatToTerm. * apply impE with (substF (equal (var 0) (n2t (h n (f n)))) 0 (n2t (f (S n)))). -- apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply H4. -- rewrite (subFormulaEqual LNN). simpl. rewrite (subTermNil LNN). ++ unfold f. simpl. apply eqRefl. ++ apply closedNatToTerm. } { apply impE with (substF5 βR 2 (n2t x) 1 (Succ (var 3)) 3 (n2t n) 0 (n2t (f (S n))) 1 (n2t (f n))). - apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). + discriminate. + simpl. intro H4. lia. + apply closedNatToTerm. - apply impE with (substF5 βR 2 (n2t x) 3 (n2t n) 1 (n2t (S n)) 0 (n2t (f (S n))) 1 (n2t (f n))). + apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]). replace (n2t (S n)) with (substT (Succ (var 3)) 3 (n2t n)). * apply (subSubFormula LNN). -- discriminate. -- apply closedNatToTerm. * simpl. reflexivity. + destruct repBeta as (H4, H5). apply impE with (substF4 βR 2 (n2t x) 1 (n2t (S n)) 0 (n2t (f (S n))) 1 (n2t (f n))). * apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN). intro H6. destruct (freeVarSubFormula3 _ _ _ _ _ H6) as [H7 | H7]. -- elim (proj1 (Nat.le_ngt 3 2)). ++ apply H4. eapply in_remove. apply H7. ++ repeat constructor. -- elim (closedNatToTerm _ _ H7). * simpl in H5. apply impE with (substF2 (equal (var 0) (n2t (β x (S n)))) 0 (n2t (f (S n))) 1 (n2t (f n))). -- apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply H5. -- repeat rewrite (subFormulaEqual LNN). simpl. repeat (rewrite (subTermNil LNN (n2t (β x (S n)))); [| apply closedNatToTerm ]). rewrite (subTermNil LNN). ++ rewrite H2. ** apply eqRefl. ** apply (proj1 (Nat.succ_lt_mono n a)). apply H1. ++ apply closedNatToTerm. } +++ unfold primRecPiFormulaHelp. repeat first [ rewrite subExistSpecial; [| discriminate ] | rewrite subForallSpecial; [| discriminate ] | rewrite (subFormulaAnd LNN) | rewrite (subFormulaImp LNN) ]. rewrite (subFormulaForall LNN). simpl. repeat first [ rewrite subExistSpecial; [| discriminate ] | rewrite subForallSpecial; [| discriminate ] | rewrite (subFormulaAnd LNN) | rewrite (subFormulaImp LNN) ]. apply andI. *** apply forallI. ---- apply closedNN. ---- destruct H as (H, H1). simpl in H1. apply impTrans with (substF2 (equal (var 0) (n2t g)) 1 (n2t a) 2 (n2t x)). ++++ apply iffE1. apply (reduceSub LNN). **** apply closedNN. **** apply (reduceSub LNN). { apply closedNN. } { apply H1. } ++++ repeat rewrite (subFormulaEqual LNN). simpl. repeat (rewrite (subTermNil LNN (n2t g)); [| apply closedNatToTerm ]). apply impI. rewrite <- (subFormulaId LNN (substF4 βR 1 Zero 2 (var 2) 1 (n2t a) 2 (n2t x)) 0). apply impE with (substF (substF (substF (substF (substF βR 1 Zero) 2 (var 2)) 1 (n2t a)) 2 (n2t x)) 0 (n2t g)). **** apply (subWithEquals LNN). apply eqSym. apply Axm; right; constructor. **** apply sysWeaken. clear H1. destruct repBeta as (H1, H4). simpl in H4. rewrite (subFormulaId LNN). apply impE with (substF3 βR 1 Zero 2 (n2t x) 0 (n2t (f 0))). { apply iffE2. apply (reduceSub LNN). - apply closedNN. - apply (reduceSub LNN). apply closedNN. apply (subFormulaNil LNN). intro H5. destruct (freeVarSubFormula3 _ _ _ _ _ H5) as [H6 | H6]. + elim (in_remove_neq _ _ _ _ _ H6). reflexivity. + elim H6. } { apply impE with (substF (equal (var 0) (n2t (β x 0))) 0 (n2t (f 0))). - apply iffE2. apply (reduceSub LNN). + apply closedNN. + apply iffTrans with (substF2 βR 2 (n2t x) 1 (n2t 0)). * apply (subFormulaExch LNN). -- discriminate. -- apply closedNatToTerm. -- apply closedNatToTerm. * apply H4. - rewrite (subFormulaEqual LNN). simpl. rewrite (subTermNil LNN). + rewrite H2. apply eqRefl. apply Nat.lt_0_succ. + apply closedNatToTerm. } *** apply forallI. ---- apply closedNN. ---- apply impTrans with (LT (var 3) (n2t a)). ++++ unfold LT at 1. repeat rewrite (subFormulaRelation LNN). simpl. rewrite (subTermNil LNN). **** apply impRefl. **** apply closedNatToTerm. ++++ apply boundedLT. intros n H1. repeat rewrite (subFormulaId LNN). repeat first [ rewrite subExistSpecial; [| discriminate ] | rewrite subForallSpecial; [| discriminate ] | rewrite (subFormulaAnd LNN) | rewrite (subFormulaImp LNN) ]. apply forallI. **** apply closedNN. **** apply forallI. { apply closedNN. } { apply impTrans with (equal (var 1) (n2t (f n))). - destruct repBeta as (H4, H5). simpl in H5. apply impTrans with (substF4 βR 1 (var 3) 2 (n2t x) 0 (var 1) 3 (n2t n)). apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN |]). + apply (subFormulaExch LNN). * discriminate. * intro H6. destruct H6 as [H6 | H6]. -- discriminate H6. -- elim H6. * apply closedNatToTerm. + apply impTrans with (substF4 βR 1 (var 3) 2 (n2t x) 3 (n2t n) 0 (var 1)). * apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). -- discriminate. -- intro H6. destruct H6 as [H6 | H6]. ++ discriminate H6. ++ elim H6. -- apply closedNatToTerm. * apply impTrans with (substF4 βR 2 (n2t x) 1 (var 3) 3 (n2t n) 0 (var 1)). -- apply iffE2; repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). ++ discriminate. ++ apply closedNatToTerm. ++ intro H6. destruct H6 as [H6 | H6]. ** discriminate H6. ** elim H6. -- apply impTrans with (substF3 βR 2 (n2t x) 1 (n2t n) 0 (var 1)). ++ apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN). intro H6. assert (H7: In 3 (freeVarF (substF βR 2 (n2t x)))). { eapply in_remove. apply H6. } destruct (freeVarSubFormula3 _ _ _ _ _ H7) as [H8 | H8]. ** elim (proj1 (Nat.le_ngt 3 2)). apply H4. eapply in_remove. --- apply H8. --- repeat constructor. ** elim (closedNatToTerm _ _ H8). ++ apply impTrans with (substF (equal (var 0) (n2t (β x n))) 0 (var 1)). ** apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply H5. ** repeat rewrite (subFormulaEqual LNN). simpl. repeat rewrite (subTermNil LNN (n2t (β x n))). --- rewrite H2. +++ apply impRefl. +++ apply Nat.lt_lt_succ_r. apply H1. --- apply closedNatToTerm. - rewrite <- (subFormulaId LNN (impH (substF3 B 2 (var 3) 2 (n2t x) 3 (n2t n)) (substF3 βR 1 (Succ (var 3)) 2 (n2t x) 3 (n2t n))) 1). apply impI. apply impE with (substF (impH (substF3 B 2 (var 3) 2 (n2t x) 3 (n2t n)) (substF3 βR 1 (Succ (var 3)) 2 (n2t x) 3 (n2t n))) 1 (n2t (f n))). + apply (subWithEquals LNN). apply eqSym. apply Axm; right; constructor. + apply sysWeaken. rewrite (subFormulaImp LNN). apply impTrans with (equal (var 0) (n2t (f (S n)))). * destruct H0 as (H0, H4). simpl in H4. apply impTrans with (substF3 B 2 (var 3) 3 (n2t n) 1 (n2t (f n))). -- apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN). intro H5. destruct (freeVarSubFormula3 _ _ _ _ _ H5) as [H6 | [H6 | H6]]. ++ elim (in_remove_neq _ _ _ _ _ H6). reflexivity. ++ discriminate H6. ++ elim H6. -- apply impTrans with (substF2 B 2 (n2t n) 1 (n2t (f n))). ++ apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN). intro H5; elim (proj1 (Nat.le_ngt 3 2)). ** apply H0. eapply in_remove. apply H5. ** repeat constructor. ++ unfold f. simpl. apply iffE1. apply H4. * rewrite <- (subFormulaId LNN (substF4 βR 1 (Succ (var 3)) 2 (n2t x) 3 (n2t n) 1 (n2t (f n))) 0). apply impI. apply impE with (substF5 βR 1 (Succ (var 3)) 2 (n2t x) 3 (n2t n) 1 (n2t (f n)) 0 (n2t (f (S n)))). -- apply (subWithEquals LNN). apply eqSym. apply Axm; right; constructor. -- apply sysWeaken. apply impE with (substF5 βR 2 (n2t x) 1 (Succ (var 3)) 3 (n2t n) 1 (n2t (f n)) 0 (n2t (f (S n)))). ++ apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). ** discriminate. ** simpl. lia. ** apply closedNatToTerm. ++ apply impE with (substF5 βR 2 (n2t x) 3 (n2t n) 1 (n2t (S n)) 1 (n2t (f n)) 0 (n2t (f (S n)))). ** apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]). replace (n2t (S n)) with (substT (Succ (var 3)) 3 (n2t n)). --- apply (subSubFormula LNN). +++ discriminate. +++ apply closedNatToTerm. --- simpl. reflexivity. ** destruct repBeta as (H4, H5). apply impE with (substF4 βR 2 (n2t x) 1 (n2t (S n)) 1 (n2t (f n)) 0 (n2t (f (S n)))). --- apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN). intro H6. destruct (freeVarSubFormula3 _ _ _ _ _ H6) as [H7 | H7]. +++ elim (proj1 (Nat.le_ngt 3 2)). *** apply H4. eapply in_remove. apply H7. *** repeat constructor. +++ elim (closedNatToTerm _ _ H7). --- simpl in H5. apply impE with (substF2 (equal (var 0) (n2t (β x (S n)))) 1 (n2t (f n)) 0 (n2t (f (S n)))). +++ apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]). apply H5. +++ repeat rewrite (subFormulaEqual LNN). simpl. repeat (rewrite (subTermNil LNN (n2t (β x (S n)))); [| apply closedNatToTerm ]). rewrite H2. *** apply eqRefl. *** repeat rewrite <- Nat.succ_lt_mono. apply H1. } +++ intros b H1. assert (H4: forall z : nat, decidable (f z = β b z)). { unfold decidable. intros z. destruct (eq_nat_dec (f z) (β b z)); auto. } decompose record (notBoundedForall (fun z : nat => f z = β b z) (S a) H4 (H3 b H1)) /r; intros x0 H6 H7. apply impE with (notH (equal (n2t (f x0)) (n2t (β b x0)))). *** apply cp2. unfold primRecSigmaFormulaHelp. repeat first [ rewrite subExistSpecial; [| discriminate ] | rewrite subForallSpecial; [| discriminate ] | rewrite (subFormulaAnd LNN) | rewrite (subFormulaImp LNN) ]. rewrite (subFormulaExist LNN). simpl. repeat first [ rewrite subExistSpecial; [| discriminate ] | rewrite subForallSpecial; [| discriminate ] | rewrite (subFormulaAnd LNN) | rewrite (subFormulaImp LNN) ]. apply impI. clear H4 H1 H3 H2 x P H7. induction x0 as [| x0 Hrecx0]. ---- apply impE with (existH 0 (andH (substF (substF A 1 (n2t a)) 2 (n2t b)) (substF4 βR 1 Zero 2 (var 2) 1 (n2t a) 2 (n2t b)))). ++++ apply sysWeaken. apply impI. apply existSys. **** apply closedNN. **** intro H1. destruct (in_app_or _ _ _ H1) as [H2 | H2]. { elim (closedNatToTerm _ _ H2). } { elim (closedNatToTerm _ _ H2). } **** apply eqTrans with (var 0). { destruct H as (H, H1). simpl in H1. apply eqSym. unfold f; simpl. apply impE with A. - apply sysWeaken. apply iffE1. assumption. - apply impE with (substF2 A 1 (n2t a) 2 (n2t b)). + apply sysWeaken. apply iffE1. apply iffTrans with (substF A 2 (n2t b)). * repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN). intro H2. elim (proj1 (Nat.le_ngt 1 0)); auto. * apply (subFormulaNil LNN). intro H2. elim (proj1 (Nat.le_ngt 2 0)); auto. + eapply andE1. apply Axm; right; constructor. } { destruct repBeta as (H1, H2). simpl in H2. apply impE with (substF4 βR 1 Zero 2 (var 2) 1 (n2t a) 2 (n2t b)). - apply sysWeaken. apply iffE1. apply iffTrans with (substF2 βR 2 (n2t b) 1 (n2t 0)). + rewrite (subFormulaId LNN). apply iffTrans with (substF2 βR 1 Zero 2 (n2t b)). * repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN). intro H3. destruct (freeVarSubFormula3 _ _ _ _ _ H3) as [H4 | H4]. -- elim (in_remove_neq _ _ _ _ _ H4); reflexivity. -- apply H4. * apply (subFormulaExch LNN). -- discriminate. -- apply closedNatToTerm. -- apply closedNatToTerm. + apply H2. - eapply andE2. apply Axm; right; constructor. } ++++ eapply andE1. apply Axm; right; constructor. ---- apply impE with (equal (n2t (f x0)) (n2t (β b x0))); [| apply Hrecx0 ]. ++++ clear Hrecx0. apply impE with (forallH 3 (impH (substF2 (LT (var 3) (var 1)) 1 (n2t a) 2 (n2t b)) (existH 0 (existH 1 (andH (substF4 βR 1 (var 3) 2 (var 2) 0 (var 1) 2 (n2t b)) (andH (substF2 B 2 (var 3) 2 (n2t b)) (substF3 βR 1 (Succ (var 3)) 2 (var 2) 2 (n2t b)))))))); [| eapply andE2; apply Axm; right; constructor ]. apply sysWeaken. apply impTrans with (substF (impH (substF2 (LT (var 3) (var 1)) 1 (n2t a) 2 (n2t b)) (existH 0 (existH 1 (andH (substF4 βR 1 (var 3) 2 (var 2) 0 (var 1) 2 (n2t b)) (andH (substF2 B 2 (var 3) 2 (n2t b)) (substF3 βR 1 (Succ (var 3)) 2 (var 2) 2 (n2t b))))))) 3 (n2t x0)). **** apply impI. apply forallE. apply Axm; right; constructor. **** repeat first [ rewrite subExistSpecial; [| discriminate ] | rewrite subForallSpecial; [| discriminate ] | rewrite (subFormulaAnd LNN) | rewrite (subFormulaImp LNN) ]. apply impTrans with (existH 0 (existH 1 (andH (substF5 βR 1 (var 3) 2 (var 2) 0 (var 1) 2 (n2t b) 3 (n2t x0)) (andH (substF3 B 2 (var 3) 2 (n2t b) 3 (n2t x0)) (substF4 βR 1 (Succ (var 3)) 2 (var 2) 2 (n2t b) 3 (n2t x0)))))). { apply impI. apply impE with (substF3 (LT (var 3) (var 1)) 1 (n2t a) 2 (n2t b) 3 (n2t x0)). - apply Axm; right; constructor. - apply sysWeaken. unfold LT. repeat rewrite (subFormulaRelation LNN). simpl. repeat (rewrite (subTermNil LNN (n2t a)); [| apply closedNatToTerm ]). fold (LT (n2t x0) (n2t a)). apply natLT. now rewrite Nat.succ_lt_mono. } { apply impI. assert (H1:forall n : nat, ~ In n (freeVarF (impH (equal (n2t (f x0)) (n2t (β b x0))) (equal (n2t (f (S x0))) (n2t (β b (S x0))))))). { simpl. intros n H1. destruct (in_app_or _ _ _ H1) as [H2 | H2]; induction (in_app_or _ _ _ H2) as [H3 | H3]; elim (closedNatToTerm _ _ H3). } apply existSys. - apply closedNN. - apply H1. - apply existSys. + apply closedNN. + apply H1. + unfold f at 2; simpl. fold (f x0) in |- *. apply impE with (equal (var 1) (n2t (β b x0))). * apply impI. apply impE with (equal (var 0) (n2t (h x0 (β b x0)))). -- repeat apply impI. apply eqTrans with (var 0). ++ apply eqTrans with (n2t (h x0 (β b x0))). ** destruct (eq_nat_dec (f x0) (β b x0)) as [a0 | b0]. --- rewrite a0. apply eqRefl. --- apply contradiction with (equal (n2t (f x0)) (n2t (β b x0))). +++ apply Axm; right; constructor. +++ do 4 apply sysWeaken. apply natNE. auto. ** apply eqSym. apply Axm; left; right; constructor. ++ apply impE with (substF4 βR 1 (Succ (var 3)) 2 (var 2) 2 (n2t b) 3 (n2t x0)). ** do 4 apply sysWeaken. apply iffE1. destruct repBeta as (H2, H3). simpl in H3. apply iffTrans with (substF2 βR 2 (n2t b) 1 (n2t (S x0))). --- rewrite (subFormulaId LNN). apply iffTrans with (substF3 βR 2 (n2t b) 1 (Succ (var 3)) 3 (n2t x0)). +++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). *** discriminate. *** simpl; lia. *** apply closedNatToTerm. +++ apply iffTrans with (substF3 βR 2 (n2t b) 3 (n2t x0) 1 (substT (Succ (var 3)) 3 (n2t x0))). *** apply (subSubFormula LNN). ---- discriminate. ---- apply closedNatToTerm. *** simpl; apply iffTrans with (substF2 βR 2 (n2t b) 1 (substT (Succ (var 3)) 3 (n2t x0))). ---- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN). intro H4. destruct (freeVarSubFormula3 _ _ _ _ _ H4) as [H5 | H5]. ++++ elim (proj1 (Nat.le_ngt 3 2)). **** apply H2. eapply in_remove. apply H5. **** repeat constructor. ++++ elim (closedNatToTerm _ _ H5). ---- apply iffRefl. --- apply H3. ** eapply andE2. eapply andE2. apply Axm; do 3 left; right; constructor. -- apply impE with (substF4 B 2 (var 3) 2 (n2t b) 3 (n2t x0) 1 (n2t (β b x0))). ++ do 2 apply sysWeaken. destruct H0 as (H0, H2). simpl in H2. apply iffE1. apply iffTrans with (substF2 B 2 (n2t x0) 1 (n2t (β b x0))). ** apply iffTrans with (substF3 B 2 (var 3) 3 (n2t x0) 1 (n2t (β b x0))). --- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN). intro H3. destruct (freeVarSubFormula3 _ _ _ _ _ H3) as [H4 | H4]. +++ elim (in_remove_neq _ _ _ _ _ H4). reflexivity. +++ destruct H4 as [H4 | H4]. *** discriminate H4. *** apply H4. --- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN). intro H3. elim (proj1 (Nat.le_ngt 3 2)). +++ apply H0. eapply in_remove. apply H3. +++ repeat constructor. ** apply H2. ++ apply impE with (substF4 B 2 (var 3) 2 (n2t b) 3 (n2t x0) 1 (var 1)). ** apply (subWithEquals LNN). apply Axm; right; constructor. ** repeat rewrite (subFormulaId LNN). eapply andE1. eapply andE2. apply Axm; left; right; constructor. * apply impE with (substF5 βR 1 (var 3) 2 (var 2) 0 (var 1) 2 (n2t b) 3 (n2t x0)). -- apply sysWeaken. apply iffE1. destruct repBeta as (H2, H3). simpl in H3. apply iffTrans with (substF (equal (var 0) (n2t (β b x0))) 0 (var 1)). ++ rewrite (subFormulaId LNN). apply iffTrans with (substF4 βR 1 (var 3) 2 (n2t b) 0 (var 1) 3 (n2t x0)). ** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). --- discriminate. --- intros [H4 | H4]. +++ discriminate H4. +++ apply H4. --- apply closedNatToTerm. ** apply iffTrans with (substF4 βR 1 (var 3) 2 (n2t b) 3 (n2t x0) 0 (var 1)). --- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). +++ discriminate. +++ intros [H4 | H4]. *** discriminate H4. *** apply H4. +++ apply closedNatToTerm. --- apply (reduceSub LNN). +++ apply closedNN. +++ apply iffTrans with (substF3 βR 2 (n2t b) 1 (var 3) 3 (n2t x0)). *** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). ---- discriminate. ---- intros [H4 | H4]. ++++ discriminate H4. ++++ apply H4. ---- apply closedNatToTerm. *** apply iffTrans with (substF2 βR 2 (n2t b) 1 (n2t x0)). ---- repeat (apply (reduceSub LNN); [apply closedNN |]). apply (subFormulaTrans LNN). intro H4. assert (H5: In 3 (freeVarF (substF βR 2 (n2t b)))). { eapply in_remove. apply H4. } destruct (freeVarSubFormula3 _ _ _ _ _ H5) as [H7 | H7]. ++++ elim (proj1 (Nat.le_ngt 3 2)). **** apply H2. eapply in_remove. apply H7. **** repeat constructor. ++++ elim (closedNatToTerm _ _ H7). ---- apply H3. ++ rewrite (subFormulaEqual LNN). simpl. rewrite subTermNil. ** apply iffRefl. ** apply closedNatToTerm. -- eapply andE1. apply Axm; right; constructor. } ++++ apply Nat.lt_lt_succ_r. now rewrite Nat.succ_lt_mono. *** apply natNE. auto. +++ intros b H1. assert (H4: forall z : nat, decidable (f z = β b z)). { unfold decidable. intros z. destruct (eq_nat_dec (f z) (β b z)); auto. } decompose record (notBoundedForall (fun z : nat => f z = β b z) (S a) H4 (H3 b H1)) /r; intros x0 H6 H7. apply impE with (notH (equal (n2t (f x0)) (n2t (β b x0)))). *** apply cp2. unfold primRecPiFormulaHelp. repeat first [ rewrite subExistSpecial; [| discriminate ] | rewrite subForallSpecial; [| discriminate ] | rewrite (subFormulaAnd LNN) | rewrite (subFormulaImp LNN) ]. rewrite (subFormulaForall LNN). simpl. repeat first [ rewrite subExistSpecial; [| discriminate ] | rewrite subForallSpecial; [| discriminate ] | rewrite (subFormulaAnd LNN) | rewrite (subFormulaImp LNN) ]. apply impI. clear H4 H1 H3 H2 x P H7. induction x0 as [| x0 Hrecx0]. ---- apply impE with (forallH 0 (impH (substF2 A 1 (n2t a) 2 (n2t b)) (substF4 βR 1 Zero 2 (var 2) 1 (n2t a) 2 (n2t b)))). ++++ apply sysWeaken. apply impTrans with (substF (impH (substF2 A 1 (n2t a) 2 (n2t b)) (substF4 βR 1 Zero 2 (var 2) 1 (n2t a) 2 (n2t b))) 0 (n2t (f 0))). **** apply impI. apply forallE. apply Axm; right; constructor. **** apply impI. rewrite (subFormulaImp LNN). apply impE with (substF5 βR 1 Zero 2 (var 2) 1 (n2t a) 2 (n2t b) 0 (n2t (f 0))). { apply sysWeaken. apply impTrans with (substF (equal (var 0) (n2t (β b 0))) 0 (n2t (f 0))). - apply iffE1. apply (reduceSub LNN). + apply closedNN. + rewrite (subFormulaId LNN). destruct repBeta as (H1, H2). simpl in H2. apply iffTrans with (substF2 βR 2 (n2t b) 1 (n2t 0)). * apply iffTrans with (substF2 βR 1 Zero 2 (n2t b)). -- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN). intro H3. destruct (freeVarSubFormula3 _ _ _ _ _ H3) as [H4 | H4]. ++ elim (in_remove_neq _ _ _ _ _ H4); reflexivity. ++ apply H4. -- apply (subFormulaExch LNN). ++ discriminate. ++ apply closedNatToTerm. ++ apply closedNatToTerm. * apply H2. - rewrite (subFormulaEqual LNN). simpl. rewrite (subTermNil LNN). + apply impRefl. + apply closedNatToTerm. } { apply impE with (substF3 A 1 (n2t a) 2 (n2t b) 0 (n2t (f 0))). - apply Axm; right; constructor. - apply sysWeaken. apply impE with (substF (equal (var 0) (n2t (f 0))) 0 (n2t (f 0))). + apply iffE2. apply (reduceSub LNN); [ apply closedNN |]. destruct H as (H, H1). simpl in H1. unfold f; simpl. apply iffTrans with A; [| assumption ]. apply iffTrans with (substF A 2 (n2t b)). * repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN). intro H2. elim (proj1 (Nat.le_ngt 1 0)); auto. * apply (subFormulaNil LNN). intro H2. elim (proj1 (Nat.le_ngt 2 0)); auto. + rewrite (subFormulaEqual LNN). simpl. rewrite (subTermNil LNN). * apply eqRefl. * apply closedNatToTerm. } ++++ eapply andE1. apply Axm; right; constructor. ---- apply impE with (equal (n2t (f x0)) (n2t (β b x0))); [| apply Hrecx0 ]. ++++ clear Hrecx0. apply impE with (forallH 3 (impH (substF2 (LT (var 3) (var 1)) 1 (n2t a) 2 (n2t b)) (forallH 0 (forallH 1 (impH (substF4 βR 1 (var 3) 2 (var 2) 0 (var 1) 2 (n2t b)) (impH (substF2 B 2 (var 3) 2 (n2t b)) (substF3 βR 1 (Succ (var 3)) 2 (var 2) 2 (n2t b)))))))); [| eapply andE2; apply Axm; right; constructor ]. apply sysWeaken. apply impTrans with (substF (impH (substF2 (LT (var 3) (var 1)) 1 (n2t a) 2 (n2t b)) (forallH 0 (forallH 1 (impH (substF4 βR 1 (var 3) 2 (var 2) 0 (var 1) 2 (n2t b)) (impH (substF (substF B 2 (var 3)) 2 (n2t b)) (substF3 βR 1 (Succ (var 3)) 2 (var 2) 2 (n2t b))))))) 3 (n2t x0)). **** apply impI. apply forallE. apply Axm; right; constructor. **** repeat first [ rewrite subExistSpecial; [| discriminate ] | rewrite subForallSpecial; [| discriminate ] | rewrite (subFormulaAnd LNN) | rewrite (subFormulaImp LNN) ]. apply impTrans with (forallH 0 (forallH 1 (impH (substF5 βR 1 (var 3) 2 (var 2) 0 (var 1) 2 (n2t b) 3 (n2t x0)) (impH (substF3 B 2 (var 3) 2 (n2t b) 3 (n2t x0)) (substF4 βR 1 (Succ (var 3)) 2 (var 2) 2 (n2t b) 3 (n2t x0)))))). { apply impI. apply impE with (substF3 (LT (var 3) (var 1)) 1 (n2t a) 2 (n2t b) 3 (n2t x0)). - apply Axm; right; constructor. - apply sysWeaken. unfold LT. repeat rewrite (subFormulaRelation LNN). simpl. repeat (rewrite (subTermNil LNN (n2t a)); [| apply closedNatToTerm ]). fold (LT (n2t x0) (n2t a)). apply natLT. now apply Nat.succ_lt_mono. } { apply impTrans with (substF (forallH 1 (impH (substF5 βR 1 (var 3) 2 (var 2) 0 (var 1) 2 (n2t b) 3 (n2t x0)) (impH (substF3 B 2 (var 3) 2 (n2t b) 3 (n2t x0)) (substF4 βR 1 (Succ (var 3)) 2 (var 2) 2 (n2t b) 3 (n2t x0))))) 0 (n2t (f (S x0)))). - apply impI. apply forallE. apply Axm; right; constructor. - repeat first [ rewrite subExistSpecial; [| discriminate ] | rewrite subForallSpecial; [| discriminate ] | rewrite (subFormulaAnd LNN) | rewrite (subFormulaImp LNN) ]. apply impTrans with (substF (impH (substF6 βR 1 (var 3) 2 (var 2) 0 (var 1) 2 (n2t b) 3 (n2t x0) 0 (n2t (f (S x0)))) (impH (substF4 B 2 (var 3) 2 (n2t b) 3 (n2t x0) 0 (n2t (f (S x0)))) (substF5 βR 1 (Succ (var 3)) 2 (var 2) 2 (n2t b) 3 (n2t x0) 0 (n2t (f (S x0)))))) 1 (n2t (β b x0))). + apply impI. apply forallE. apply Axm; right; constructor. + repeat first [ rewrite subExistSpecial; [| discriminate ] | rewrite subForallSpecial; [| discriminate ] | rewrite (subFormulaAnd LNN) | rewrite (subFormulaImp LNN) ]. repeat apply impI. apply impE with (substF (equal (var 0) (n2t (β b (S x0)))) 0 (n2t (f (S x0)))). * rewrite (subFormulaEqual LNN). simpl. rewrite (subTermNil LNN). -- apply impRefl. -- apply closedNatToTerm. * apply impE with (substF6 βR 1 (Succ (var 3)) 2 (var 2) 2 (n2t b) 3 (n2t x0) 0 (n2t (f (S x0))) 1 (n2t (β b x0))). -- do 2 apply sysWeaken. apply iffE1. apply iffTrans with (substF6 βR 1 (Succ (var 3)) 2 (var 2) 2 (n2t b) 3 (n2t x0) 1 (n2t (β b x0)) 0 (n2t (f (S x0)))). ++ apply (subFormulaExch LNN). ** discriminate. ** apply closedNatToTerm. ** apply closedNatToTerm. ++ apply (reduceSub LNN). ** apply closedNN. ** destruct H0 as (H0, H1). destruct repBeta as (H2, H3). simpl in H3. apply iffTrans with (substF2 βR 2 (n2t b) 1 (n2t (S x0))). --- rewrite (subFormulaId LNN). apply iffTrans with (substF4 βR 2 (n2t b) 1 (Succ (var 3)) 3 (n2t x0) 1 (n2t (β b x0))). +++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). *** discriminate. *** intros [H4 | H4]. ---- discriminate H4. ---- apply H4. *** apply closedNatToTerm. +++ apply iffTrans with (substF4 βR 2 (n2t b) 3 (n2t x0) 1 (substT (Succ (var 3)) 3 (n2t x0)) 1 (n2t (β b x0))). *** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subSubFormula LNN). ---- discriminate. ---- apply closedNatToTerm. *** simpl; apply iffTrans with (substF3 βR 2 (n2t b) 1 (substT (Succ (var 3)) 3 (n2t x0)) 1 (n2t (β b x0))). ---- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN). intro H4. destruct (freeVarSubFormula3 _ _ _ _ _ H4) as [H5 | H5]. { elim (proj1 (Nat.le_ngt 3 2)). - apply H2. eapply in_remove. apply H5. - repeat constructor. } { elim (closedNatToTerm _ _ H5). } ---- apply (subFormulaNil LNN). intro H4. destruct (freeVarSubFormula3 _ _ _ _ _ H4) as [H5 | H5]. { elim (in_remove_neq _ _ _ _ _ H5). reflexivity. } { rewrite freeVarSucc in H5. elim (closedNatToTerm _ _ H5). } --- apply H3. -- eapply impE. ++ eapply impE. ** apply Axm; left; right; constructor. ** do 2 apply sysWeaken. apply impE with (substF2 (equal (var 1) (n2t (β b x0))) 0 (n2t (f (S x0))) 1 (n2t (β b x0))). --- apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]). destruct H0 as (H0, H1). destruct repBeta as (H2, H3). simpl in H3. apply iffTrans with (substF (equal (var 0) (n2t (β b x0))) 0 (var 1)). +++ rewrite (subFormulaId LNN). apply iffTrans with (substF4 βR 1 (var 3) 2 (n2t b) 0 (var 1) 3 (n2t x0)). *** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). ---- discriminate. ---- intros [H4 | H4]. ++++ discriminate H4. ++++ apply H4. ---- apply closedNatToTerm. *** apply iffTrans with (substF4 βR 1 (var 3) 2 (n2t b) 3 (n2t x0) 0 (var 1)). ---- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). ++++ discriminate. ++++ simpl. lia. ++++ apply closedNatToTerm. ---- apply (reduceSub LNN). ++++ apply closedNN. ++++ apply iffTrans with (substF3 βR 2 (n2t b) 1 (var 3) 3 (n2t x0)). **** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). { discriminate. } { simpl. lia. } { apply closedNatToTerm. } **** apply iffTrans with (substF2 βR 2 (n2t b) 1 (n2t x0)). { repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN). intro H4. assert (H5: In 3 (freeVarF (substF βR 2 (n2t b)))). { eapply in_remove. apply H4. } destruct (freeVarSubFormula3 _ _ _ _ _ H5) as [H7 | H7]. - elim (proj1 (Nat.le_ngt 3 2)). + apply H2. eapply in_remove. apply H7. + repeat constructor. - elim (closedNatToTerm _ _ H7). } { apply H3. } +++ rewrite (subFormulaEqual LNN). simpl. rewrite subTermNil. **** apply iffRefl. **** apply closedNatToTerm. --- repeat rewrite (subFormulaEqual LNN). simpl. repeat rewrite (subTermNil LNN (n2t (β b x0))); try apply closedNatToTerm. apply eqRefl. ++ apply impE with (substF5 B 2 (var 3) 2 (n2t b) 3 (n2t x0) 0 (n2t (f (S x0))) 1 (n2t (f x0))). ** apply (subWithEquals LNN). apply Axm; right; constructor. ** do 2 apply sysWeaken. apply impE with (substF5 B 2 (var 3) 2 (n2t b) 3 (n2t x0) 1 (n2t (f x0)) 0 (n2t (f (S x0)))). --- apply iffE1. apply (subFormulaExch LNN). +++ discriminate. +++ apply closedNatToTerm. +++ apply closedNatToTerm. --- apply impE with (substF (equal (var 0) (n2t (f (S x0)))) 0 (n2t (f (S x0)))). +++ apply iffE2. apply (reduceSub LNN). *** apply closedNN. *** destruct H0 as (H0, H1). simpl in H1. apply iffTrans with (substF2 B 2 (n2t x0) 1 (n2t (f x0))). ---- apply iffTrans with (substF3 B 2 (var 3) 3 (n2t x0) 1 (n2t (f x0))). ++++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN). intro H2. destruct (freeVarSubFormula3 _ _ _ _ _ H2) as [H3 | H3]. **** elim (in_remove_neq _ _ _ _ _ H3). reflexivity. **** destruct H3 as [H3 | H3]. { discriminate H3. } { apply H3. } ++++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN). intro H2. elim (proj1 (Nat.le_ngt 3 2)). **** apply H0. eapply in_remove. apply H2. **** repeat constructor. ---- unfold f. simpl. apply H1. +++ rewrite (subFormulaEqual LNN). simpl. rewrite (subTermNil LNN). *** apply eqRefl. *** apply closedNatToTerm. } ++++ apply Nat.lt_lt_succ_r. now rewrite Nat.succ_lt_mono. *** apply natNE. auto. --- apply iffRefl. ++ apply iffTrans with (substF2 βR 1 (n2t a) 2 (n2t x)). ** apply iffI. --- apply impI. apply existSys. +++ apply closedNN. +++ intro H1. destruct (freeVarSubFormula3 _ _ _ _ _ H1) as [H4 | H4]. *** elim (in_remove_neq _ _ _ _ _ H4). reflexivity. *** elim (closedNatToTerm _ _ H4). +++ apply impE with (substF2 βR 1 (n2t a) 2 (var 2)). *** apply (subWithEquals LNN). eapply andE1. apply Axm; right; constructor. *** rewrite (subFormulaId LNN). eapply andE2. apply Axm; right; constructor. --- apply impI. apply existI with (n2t x). rewrite (subFormulaAnd LNN). apply andI. +++ rewrite (subFormulaEqual LNN). simpl. rewrite subTermNil. *** apply eqRefl. *** apply closedNatToTerm. +++ apply Axm; right; constructor. ** apply iffTrans with (substF2 βR 2 (n2t x) 1 (n2t a)). --- apply (subFormulaExch LNN). +++ discriminate. +++ apply closedNatToTerm. +++ apply closedNatToTerm. --- rewrite H2. +++ destruct repBeta as (H1, H4). apply H4. +++ apply Nat.lt_succ_diag_r. -- intros z H2. unfold beta. repeat (rewrite cPairProjections1 || rewrite cPairProjections2). now apply (p z). - simpl; intros A g H B h H0 a a0. apply Representable_ext with (evalPrimRecFunc n (g a0) (fun x y : nat => h x y a0) a). + induction a as [| a Hreca]. * simpl. apply extEqualRefl. * simpl. apply extEqualCompose2. -- apply Hreca. -- apply extEqualRefl. + destruct H as (H, H1). destruct H0 as (H0, H2). simpl in H1. simpl in H2. assert (H3: RepresentableHelp n (evalPrimRecFunc n (g a0) (fun x y : nat => h x y a0) a) (substF (primRecSigmaFormula n (substF A n.+1 (n2t a0)) (substF3 B n.+1 (n2t a0) n.+2 (var n.+1) n.+3 (var n.+2))) n.+1 (n2t a))). { apply Hrecn. - split. + intros v H3. induction (freeVarSubFormula3 _ _ _ _ _ H3). * assert (H5: v <= S n). { apply H. eapply in_remove. apply H4. } destruct (proj1 (Nat.lt_eq_cases v (S n)) H5) as [H6 | H6]. -- now apply Nat.lt_succ_r. -- elim (in_remove_neq _ _ _ _ _ H4). auto. * elim (closedNatToTerm _ _ H4). + apply H1. - split. + intros v H3. repeat match goal with | H:(In v (List.remove eq_nat_dec ?X1 (freeVarF ?X2))) |- _ => assert (In v (freeVarF X2)); [ eapply in_remove; apply H | assert (v <> X1); [ eapply in_remove_neq; apply H | clear H ] ] | H:(In v (freeVarF (substF ?X1 ?X2 ?X3))) |- _ => induction (freeVarSubFormula3 _ _ _ _ _ H); clear H end. * assert (v <= n.+3). { apply H0. auto. } lia. * elim (closedNatToTerm _ _ H4). * destruct H4 as [H3| H3]. -- rewrite <- H3. apply Nat.le_succ_diag_r. -- elim H3. * destruct H4 as [H3| H3]. -- rewrite <- H3. apply le_n. -- elim H3. + simpl. intros. apply RepresentableAlternate with (substF3 B n.+3 (n2t a1) n.+2 (n2t a2) n.+1 (n2t a0)). * apply iffSym. apply iffTrans with (substF4 B n.+1 (n2t a0) n.+2 (var n.+1) n.+3 (n2t a1) n.+1 (n2t a2)). -- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN). intro H3. repeat match goal with | H:(In ?X1 (List.remove eq_nat_dec ?X1 (freeVarF ?X2))) |- _ => elim (in_remove_neq _ _ _ _ _ H); reflexivity | H:(In ?X3 (List.remove eq_nat_dec ?X1 (freeVarF ?X2))) |- _ => assert (In X3 (freeVarF X2)); [ eapply in_remove; apply H | assert (X3 <> X1); [ eapply in_remove_neq; apply H | clear H ] ] | H:(In ?X4 (freeVarF (substF ?X1 ?X2 ?X3))) |- _ => induction (freeVarSubFormula3 _ _ _ _ _ H); clear H | H:(In ?X4 (@freeVarT LNN (var ?X1))) |- _ => induction H as [H3| H3]; [ idtac | contradiction ] end. congruence. -- apply iffTrans with (substF4 B n.+1 (n2t a0) n.+3 (n2t a1) n.+2 (var n.+1) n.+1 (n2t a2)). ++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). ** lia. ** simpl. lia. ** apply closedNatToTerm. ++ apply iffTrans with (substF3 B n.+1 (n2t a0) n.+3 (n2t a1) n.+2 (n2t a2)). ** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN). intro H3. repeat match goal with | H:(In ?X1 (List.remove eq_nat_dec ?X1 (freeVarF ?X2))) |- _ => elim (in_remove_neq _ _ _ _ _ H); reflexivity | H:(In ?X3 (List.remove eq_nat_dec ?X1 (freeVarF ?X2))) |- _ => assert (In X3 (freeVarF X2)); [ eapply in_remove; apply H | assert (X3 <> X1); [ eapply in_remove_neq; apply H | clear H ] ] | H:(In ?X4 (freeVarF (substF ?X1 ?X2 ?X3))) |- _ => induction (freeVarSubFormula3 _ _ _ _ _ H); clear H | H:(In ?X4 (@freeVarT LNN (var ?X1))) |- _ => simple induction H; [ idtac | contradiction ] end. --- elim (closedNatToTerm _ _ H3). --- elim (closedNatToTerm _ _ H3). ** apply iffTrans with (substF3 B n.+3 (n2t a1) n.+1 (n2t a0) n.+2 (n2t a2)). --- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN). +++ lia. +++ apply closedNatToTerm. +++ apply closedNatToTerm. --- apply (subFormulaExch LNN). +++ lia. +++ apply closedNatToTerm. +++ apply closedNatToTerm. * apply H2. } apply RepresentableAlternate with (substF (primRecSigmaFormula n (substF A n.+1 (n2t a0)) (substF3 B n.+1 (n2t a0) n.+2 (var n.+1) n.+3 (var n.+2))) n.+1 (n2t a)). * clear H3 Hrecn; apply iffSym. apply iffTrans with (substF2 (primRecSigmaFormula (S n) A B) n.+1 (n2t a0) n.+2 (n2t a)). -- apply (subFormulaExch LNN). ++ lia. ++ apply closedNatToTerm. ++ apply closedNatToTerm. -- apply iffTrans with (substF3 (primRecSigmaFormula (S n) A B) n.+1 (n2t a0) n.+2 (var (S n)) n.+1 (n2t a)). ++ apply iffSym. apply (subFormulaTrans LNN). intro H3. assert (H4: In n.+1 (freeVarF (substF (primRecSigmaFormula n.+1 A B) n.+1 (n2t a0)))). { eapply in_remove. apply H3. } destruct (freeVarSubFormula3 _ _ _ _ _ H4) as [H5 | H5]. ** elim (in_remove_neq _ _ _ _ _ H5). reflexivity. ** elim (closedNatToTerm _ _ H5). ++ apply (reduceSub LNN). apply closedNN. unfold primRecSigmaFormula. assert (H3 := I). assert (H4 := I). assert (subExistSpecial : forall (F : Formula) (a b c : nat), b <> c -> substF (existH b F) c (n2t a) = existH b (substF F c (n2t a))). { intros F a1 b c H5. rewrite (subFormulaExist LNN). destruct (eq_nat_dec b c) as [e | e]. - elim H5. auto. - destruct (In_dec eq_nat_dec b (freeVarT (n2t a1))) as [e0 | e0]. + elim (closedNatToTerm _ _ e0). + reflexivity. } assert (subForallSpecial : forall (F : Formula) (a b c : nat), b <> c -> substF (forallH b F) c (n2t a) = forallH b (substF F c (n2t a))). { intros F a1 b c H5. rewrite (subFormulaForall LNN). destruct (eq_nat_dec b c) as [e | e]. - elim H5. auto. - destruct (In_dec eq_nat_dec b (freeVarT (n2t a1))) as [e0 | e0]. + elim (closedNatToTerm _ _ e0). + reflexivity. } assert (H5: forall a b : nat, a <> b -> b <> a) by auto. assert (subExistSpecial2 : forall (F : Formula) (a b c : nat), b <> c -> b <> a -> substF (existH b F) c (var a) = existH b (substF F c (var a))). { intros F a1 b c H6 H7. rewrite (subFormulaExist LNN). destruct (eq_nat_dec b c) as [e | e]. - elim H6. auto. - destruct (In_dec eq_nat_dec b (@freeVarT LNN (var a1))) as [e0 | e0]. + destruct e0 as [H8| H8]. * elim H7; auto. * elim H8. + reflexivity. } assert (subForallSpecial2 : forall (F : Formula) (a b c : nat), b <> c -> b <> a -> substF (forallH b F) c (var a) = forallH b (substF F c (var a))). { intros F a1 b c H6 H7; rewrite (subFormulaForall LNN). destruct (eq_nat_dec b c) as [e | e]. - elim H6. auto. - destruct (In_dec eq_nat_dec b (@freeVarT LNN (var a1))) as [e0 | e0]. + destruct e0 as [H8 | H8]. * elim H7; auto. * elim H8. + reflexivity. } assert (H6 := I). assert (H7 := I). assert (H8: forall (a b : Term) (v : nat) (s : Term), substF (LT a b) v s = LT (substT a v s) (substT b v s)). { intros a1 b v s. unfold LT. rewrite (subFormulaRelation LNN). reflexivity. } assert (H9: forall (f : Formula) (a : nat) (s : Term), substF (existH a f) a s = existH a f). { intros f a1 s. rewrite (subFormulaExist LNN). destruct (eq_nat_dec a1 a1) as [e | e]. - reflexivity. - elim e; auto. } assert (H10: forall (f : Formula) (a : nat) (s : Term), substF (forallH a f) a s = forallH a f). { intros f a1 s. rewrite (subFormulaForall LNN). destruct (eq_nat_dec a1 a1) as [e | e]. - reflexivity. - elim e; auto. } assert (H11 := I). assert (H12 := I). assert (H13 := I). assert (H14 := I). assert (H15 := I). assert (H16 := I). Opaque substF. unfold minimize, primRecSigmaFormulaHelp, primRecPiFormulaHelp; repeat first [ discriminate | simple apply iffRefl | simple apply (reduceExist LNN); [ apply closedNN |] | simple apply (reduceForall LNN); [ apply closedNN |] | simple apply (reduceAnd LNN) | simple apply (reduceImp LNN) | simple apply (reduceNot LNN) | match goal with | |- (folProof.SysPrf LNN NN (iffH (substF2 (existH n.+2 ?X1) ?X2 (var n.+2) ?X3 ?X4) _)) => apply iffTrans with (substF (substF (existH n.+1 (substF X1 n.+2 (var n.+1))) X2 (var n.+2)) X3 X4); [ repeat (apply (reduceSub LNN); [ apply closedNN |]); apply (rebindExist LNN) |] | |- (folProof.SysPrf LNN NN (iffH (substF3 (forallH (S (S n)) ?X1) ?X2 (var (S (S n))) ?X3 ?X4 ?X5 ?X6) _)) => apply iffTrans with (substF (substF (substF (forallH (S n) (substF X1 (S (S n)) (var (S n)))) X2 (var (S (S n)))) X3 X4) X5 X6); [ repeat (apply (reduceSub LNN); [ apply closedNN |]); apply (rebindForall LNN) |] | |- (folProof.SysPrf LNN NN (iffH (substF (forallH (S ?X6) ?X1) ?X2 (var (S ?X6))) _)) => apply iffTrans with (substF (forallH X6 (substF X1 (S X6) (var X6))) X2 (var (S X6))); [ repeat (apply (reduceSub LNN); [ apply closedNN |]); apply (rebindForall LNN) |] | |- (folProof.SysPrf LNN NN (iffH (existH (S ?X1) ?X2) ?X3)) => apply iffTrans with (existH X1 (substF X2 (S X1) (var X1))); [ apply (rebindExist LNN) |] | |- (folProof.SysPrf LNN NN (iffH (forallH (S ?X1) ?X2) ?X3)) => apply iffTrans with (forallH X1 (substF X2 (S X1) (var X1))); [ apply (rebindForall LNN) |] | |- (?X1 <> S ?X1) => lia | |- (?X1 <> S (S ?X1)) => lia | |- (?X1 <> S (S (S ?X1))) => lia | |- (?X1 <> S (S (S (S ?X1)))) => lia | |- (S ?X1 <> ?X1) => lia | |- (S (S ?X1) <> ?X1) => lia | |- (S (S (S ?X1)) <> ?X1) => lia | |- (S (S (S (S ?X1))) <> ?X1) => lia | |- (~ In _ _) => PRsolveFV A B n end | rewrite H9 | rewrite H10 | rewrite (subFormulaAnd LNN) | rewrite (subFormulaImp LNN) | rewrite (subFormulaNot LNN) | rewrite H8 | rewrite (subTermVar1 LNN) | rewrite (subTermVar2 LNN) | rewrite subForallSpecial2; let fail := (match goal with | |- (?X1 <> ?X1) => constr:(false) | _ => constr:(true) end) in match constr:(fail) with | true => idtac end | rewrite subForallSpecial | rewrite subExistSpecial2; let fail := (match goal with | |- (?X1 <> ?X1) => constr:(false) | _ => constr:(true) end) in match constr:(fail) with | true => idtac end | rewrite subExistSpecial ]. ** apply iffTrans with (substF2 A n.+1 (n2t a0) n.+3 (var n.+2)). --- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN). PRsolveFV A B n. --- apply (subFormulaNil LNN). PRsolveFV A B n. ** apply iffTrans with (substF4 βR 1 Zero 2 (var n.+3) n.+2 (var n.+1) n.+3 (var n.+2)). --- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN). PRsolveFV A B n. --- apply iffTrans with (substF3 βR 1 Zero 2 (var n.+3) n.+3 (var n.+2)). +++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN). PRsolveFV A B n. +++ apply (subFormulaTrans LNN). PRsolveFV A B n. ** apply iffTrans with (substF6 βR 1 (var n.+4) 2 (var n.+3) 0 (var n.+2) n.+2 (var n.+1) n.+3 (var n.+2) n.+4 (var n.+3)). --- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN). PRsolveFV A B n. --- apply iffTrans with (substF5 βR 1 (var n.+4) 2 (var n.+3) 0 (var n.+1) n.+3 (var n.+2) n.+4 (var n.+3)). +++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN). PRsolveFV A B n. +++ apply iffTrans with (substF5 βR 1 (var n.+4) 2 (var n.+3) n.+3 (var n.+2) 0 (var n.+1) n.+4 (var n.+3)). *** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN); PRsolveFV A B n. *** apply iffTrans with (substF4 βR 1 (var n.+4) 2 (var n.+2) 0 (var n.+1) n.+4 (var n.+3)). ---- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN). PRsolveFV A B n. ---- apply iffTrans with (substF4 βR 1 (var n.+4) 2 (var n.+2) n.+4 (var n.+3) 0 (var n.+1)). ++++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN); PRsolveFV A B n. ++++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply iffTrans with (substF3 βR 1 (var n.+4) n.+4 (var n.+3) 2 (var n.+2)). **** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN); PRsolveFV A B n. **** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN). PRsolveFV A B n. ** apply iffTrans with (substF5 B n.+1 (n2t a0) n.+3 (var n.+4) n.+2 (var n.+1) n.+3 (var n.+2) n.+4 (var n.+3)). --- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN); PRsolveFV A B n. --- apply iffTrans with (substF5 B n.+1 (n2t a0) n.+2 (var n.+1) n.+3 (var n.+4) n.+3 (var n.+2) n.+4 (var n.+3)). +++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN); PRsolveFV A B n. +++ apply iffTrans with (substF4 B n.+1 (n2t a0) n.+2 (var n.+1) n.+3 (var n.+4) n.+4 (var n.+3)). *** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. *** apply iffTrans with (substF3 B n.+1 (n2t a0) n.+2 (var n.+1) n.+3 (var n.+3)). ---- apply (subFormulaTrans LNN); PRsolveFV A B n. ---- apply iffSym. apply (subFormulaTrans LNN); PRsolveFV A B n. ** apply iffTrans with (substF5 βR 1 (Succ (var n.+4)) 2 (var n.+3) n.+2 (var n.+1) n.+3 (var n.+2) n.+4 (var n.+3)). --- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. --- apply iffTrans with (substF4 βR 1 (Succ (var n.+4)) 2 (var n.+3) n.+3 (var n.+2) n.+4 (var n.+3)). +++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. +++ apply iffTrans with (substF3 βR 1 (Succ (var n.+4)) 2 (var n.+2) n.+4 (var n.+3)). *** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN); PRsolveFV A B n. *** apply iffTrans with (substF3 βR 1 (Succ (var n.+4)) n.+4 (var n.+3) 2 (var n.+2)). ---- apply (subFormulaExch LNN); PRsolveFV A B n. ---- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply iffTrans with (substF2 βR n.+4 (var n.+3) 1 (substT (Succ (var n.+4)) n.+4 (var n.+3))). ++++ apply (subSubFormula LNN); PRsolveFV A B n. ++++ replace (substT (Succ (var n.+4)) n.+4 (var n.+3)) with (Succ (substT (var n.+4) (n.+4) (var n.+3))). **** rewrite (subTermVar1 LNN). repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. **** reflexivity. ** apply iffTrans with (substF4 A n.+1 (n2t a0) n.+2 (var n.+1) n.+3 (var n.+2) n.+5 (var n.+4)). --- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. --- apply iffTrans with (substF3 A n.+1 (n2t a0) n.+3 (var n.+2) n.+5 (var n.+4)). +++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. +++ apply iffTrans with (substF2 A n.+1 (n2t a0) n.+5 (var n.+4)). *** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. *** apply iffTrans with (substF A (S n) (n2t a0)). ---- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. ---- apply iffSym. apply (subFormulaNil LNN); PRsolveFV A B n. ** apply iffTrans with (substF6 βR 1 Zero 2 (var n.+5) n.+1 (n2t a0) n.+2 (var n.+1) n.+3 (var n.+2) n.+5 (var n.+4)). --- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN); PRsolveFV A B n. --- apply iffTrans with (substF5 βR 1 Zero 2 (var n.+5) n.+2 (var n.+1) n.+3 (var n.+2) n.+5 (var n.+4)). +++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. lia. +++ apply iffTrans with (substF4 βR 1 Zero 2 (var n.+5) n.+3 (var n.+2) n.+5 (var n.+4)). *** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. *** apply iffTrans with (substF3 βR 1 Zero 2 (var n.+5) n.+5 (var n.+4)). ---- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. ---- apply iffTrans with (substF2 βR 1 Zero 2 (var n.+4)). ++++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN); PRsolveFV A B n. ++++ apply iffSym. apply (subFormulaTrans LNN); PRsolveFV A B n. congruence. ** apply iffTrans with (substF9 βR 1 (var n.+4) 2 (var n.+3) n.+3 (var n.+5) 0 (var n.+2) n.+1 (n2t a0) n.+2 (var n.+1) n.+3 (var n.+2) n.+4 (var n.+3) n.+5 (var n.+4)). --- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN); PRsolveFV A B n. --- apply iffTrans with (substF8 βR 1 (var n.+4) 2 (var n.+5) 0 (var n.+2) n.+1 (n2t a0) n.+2 (var n.+1) n.+3 (var n.+2) n.+4 (var n.+3) n.+5 (var n.+4)). +++ repeat (apply (reduceSub LNN); [apply closedNN |]). apply (subFormulaTrans LNN); PRsolveFV A B n. +++ apply iffTrans with (substF7 βR 1 (var n.+4) 2 (var n.+5) 0 (var n.+2) n.+2 (var n.+1) n.+3 (var n.+2) n.+4 (var n.+3) n.+5 (var n.+4)). *** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. lia. *** apply iffTrans with (substF6 βR 1 (var n.+4) 2 (var n.+5) 0 (var n.+1) n.+3 (var n.+2) n.+4 (var n.+3) n.+5 (var n.+4)). ---- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN); PRsolveFV A B n. ---- apply iffTrans with (substF5 βR 1 (var n.+4) 2 (var n.+5) 0 (var n.+1) n.+4 (var n.+3) n.+5 (var n.+4)). ++++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. ++++ apply iffTrans with (substF5 βR 1 (var n.+4) 2 (var n.+5) n.+4 (var n.+3) 0 (var n.+1) n.+5 (var n.+4)). **** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN); PRsolveFV A B n. **** apply iffTrans with (substF5 βR 1 (var n.+4) n.+4 (var n.+3) 2 (var n.+5) 0 (var n.+1) n.+5 (var n.+4)). { repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN); PRsolveFV A B n. } { apply iffTrans with (substF4 βR 1 (var n.+3) 2 (var n.+5) 0 (var n.+1) n.+5 (var n.+4)). - repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN); PRsolveFV A B n. - apply iffTrans with (substF4 βR 1 (var n.+3) 2 (var n.+5) n.+5 (var n.+4) 0 (var n.+1)). + repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN); PRsolveFV A B n. lia. + apply iffTrans with (substF3 βR 1 (var n.+3) 2 (var n.+4) 0 (var n.+1)). * repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN); PRsolveFV A B n. * apply iffSym. apply iffTrans with (substF4 βR 1 (var n.+3) 2 (var n.+2) n.+2 (var n.+4) 0 (var n.+1)). -- apply (subFormulaExch LNN); PRsolveFV A B n. -- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN); PRsolveFV A B n. congruence. } ** apply iffTrans with (substF6 B n.+3 (var n.+4) n.+1 (n2t a0) n.+2 (var n.+1) n.+3 (var n.+2) n.+4 (var n.+3) n.+5 (var n.+4)). --- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. --- apply iffTrans with (substF5 B n.+3 (var n.+4) n.+1 (n2t a0) n.+2 (var n.+1) n.+4 (var n.+3) n.+5 (var n.+4)). +++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. +++ apply iffTrans with (substF5 B n.+1 (n2t a0) n.+3 (var n.+4) n.+2 (var n.+1) n.+4 (var n.+3) n.+5 (var n.+4)). *** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN); PRsolveFV A B n. *** apply iffTrans with (substF5 B n.+1 (n2t a0) n.+2 (var n.+1) n.+3 (var n.+4) n.+4 (var n.+3) n.+5 (var n.+4)). ---- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN); PRsolveFV A B n. ---- apply iffTrans with (substF4 B n.+1 (n2t a0) n.+2 (var n.+1) n.+3 (var n.+3) n.+5 (var n.+4)). ++++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN); PRsolveFV A B n. ++++ apply iffTrans with (substF3 B n.+1 (n2t a0) n.+2 (var n.+1) n.+3 (var n.+3)). **** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. lia. **** apply iffSym. apply iffTrans with (substF4 B n.+1 (n2t a0) n.+2 (var n.+1) n.+3 (var n.+2) n.+2 (var n.+3)). { apply (subFormulaNil LNN); PRsolveFV A B n. } { apply (subFormulaTrans LNN); PRsolveFV A B n. } ** apply iffTrans with (substF7 βR 1 (Succ (var n.+4)) 2 (var n.+5) n.+1 (n2t a0) n.+2 (var n.+1) n.+3 (var n.+2) n.+4 (var n.+3) n.+5 (var n.+4)). --- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN); PRsolveFV A B n. --- apply iffTrans with (substF6 βR 1 (Succ (var n.+4)) 2 (var n.+5) n.+2 (var n.+1) n.+3 (var n.+2) n.+4 (var n.+3) n.+5 (var n.+4)). +++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. lia. +++ apply iffTrans with (substF5 βR 1 (Succ (var n.+4)) 2 (var n.+5) n.+3 (var n.+2) n.+4 (var n.+3) n.+5 (var n.+4)). *** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. *** apply iffTrans with (substF4 βR 1 (Succ (var n.+4)) 2 (var n.+5) n.+4 (var n.+3) n.+5 (var n.+4)). ---- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. ---- apply iffTrans with (substF4 βR 1 (Succ (var n.+4)) n.+4 (var n.+3) 2 (var n.+5) n.+5 (var n.+4)). ++++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaExch LNN); PRsolveFV A B n. ++++ apply iffTrans with (substF3 βR 1 (Succ (var n.+4)) n.+4 (var n.+3) 2 (var n.+4)). **** repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN); PRsolveFV A B n. **** apply iffTrans with (substF2 βR 1 (Succ (var n.+3)) 2 (var n.+4)). { repeat (apply (reduceSub LNN); [ apply closedNN |]). apply iffTrans with (substF2 βR n.+4 (var n.+3) 1 (substT (Succ (var n.+4)) n.+4 (var n.+3))). - apply (subSubFormula LNN); PRsolveFV A B n. - replace (substT (Succ (var n.+4)) n.+4 (var n.+3)) with (Succ (substT (var n.+4) n.+4 (var n.+3))). + rewrite (subTermVar1 LNN). repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. + reflexivity. } { apply iffSym. apply (subFormulaTrans LNN); PRsolveFV A B n. congruence. } ** apply iffTrans with (substF4 βR 2 (var n.+3) 1 (var n.+2) n.+2 (var n.+1) n.+3 (var n.+2)). --- repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaNil LNN); PRsolveFV A B n. --- apply iffTrans with (substF3 βR 2 (var n.+3) 1 (var n.+1) n.+3 (var n.+2)). +++ repeat (apply (reduceSub LNN); [ apply closedNN |]). apply (subFormulaTrans LNN); PRsolveFV A B n. +++ apply iffTrans with (substF3 βR 2 (var n.+3) n.+3 (var n.+2) 1 (var n.+1)). *** apply (subFormulaExch LNN); PRsolveFV A B n. *** repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaTrans LNN); PRsolveFV A B n. * apply H3. } intros n A g H0 B h H1. split. - destruct H0 as (H0, H2). destruct H1 as (H1, H3). intros v H4. assert (H5: forall v : nat, In v (freeVarF βR) -> v <= 2). { eapply proj1. apply betaRepresentable. } assert (H6: forall v : nat, v <> n.+2 -> v <= n.+2 -> v <= n.+1) by lia. unfold primRecSigmaFormula, minimize, existH in H4; repeat match goal with | H1:(?X1 = ?X2), H2:(?X1 <> ?X2) |- _ => elim H2; apply H1 | H1:(?X1 = ?X2), H2:(?X2 <> ?X1) |- _ => elim H2; symmetry in |- *; apply H1 | H:(v = ?X1) |- _ => rewrite H; clear H | H:(?X1 = v) |- _ => rewrite <- H; clear H | H:(In ?X3 (freeVarF (existH ?X1 ?X2))) |- _ => assert (In X3 (List.remove eq_nat_dec X1 (freeVarF X2))); [ apply H | clear H ] | H:(In ?X3 (freeVarF (forallH ?X1 ?X2))) |- _ => assert (In X3 (List.remove eq_nat_dec X1 (freeVarF X2))); [ apply H | clear H ] | H:(In ?X3 (List.remove eq_nat_dec ?X1 (freeVarF ?X2))) |- _ => assert (In X3 (freeVarF X2)); [ eapply in_remove; apply H | assert (X3 <> X1); [ eapply in_remove_neq; apply H | clear H ] ] | H:(In ?X3 (freeVarF (andH ?X1 ?X2))) |- _ => assert (In X3 (freeVarF X1 ++ freeVarF X2)); [ apply H | clear H ] | H:(In ?X3 (freeVarF (impH ?X1 ?X2))) |- _ => assert (In X3 (freeVarF X1 ++ freeVarF X2)); [ apply H | clear H ] | H:(In ?X3 (freeVarF (notH ?X1))) |- _ => assert (In X3 (freeVarF X1)); [ apply H | clear H ] | H:(In _ (freeVarF (primRecSigmaFormulaHelp _ _ _))) |- _ => decompose sum (freeVarPrimRecSigmaFormulaHelp1 _ _ _ _ H); clear H | H:(In _ (freeVarF (primRecPiFormulaHelp _ _ _))) |- _ => decompose sum (freeVarPrimRecPiFormulaHelp1 _ _ _ _ H); clear H | H:(In ?X3 (freeVarF A)) |- _ => apply Nat.le_trans with n; [ apply H0; apply H | apply Nat.le_succ_diag_r ] | H:(In ?X3 (freeVarF B)) |- _ => apply H6; [ clear H | apply H1; apply H ] | H:(In _ (_ ++ _)) |- _ => induction (in_app_or _ _ _ H); clear H | H:(In _ (freeVarF (substF ?X1 ?X2 ?X3))) |- _ => induction (freeVarSubFormula3 _ _ _ _ _ H); clear H | H:(In _ (freeVarF (LT ?X1 ?X2))) |- _ => rewrite freeVarLT in H | H:(In _ (freeVarT (n2t _))) |- _ => elim (closedNatToTerm _ _ H) | H:(In _ (freeVarT Zero)) |- _ => elim H | H:(In _ (freeVarT (Succ _))) |- _ => rewrite freeVarSucc in H | H:(In _ (@freeVarT LNN (var _))) |- _ => simpl in H; decompose sum H; clear H | H:(In _ (@freeVarT LNN (var _))) |- _ => simpl in H; decompose sum H; clear H end; try first [ assumption | apply le_n ]. assert (H7: v <= 2) by auto. lia. - apply H; auto. Qed.
imports: Coq(Arith) hydras.Ackermann(extEqualNat subAll folProp subProp folReplace folLogic3 NN NNtheory primRec expressible) Coqprime(ChineseRem) Coq(Vector List Lia) hydras(ListExt cPair MoreDecidable) hydras(Compat815 ssrnat_extracts) Coq(Utf8)