proposition: Lemma measure_compat : coarser Call Call_lt (ltof Call Call_measure).
proof: Proof. unfold coarser, ltof in |- *. simple induction 1; unfold Call_measure in |- *. intros; apply lt_n_S; apply mult_lt_l; auto with arith. unfold three in |- *; auto with arith. auto with arith. intros. apply lt_le_trans with (three * S p). simpl in |- *. apply lt_n_S. rewrite <- plus_n_O. apply plus_lt_compat_l. rewrite <- plus_Snm_nSm. simpl in |- *; auto with arith. auto with arith. auto with arith. intros. apply lt_le_trans with (three * S q). replace (three * S q) with (S (S (S (three * q)))). auto with arith. rewrite <- mult_n_Sm. rewrite plus_comm; simpl in |- *; auto with arith. auto with arith. intros; do 2 apply lt_n_S; apply mult_lt_l; auto with arith. unfold three in |- *; auto with arith. Qed.
imports: monoid spec Constants machine Euclid Le_lt_compl euclid shift two_power log2_spec develop Arith Peano_dec Compare_dec strategies Mult_compl Wf_nat Wf_compl