- generalize in match (loop_invariant' x y y (le_n y)); intro;
- generalize in match (breakpoint (mult_status x y) (5 + 23*y) 9); intro;
- cut (5 + 23*y +9 = 14 + 23* y);
- [2: autobatch paramodulation
- | rewrite > Hcut in H1;
- change in H1:(? ? % ?) with s;
- letin s0 ≝ (execute (mult_status x y) (S (S (S (S (S O))))+S 22*y));
- generalize in match H; intro K; clear H;
- change in K with
- (s0 =
- mk_status (byte_of_nat (x*y)) 4 0 true false
- (update
- (update
- (update (mult_memory x y) 30 x)
- 31 (byte_of_nat (y-y)))
- 32 (byte_of_nat (x*y))) O);
- clear Hcut;
- generalize in match H1; intro K1; clear H1;
- change in K1 with (s = execute s0 9);
- rewrite > K in K1;
- clear K; clear s0; clearbody s; clear i;
- rewrite < minus_n_n in K1;
- split;
- rewrite > K1;
- reflexivity
- ]
-qed.*)
\ No newline at end of file
+ cut (14 + 23 * y = 5 + 23*y + 9);
+ [2: autobatch paramodulation;
+ | rewrite > Hcut; (* clear Hcut; *)
+ rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
+ rewrite > loop_invariant';
+ [2: apply le_n
+ | rewrite < minus_n_n;
+ apply status_eq;
+ [1,2,3,4,5,7: normalize; reflexivity
+ | elim daemon
+ ]
+ ]
+ ].
+qed.
\ No newline at end of file