proposition: Remark maxSubTerm (t : fol.Term L) (v : nat) (s : fol.Term L): fold_right Nat.max 0 (freeVarT (substT t v s)) <= fold_right Nat.max 0 (freeVarT s ++ freeVarT t).
proof: Proof. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => fold_right Nat.max 0 (freeVarTs (substTs ts v s)) <= fold_right Nat.max 0 (freeVarT s ++ freeVarTs ts)); simpl; intros. - induction (eq_nat_dec v n) as [a | ?]. + apply maxLemma2. + apply maxLemma3. - apply H. - apply Nat.le_0_l. - replace (freeVarTs (Tcons (substT t0 v s) (substTs t1 v s))) with (freeVarT (substT t0 v s) ++ freeVarTs (substTs t1 v s)). + replace (freeVarTs (Tcons t0 t1)) with (freeVarT t0 ++ freeVarTs t1). * induction (maxApp (freeVarT (substT t0 v s)) (freeVarTs (substTs t1 v s))) as [a | b]. -- rewrite a; eapply Nat.le_trans. ++ apply H. ++ induction (maxApp (freeVarT s) (freeVarT t0)) as [a0 | b]. ** rewrite a0. apply maxLemma2. ** rewrite b; apply Nat.le_trans with (fold_right Nat.max 0 (freeVarT t0 ++ freeVarTs t1)). apply maxLemma2. apply maxLemma3. -- rewrite b. eapply Nat.le_trans. ++ apply H0. ++ induction (maxApp (freeVarT s) (freeVarTs t1)) as [a | b0]. ** rewrite a. apply maxLemma2. ** rewrite b0. apply Nat.le_trans with (fold_right Nat.max 0 (freeVarT t0 ++ freeVarTs t1)). apply maxLemma3. apply maxLemma3. * reflexivity. + reflexivity. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)