| changeset 4710 | 05e57f1879ee |
| parent 4359 | 6f2986464280 |
| child 5069 | 3ea049f7979d |
| 4709:d24168720303 | 4710:05e57f1879ee |
|---|---|
57 \ DO {A^B = c * a^b} \ |
57 \ DO {A^B = c * a^b} \ |
58 \ a:=a*a; \ |
58 \ a:=a*a; \ |
59 \ b:=b div 2 \ |
59 \ b:=b div 2 \ |
60 \ END; \ |
60 \ END; \ |
61 \ c:=c*a; \ |
61 \ c:=c*a; \ |
62 \ b:=pred b \ |
62 \ b:= b - 1 \ |
63 \ END \ |
63 \ END \ |
64 \ {c = A^B}"; |
64 \ {c = A^B}"; |
65 |
65 |
66 by (hoare_tac 1); |
66 by (hoare_tac 1); |
67 |
67 |