This is a proof of the Hoare while rule

      {B;C} p {C}
-----------------------
{C} while B do p {C;~B}

in KAT.  Recall that a partial correctness assertion {A} p {B}
is represented as either of the equivalent equations A;p = A;p;B
or A;p;~B = 0.  The while loop while B do p is represented as
(B;p)*;~B.  The rule is thus represented as a universal Horn formula

B;C;p = B;C;p;C  ->  C;(B;p)*;~B = C;(B;p)*;~B;C;~B

This proof illustrates the technique of publishing a more general
form of the desired theorem, citing the desired theorem as a special
case, then going back and proving the more general form.

======================================================================

>pub B;C;p = B;C;p;C -> C;(B;p)*;~B = C;(B;p)*;~B;C;~B
L0: B;C;p = B;C;p;C -> C;(B;p)*;~B = C;(B;p)*;~B;C;~B  (1 task)

current task:
T0: B;C;p = B;C;p;C |- C;(B;p)*;~B = C;(B;p)*;~B;C;~B

>focus

current task:
T0: B;C;p = B;C;p;C |- C;(B;p)*;~B = C;(B;p)*;~B;C;~B

C;(B;p)*;~B = C;(B;p)*;~B;C;~B
-----------

>r d d d r r

current task:
T0: B;C;p = B;C;p;C |- C;(B;p)*;~B = C;(B;p)*;~B;C;~B

C;(B;p)*;~B = C;(B;p)*;~B;C;~B
                       ----

>cite commut. l

current task:
T0: B;C;p = B;C;p;C |- C;(B;p)*;~B = C;(B;p)*;C;~B;~B

C;(B;p)*;~B = C;(B;p)*;C;~B;~B
                       ----

>r

current task:
T0: B;C;p = B;C;p;C |- C;(B;p)*;~B = C;(B;p)*;C;~B;~B

C;(B;p)*;~B = C;(B;p)*;C;~B;~B
                         -----

>cite idemp. l

current task:
T0: B;C;p = B;C;p;C |- C;(B;p)*;~B = C;(B;p)*;C;~B

C;(B;p)*;~B = C;(B;p)*;C;~B
                         --

>unf

current task:
T0: B;C;p = B;C;p;C |- C;(B;p)*;~B = C;(B;p)*;C;~B

>cite cong.R

current task:
T1: B;C;p = B;C;p;C |- C;(B;p)* = C;(B;p)*;C

>cut C;B;p = C;B;p;C

current task:
T2: B;C;p = B;C;p;C, C;B;p = C;B;p;C |- C;(B;p)* = C;(B;p)*;C

>pub C;q = C;q;C -> C;q* = C;q*;C
L1: C;q = C;q;C -> C;q* = C;q*;C  (1 task)

current task:
T4: C;q = C;q;C |- C;q* = C;q*;C

>get L0
L0: B;C;p = B;C;p;C -> C;(B;p)*;~B = C;(B;p)*;~B;C;~B  (2 tasks)

current task:
T2: B;C;p = B;C;p;C, C;B;p = C;B;p;C |- C;(B;p)* = C;(B;p)*;C

>cite L1

current task:
T5: B;C;p = B;C;p;C, C;B;p = C;B;p;C |- C;B;p = C;B;p;C

>use A1
task completed

current task:
T3: B;C;p = B;C;p;C |- C;B;p = C;B;p;C

>focus

current task:
T3: B;C;p = B;C;p;C |- C;B;p = C;B;p;C

C;B;p = C;B;p;C
-----

>d

current task:
T3: B;C;p = B;C;p;C |- C;B;p = C;B;p;C

C;B;p = C;B;p;C
---

>cite commut. l

current task:
T3: B;C;p = B;C;p;C |- B;C;p = C;B;p;C

B;C;p = C;B;p;C
---

>u r d d

current task:
T3: B;C;p = B;C;p;C |- B;C;p = C;B;p;C

B;C;p = C;B;p;C
        ---

>cite commut. l

current task:
T3: B;C;p = B;C;p;C |- B;C;p = B;C;p;C

B;C;p = B;C;p;C
        ---

>unf

current task:
T3: B;C;p = B;C;p;C |- B;C;p = B;C;p;C

>use A0
task completed

no tasks

>lib
L0: B;C;p = B;C;p;C -> C;(B;p)*;~B = C;(B;p)*;~B;C;~B  (proved)
L1: C;q = C;q;C -> C;q* = C;q*;C  (1 task)
ref=: x = x  (proved)
sym: x = y -> y = x  (proved)
trans=: x = y -> y = z -> x = z  (proved)
cong+R: x = y -> x + z = y + z  (proved)
cong.L: y = z -> x;y = x;z  (proved)
cong.R: x = y -> x;z = y;z  (proved)
cong*: x = y -> x* = y*  (proved)
<intro: x + y = y -> x < y  (proved)
<elim: x < y -> x + y = y  (proved)
ref<: x < x  (proved)
antisym: x < y -> y < x -> x = y  (proved)
trans<: x < y -> y < z -> x < z  (proved)
supL: x < x + y  (proved)
supR: y < x + y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
=<: x = y -> x < y  (proved)
mono+R: x < y -> x + z < y + z  (proved)
mono.L: y < z -> x;y < x;z  (proved)
mono.R: x < y -> x;z < y;z  (proved)
mono*: x < y -> x* < y*  (proved)
commut+: x + y = y + x  (proved)
id+L: 0 + x = x  (proved)
id+R: x + 0 = x  (proved)
idemp+: x + x = x  (proved)
id.L: 1;x = x  (proved)
id.R: x;1 = x  (proved)
annihL: 0;x = 0  (proved)
annihR: x;0 = 0  (proved)
distrL: x;(y + z) = x;y + x;z  (proved)
distrR: (x + y);z = x;z + y;z  (proved)
unwindL: 1 + x;x* = x*  (proved)
unwindR: 1 + x*;x = x*  (proved)
*L: z;y + x < z -> x;y* < z  (proved)
*R: x;z + y < z -> x*;y < z  (proved)
slide: x;(y;x)* = (x;y)*;x  (proved)
denest: x*;(y;x*)* = (x + y)*  (proved)
commut.: B;C = C;B  (proved)
idemp.: B;B = B  (proved)
~~: ~~B = B  (proved)
deMorgan+: ~(B + C) = ~B;~C  (proved)
deMorgan.: ~(B;C) = ~B + ~C  (proved)
~0: ~0 = 1  (proved)
~1: ~1 = 0  (proved)
compl+: B + ~B = 1  (proved)
compl.: B;~B = 0  (proved)
<1: B + 1 = 1  (proved)
distr.L: B + C;D = (B + C);(B + D)  (proved)
distr.R: B;C + D = (B + D);(C + D)  (proved)
abs+: B + B;C = B  (proved)
abs.: B;(B + C) = B  (proved)

no tasks

>get L1
L1: C;q = C;q;C -> C;q* = C;q*;C  (1 task)

current task:
T4: C;q = C;q;C |- C;q* = C;q*;C

>cite antisym

current task:
T6: C;q = C;q;C |- C;q* < C;q*;C

>cite *L

current task:
T8: C;q = C;q;C |- C;q*;C;q + C < C;q*;C

>foc

current task:
T8: C;q = C;q;C |- C;q*;C;q + C < C;q*;C

C;q*;C;q + C < C;q*;C
------------

>d d d r r

current task:
T8: C;q = C;q;C |- C;q*;C;q + C < C;q*;C

C;q*;C;q + C < C;q*;C
     ---

>use A0 l

current task:
T8: C;q = C;q;C |- C;q*;C;q;C + C < C;q*;C

C;q*;C;q;C + C < C;q*;C
     -----

>u r

current task:
T8: C;q = C;q;C |- C;q*;C;q;C + C < C;q*;C

C;q*;C;q;C + C < C;q*;C
             -

>cite idemp. r

current task:
T8: C;q = C;q;C |- C;q*;C;q;C + C;C < C;q*;C

C;q*;C;q;C + C;C < C;q*;C
             ---

>d

current task:
T8: C;q = C;q;C |- C;q*;C;q;C + C;C < C;q*;C

C;q*;C;q;C + C;C < C;q*;C
             -

>cite id.R r

current task:
T8: C;q = C;q;C |- C;q*;C;q;C + C;1;C < C;q*;C

C;q*;C;q;C + C;1;C < C;q*;C
             ---

>u u

current task:
T8: C;q = C;q;C |- C;q*;C;q;C + C;1;C < C;q*;C

C;q*;C;q;C + C;1;C < C;q*;C
------------------

>cite distrR r

current task:
T8: C;q = C;q;C |- (C;q*;C;q + C;1);C < C;q*;C

(C;q*;C;q + C;1);C < C;q*;C
------------------

>d

current task:
T8: C;q = C;q;C |- (C;q*;C;q + C;1);C < C;q*;C

(C;q*;C;q + C;1);C < C;q*;C
----------------

>cite distrL r

current task:
T8: C;q = C;q;C |- C;(q*;C;q + 1);C < C;q*;C

C;(q*;C;q + 1);C < C;q*;C
--------------

>unf

current task:
T8: C;q = C;q;C |- C;(q*;C;q + 1);C < C;q*;C

>cite mono.R

current task:
T9: C;q = C;q;C |- C;(q*;C;q + 1) < C;q*

>cite mono.L

current task:
T10: C;q = C;q;C |- q*;C;q + 1 < q*

>cite trans<
y=? q*;q + 1

current task:
T11: C;q = C;q;C |- q*;C;q + 1 < q*;q + 1

>cite mono+R

current task:
T13: C;q = C;q;C |- q*;C;q < q*;q

>cite mono.R

current task:
T14: C;q = C;q;C |- q*;C < q*

>foc

current task:
T14: C;q = C;q;C |- q*;C < q*

q*;C < q*
----

>r

current task:
T14: C;q = C;q;C |- q*;C < q*

q*;C < q*
       --

>cite id.R r

current task:
T14: C;q = C;q;C |- q*;C < q*;1

q*;C < q*;1
       ----

>unf

current task:
T14: C;q = C;q;C |- q*;C < q*;1

>cite mono.L

current task:
T15: C;q = C;q;C |- C < 1

>cite <intro

current task:
T16: C;q = C;q;C |- C + 1 = 1

>cite <1
task completed

current task:
T12: C;q = C;q;C |- q*;q + 1 < q*

>cite =<

current task:
T17: C;q = C;q;C |- q*;q + 1 = q*

>cite unwindR
citation does not apply

current task:
T17: C;q = C;q;C |- q*;q + 1 = q*

>cite unwindL
citation does not apply

current task:
T17: C;q = C;q;C |- q*;q + 1 = q*

>foc

current task:
T17: C;q = C;q;C |- q*;q + 1 = q*

q*;q + 1 = q*
--------

>cite commut+
which side? l

current task:
T17: C;q = C;q;C |- 1 + q*;q = q*

1 + q*;q = q*
--------

>unf

current task:
T17: C;q = C;q;C |- 1 + q*;q = q*

>cite unwindR
task completed

current task:
T7: C;q = C;q;C |- C;q*;C < C;q*

>foc

current task:
T7: C;q = C;q;C |- C;q*;C < C;q*

C;q*;C < C;q*
------

>r

current task:
T7: C;q = C;q;C |- C;q*;C < C;q*

C;q*;C < C;q*
         ----

>cite id.R r

current task:
T7: C;q = C;q;C |- C;q*;C < C;q*;1

C;q*;C < C;q*;1
         ------

>unf

current task:
T7: C;q = C;q;C |- C;q*;C < C;q*;1

>cite mono.L
ambiguous unification
specify desired bindings by number:

0: [ x=C y=q*;C z=q*;1 ]
1: [ x=C;q* y=C z=1 ]
? 1

current task:
T18: C;q = C;q;C |- C < 1

>cite <intro

current task:
T19: C;q = C;q;C |- C + 1 = 1

>cite <1
task completed

no tasks

>lib
L1: C;q = C;q;C -> C;q* = C;q*;C  (proved)
L0: B;C;p = B;C;p;C -> C;(B;p)*;~B = C;(B;p)*;~B;C;~B  (proved)
ref=: x = x  (proved)
sym: x = y -> y = x  (proved)
trans=: x = y -> y = z -> x = z  (proved)
cong+R: x = y -> x + z = y + z  (proved)
cong.L: y = z -> x;y = x;z  (proved)
cong.R: x = y -> x;z = y;z  (proved)
cong*: x = y -> x* = y*  (proved)
<intro: x + y = y -> x < y  (proved)
<elim: x < y -> x + y = y  (proved)
ref<: x < x  (proved)
antisym: x < y -> y < x -> x = y  (proved)
trans<: x < y -> y < z -> x < z  (proved)
supL: x < x + y  (proved)
supR: y < x + y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
=<: x = y -> x < y  (proved)
mono+R: x < y -> x + z < y + z  (proved)
mono.L: y < z -> x;y < x;z  (proved)
mono.R: x < y -> x;z < y;z  (proved)
mono*: x < y -> x* < y*  (proved)
commut+: x + y = y + x  (proved)
id+L: 0 + x = x  (proved)
id+R: x + 0 = x  (proved)
idemp+: x + x = x  (proved)
id.L: 1;x = x  (proved)
id.R: x;1 = x  (proved)
annihL: 0;x = 0  (proved)
annihR: x;0 = 0  (proved)
distrL: x;(y + z) = x;y + x;z  (proved)
distrR: (x + y);z = x;z + y;z  (proved)
unwindL: 1 + x;x* = x*  (proved)
unwindR: 1 + x*;x = x*  (proved)
*L: z;y + x < z -> x;y* < z  (proved)
*R: x;z + y < z -> x*;y < z  (proved)
slide: x;(y;x)* = (x;y)*;x  (proved)
denest: x*;(y;x*)* = (x + y)*  (proved)
commut.: B;C = C;B  (proved)
idemp.: B;B = B  (proved)
~~: ~~B = B  (proved)
deMorgan+: ~(B + C) = ~B;~C  (proved)
deMorgan.: ~(B;C) = ~B + ~C  (proved)
~0: ~0 = 1  (proved)
~1: ~1 = 0  (proved)
compl+: B + ~B = 1  (proved)
compl.: B;~B = 0  (proved)
<1: B + 1 = 1  (proved)
distr.L: B + C;D = (B + C);(B + D)  (proved)
distr.R: B;C + D = (B + D);(C + D)  (proved)
abs+: B + B;C = B  (proved)
abs.: B;(B + C) = B  (proved)

no tasks

>