proposition: Lemma boundComputationMonotone : forall a1 a2 b1 b2 c1 c2 : nat, a1 <= a2 -> b1 <= b2 -> c1 <= c2 -> boundComputation a1 b1 c1 <= boundComputation a2 b2 c2.
proof: Proof. intros a1 a2; revert a1; unfold boundComputation. induction a2 as [| a2 Hreca2]; simpl. - intros a1 b1 b2 c1 c2 H H0 H1; rewrite Nat.le_0_r in H; rewrite H. simpl; unfold cTriple; apply cPairLe3. + assumption. + apply cPairLe3. * assumption. * apply le_n. - intros a1 b1 b2 c1 c2 H H0 H1; generalize H ; intro H'; rewrite Nat.lt_eq_cases in H'. destruct H' as [H2 | H2]. + eapply Nat.le_trans. * apply (Hreca2 a1 b1 b2 c1 c2); try assumption. apply Compat815.lt_n_Sm_le. assumption. * unfold cTriple at 3; eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. apply cPairLe2. + rewrite H2; simpl; unfold cTriple at 6 1. apply cPairLe3. * assumption. * apply cPairLe3. -- assumption. -- apply cPairLe3; apply Hreca2; apply le_n || assumption. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)