proposition: Lemma PAboundedLT : forall (m : nat) (F : LNT.Formula) (x : nat), (forall n : nat, n < m -> SysPrf PA (substF F x (natToTerm n))) -> SysPrf PA (LNN2LNT_formula (v#x < LNN.natToTerm m)%fol -> F)%nt.
proof: Proof. simple induction m. - intros F x H; apply impI. apply contradiction with (LNN2LNT_formula (v#x < LNN.natToTerm 0)%fol). apply Axm; right; constructor. apply sysWeaken. replace (notH (LNN2LNT_formula (LT (var x) (LNN.natToTerm 0)))) with (LNN2LNT_formula (notH (LT (var x) (LNN.natToTerm 0)))). + apply NN2PA. apply nn7. + reflexivity. - intros n H a x H0; apply impI. eapply orE. + apply impE with (LNN2LNT_formula (LT (var x) (LNN.natToTerm (S n)))). * apply sysWeaken. assert (H1: SysPrf PA (LNN2LNT_formula ((v#x < S_ (LNN.natToTerm n)) -> (v#x < LNN.natToTerm n) \/ v#x = LNN.natToTerm n))%fol) by (apply NN2PA, nn8). simpl in H1; simpl. unfold orH; apply H1. * apply Axm; right; constructor. + apply sysWeaken. simpl in H; apply H; auto. + apply sysWeaken, impI. rewrite <- (subFormulaId LNT a x). rewrite LNN2LNT_natToTerm. apply impE with (substF a x (natToTerm n)). * apply (subWithEquals LNT). apply eqSym. apply Axm; right; constructor. * apply sysWeaken. apply H0. apply Nat.lt_succ_diag_r . Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(folProp folProof subProp folLogic3 folReplace NN PAtheory) hydras.Ackermann(subAll ListExt)