- letin K ≝
- (breakpoint
- (mk_status (byte_of_nat (x*n)) 12
- O (eqbyte 〈x0, x0〉 (byte_of_nat (y-S n)))
- (plusbytec (byte_of_nat (x*pred n)) x)
- (update
- (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
- 32 (byte_of_nat (x*n))) 31
- (byte_of_nat (y-S n))) O)
- 3 6); clearbody K;
- normalize in K:(? ? (? ? %) ?);
- apply transitive_eq; [2: apply K | skip | ]; clear K;