proposition: Remark codeTermFreeVar : forall s : fol.Term L, fold_right Nat.max 0 (freeVarT s) <= codeTerm s.
proof: Proof. intros s; elim s using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => fold_right Nat.max 0 (freeVarTs ts) <= codeTerms ts); simpl. - intros n; apply Nat.max_case. + unfold codeTerm, code.codeTerm; apply cPairLe2. + apply Nat.le_0_l. - intros f t H; apply Nat.le_trans with (codeTerms t). + assumption. + unfold codeTerm, code.codeTerm; apply cPairLe2. - apply Nat.le_0_l. - intros n t H t0 H0; replace (freeVarTs (Tcons t t0)) with (freeVarT t ++ freeVarTs t0); [ idtac | reflexivity ]. replace (codeTerms (Tcons t t0)) with (S (cPair (codeTerm t) (codeTerms t0))); [ idtac | reflexivity ]. induction (maxApp (freeVarT t) (freeVarTs t0)) as [a | b]. + rewrite a. eapply Nat.le_trans. * apply H. * apply le_S. apply cPairLe1. + rewrite b. eapply Nat.le_trans. * apply H0. * apply le_S. apply cPairLe2. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)