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