proposition: Lemma nnPlusNotNeeded (n:nat) : SysPrf NN (v#1 < natToTerm n \/ v#1 = natToTerm n -> v#1 < S_ (natToTerm n))%fol.
proof: Proof. induction n as [| n Hrecn]. - cbn; apply impI, orSys. + apply contradiction with (v#1 < Zero)%fol. * apply Axm; right; constructor. * apply sysWeaken, nn7. + rewrite <- (subFormulaId LNN (v#1 < S_ Zero)%fol 1). apply impE with (substF (v#1 < S_ Zero)%fol 1 Zero). * apply (subWithEquals LNN). apply eqSym. apply Axm; right; constructor. * apply sysWeaken; replace (substF (v#1 < S_ Zero)%fol 1 Zero) with (natToTerm 0 < natToTerm 1)%fol. -- apply natLT; auto. -- unfold LT; now rewrite (subFormulaRelation LNN). - cbn; apply impI, orSys. + apply impE with (v#1 < natToTerm n \/ v#1 = natToTerm n)%fol. * apply sysWeaken; apply impTrans with (v#1 < natToTerm (S n))%fol. -- apply Hrecn. -- apply boundedLT. intros n0 H. unfold Succ. replace (substF (v#1 < (S_ (S_ (natToTerm n))))%fol 1 (natToTerm n0)) with (natToTerm n0 < natToTerm (S (S n)))%fol. { apply natLT. now apply Nat.lt_lt_succ_r. } unfold LT; rewrite (subFormulaRelation LNN). cbn; rewrite (subTermNil LNN). ++ reflexivity. ++ apply closedNatToTerm. * apply impE with (v#1 < S_ (natToTerm n))%fol. -- apply sysWeaken, nn8. -- apply Axm; right; constructor. + unfold Succ; rewrite <- (subFormulaId LNN (v#1 < (S_ (S_ (natToTerm n))))%fol 1). apply impE with (substF (v#1 < S_ (S_ (natToTerm n)))%fol 1 (S_ (natToTerm n))). * apply (subWithEquals LNN), eqSym, Axm; right; constructor. * apply sysWeaken. replace (substF (v# 1 < S_ (S_ (natToTerm n)))%fol 1 (S_ (natToTerm n))) with (natToTerm (S n) < natToTerm (S (S n)))%fol. { apply natLT, Nat.lt_succ_diag_r. } unfold LT; rewrite (subFormulaRelation LNN); cbn. rewrite (subTermNil LNN). -- reflexivity. -- apply closedNatToTerm. Qed.
imports: Coq(Arith Lia) hydras.Ackermann(folLogic3 folProp subProp) hydras.Ackermann(folLogic3 folProp subProp) hydras(Compat815)