proposition: Remark maxVarFreeVar : forall f : fol.Formula L, fold_right Nat.max 0 (freeVarF f) <= fold_right Nat.max 0 (varFormula f).
proof: Proof. intros f; induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]; simpl. - apply le_n. - apply le_n. - induction (maxApp (freeVarF f1) (freeVarF f0)). + rewrite a. eapply Nat.le_trans. * apply Hrecf1. * apply maxLemma2. + rewrite b. eapply Nat.le_trans. * apply Hrecf0. * apply maxLemma3. - assumption. - apply Nat.le_trans with (fold_right Nat.max 0 (freeVarF f)). + clear Hrecf. induction (freeVarF f). * simpl in |- *. apply Nat.le_0_l. * simpl in |- *. induction (eq_nat_dec n a). -- eapply Nat.le_trans. ++ apply IHl. ++ apply Nat.le_max_r. -- simpl in |- *. apply maxLemma. ++ apply le_n. ++ assumption. + eapply Nat.le_trans. * apply Hrecf. * apply Nat.le_max_r. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)