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