- ∀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;
- letin foo ≝ (execute (mult_status x (mk_byte x0 x0)) 8);
- whd in foo;
-reduce in foo:(? ? ? ? ? ? ? ?);
- whd in foo;
-
- xxx.
- change with
- (let s ≝ execute (mult_status x (mk_byte x0 x0)) 14 in
- (* pc s = 22 ∧*) eq ? (mem s 32) (byte_of_nat 0)).
- xxxxxxxxx
- whd in ⊢ ((\lambda i:?.(let s \def ? in ? ? % %)) ?).
-
- reduce;
- (* split; *)
- reflexivity;
+ ∀x.
+ let s ≝
+ execute 14 (mk_byte x0 x0) 0 0 false false (mult_mem x (mk_byte x0 x0)) 0
+ in
+ pc s = 22 ∧ mem s 32 = byte_of_nat 0.
+ intros; split; reflexivity;