proposition: Lemma MMK : forall p q : nat, gencode (Call_M p) -> gencode (Call_M q) -> gencode (Call_K (q * p) p).
proof: Proof. refine (fun p q g g' => match g with | gencode_intro cp s => match g' with | gencode_intro cq s0 => gencode_intro _ (app cp (seq PUSH cq)) _ end end). inversion_clear s; inversion_clear s0. constructor 3. intros; rewrite Exec_app. rewrite H; simpl in |- *. rewrite H0; simpl in |- *. apply Config_inv; auto with arith. rewrite <- power_mult; auto with arith. Qed.
imports: Constants monoid spec machine Wf_compl Plus Mult Lt Mult_compl euclid two_power