+notation "hvbox(# break a)"
+ non associative with precedence 80
+for @{ 'byte_of_opcode $a }.
+interpretation "byte_of_opcode" 'byte_of_opcode a =
+ (cic:/matita/assembly/byte_of_opcode.con a).
+
+definition mult_source : list byte ≝
+ [#LDAi; mk_byte x0 x0;
+ #STAd; mk_byte x2 x0; (* 18 = locazione $12 *)
+ #LDAd; mk_byte x1 xF; (* 17 = locazione $11 *)
+ #BEQ; mk_byte x0 xC;
+ #LDAd; mk_byte x1 x2;
+ #DECd; mk_byte x1 xF;
+ #ADDd; mk_byte x1 xE; (* 16 = locazione $10 *)
+ #STAd; mk_byte x2 x0;
+ #LDAd; mk_byte x1 xF;
+ #BRA; mk_byte xF x2; (* 242 = -14 *)
+ #LDAd; mk_byte x2 x0].
+
+definition mult_status ≝
+ λx,y.
+ mk_status (mk_byte x0 x0) 0 0 false false
+ (λa:addr.
+ match leb a 29 with
+ [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
+ | false ⇒
+ match eqb a 30 with
+ [ true ⇒ x
+ | false ⇒ y
+ ]
+ ]) 0.
+
+lemma goo1:
+ ∀x.
+ (λi.
+ let s ≝ execute (mult_status x (mk_byte x0 x0)) i in
+ pc s = 22 ∧ mem s 32 = byte_of_nat 0) 14.
+ intros;
+ whd;
+ split;
+ [ reduce;
+ reflexivity
+ | reduce;
+ reflexivity
+ ].
+
+
+lemma goo1:
+ ∀x.
+ let i ≝ 14 in
+ let s ≝ execute (mult_status x (mk_byte x0 x0)) i in
+ pc s = 22 ∧ mem s 32 = byte_of_nat 0.
+ intros;
+ split;
+ [ reduce;
+
+ |
+ ].
+qed.
+
+lemma goo1:
+ ∀x,y.
+ let i ≝ 14 + 23 * nat_of_byte y in
+ let s ≝ execute (mult_status x y) i in
+ pc s = 22 ∧ mem s 32 = byte_of_nat (nat_of_byte x * nat_of_byte y).
+ intros;
+qed.
+