proposition: Lemma KMC : forall p q r : nat, gencode (Call_K p r) -> gencode (Call_M q) -> gencode (Call_C (q * p + r) p).
proof: Proof. refine (fun p q r g g' => match g with | gencode_intro cpr s => match g' with | gencode_intro cq s0 => gencode_intro _ (app cpr (app cq (seq MUL End))) _ end end). inversion_clear s; inversion_clear s0. constructor 2. intros; rewrite Exec_app. rewrite (H M MO a). rewrite (Exec_app M MO); simpl in |- *; rewrite H0. simpl in |- *. apply Config_inv. rewrite power_eucl; auto with arith. auto with arith. Qed.
imports: Constants monoid spec machine Wf_compl Plus Mult Lt Mult_compl euclid two_power