normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
cut (y - S n = a);
- [2: elim daemon | ];
+ [2: rewrite > eq_minus_S_pred;
+ rewrite > H2;
+ reflexivity | ];
rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;
(* instruction ADDd *)
letin K ≝
| rewrite < minus_n_n;
apply status_eq;
[1,2,3,4,5,7: normalize; reflexivity
- | elim daemon
+ | intro;
+ change with (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat O)) 32
+(byte_of_nat (nat_of_byte x*nat_of_byte y)) a =
+ update (update (mult_memory x y) 31 (mk_byte x0 x0)) 32
+(byte_of_nat (nat_of_byte x*nat_of_byte y)) a);
+ apply inj_update; intro;
+ apply inj_update; intro;
+ change in ⊢ (? ? (? ? ? % ?) ?) with (mult_memory x y 30);
+ apply eq_update_s_a_sa
]
]
].