proposition: Lemma exec_asm_seq : forall pg stk stk1 mem mem1 ec1 ec2 pc pc1, exec_asm ec1 pg stk mem pc = (stk1, mem1, pc1) -> exec_asm (ec1 + ec2) pg stk mem pc = exec_asm ec2 pg stk1 mem1 pc1.
proof: Proof. intros pg stk stk1 mem mem1 ec1; revert stk stk1 mem mem1. induction ec1. simpl; intros stk stk1 mem mem1 ec2 pc pc1 [= stst mm pp]. now subst. intros stk stk1 mem mem1 ec2 pc pc1. simpl. destruct (nth_error pg pc) as [i | ] eqn:nthq; cycle 1. intros [= -> -> ->]. case ec2 as [ | ec]. auto. now simpl; rewrite nthq. intros cnd1. now apply IHec1. Qed.
imports: ZArith Arith List syntax little Lia