This example gives a proof of an abstract version
of the Hoare assignment rule.

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

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

current task:
T0: B;p = p;C |- ~B;p;C + B;p;~C = 0

>pub ~B p C + B p ~C = 0 -> B p = p C
L1: ~B;p;C + B;p;~C = 0 -> B;p = p;C  (1 task)

current task:
T1: ~B;p;C + B;p;~C = 0 |- B;p = p;C

>get L0
L0: B;p = p;C -> ~B;p;C + B;p;~C = 0  (1 task)

current task:
T0: B;p = p;C |- ~B;p;C + B;p;~C = 0

>foc

current task:
T0: B;p = p;C |- ~B;p;C + B;p;~C = 0

~B;p;C + B;p;~C = 0
---------------

>d d r

current task:
T0: B;p = p;C |- ~B;p;C + B;p;~C = 0

~B;p;C + B;p;~C = 0
   ---

>use A0 r

current task:
T0: B;p = p;C |- ~B;B;p + B;p;~C = 0

~B;B;p + B;p;~C = 0
   ---

>l

current task:
T0: B;p = p;C |- ~B;B;p + B;p;~C = 0

~B;B;p + B;p;~C = 0
----

>cite compl. l
citation does not apply

current task:
T0: B;p = p;C |- ~B;B;p + B;p;~C = 0

~B;B;p + B;p;~C = 0
----

>cite commut. l

current task:
T0: B;p = p;C |- B;~B;p + B;p;~C = 0

B;~B;p + B;p;~C = 0
----

>cite compl. l

current task:
T0: B;p = p;C |- 0;p + B;p;~C = 0

0;p + B;p;~C = 0
-

>u

current task:
T0: B;p = p;C |- 0;p + B;p;~C = 0

0;p + B;p;~C = 0
---

>cite annihL l

current task:
T0: B;p = p;C |- 0 + B;p;~C = 0

0 + B;p;~C = 0
-

>r d

current task:
T0: B;p = p;C |- 0 + B;p;~C = 0

0 + B;p;~C = 0
    ---

>use A0 l

current task:
T0: B;p = p;C |- 0 + p;C;~C = 0

0 + p;C;~C = 0
    ---

>r

current task:
T0: B;p = p;C |- 0 + p;C;~C = 0

0 + p;C;~C = 0
      ----

>cite compl. l

current task:
T0: B;p = p;C |- 0 + p;0 = 0

0 + p;0 = 0
      -

>u

current task:
T0: B;p = p;C |- 0 + p;0 = 0

0 + p;0 = 0
    ---

>cite annihR l

current task:
T0: B;p = p;C |- 0 + 0 = 0

0 + 0 = 0
    -

>unf

current task:
T0: B;p = p;C |- 0 + 0 = 0

>cite id+R

no tasks

>get L1
L1: ~B;p;C + B;p;~C = 0 -> B;p = p;C  (1 task)

current task:
T1: ~B;p;C + B;p;~C = 0 |- B;p = p;C

>cut ~B p C = 0

current task:
T2: ~B;p;C + B;p;~C = 0, ~B;p;C = 0 |- B;p = p;C

>cut B p ~C = 0

current task:
T4: ~B;p;C + B;p;~C = 0, ~B;p;C = 0, B;p;~C = 0 |- B;p = p;C

>tasks
T4: ~B;p;C + B;p;~C = 0, ~B;p;C = 0, B;p;~C = 0 |- B;p = p;C
T5: ~B;p;C + B;p;~C = 0, ~B;p;C = 0 |- B;p;~C = 0
T3: ~B;p;C + B;p;~C = 0 |- ~B;p;C = 0

current task:
T4: ~B;p;C + B;p;~C = 0, ~B;p;C = 0, B;p;~C = 0 |- B;p = p;C

>ignore A0

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p = p;C

>undo

current task:
T4: ~B;p;C + B;p;~C = 0, ~B;p;C = 0, B;p;~C = 0 |- B;p = p;C

>redo

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p = p;C

>get T5

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

>ignore A1

current task:
T5: ~B;p;C + B;p;~C = 0 |- B;p;~C = 0

>tasks
T5: ~B;p;C + B;p;~C = 0 |- B;p;~C = 0
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p = p;C
T3: ~B;p;C + B;p;~C = 0 |- ~B;p;C = 0

current task:
T5: ~B;p;C + B;p;~C = 0 |- B;p;~C = 0

>foc

current task:
T5: ~B;p;C + B;p;~C = 0 |- B;p;~C = 0

B;p;~C = 0
------

>cite id+R r

current task:
T5: ~B;p;C + B;p;~C = 0 |- B;p;~C + 0 = 0

B;p;~C + 0 = 0
----------

>unf

current task:
T5: ~B;p;C + B;p;~C = 0 |- B;p;~C + 0 = 0

>cite <elim

current task:
T6: ~B;p;C + B;p;~C = 0 |- B;p;~C < 0

>cite trans<
y=? ~B p C + B p ~C

current task:
T7: ~B;p;C + B;p;~C = 0 |- B;p;~C < ~B;p;C + B;p;~C

>cite supR
task completed

current task:
T8: ~B;p;C + B;p;~C = 0 |- ~B;p;C + B;p;~C < 0

>cite =<

current task:
T9: ~B;p;C + B;p;~C = 0 |- ~B;p;C + B;p;~C = 0

>use A0
task completed

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p = p;C

>get T3

current task:
T3: ~B;p;C + B;p;~C = 0 |- ~B;p;C = 0

>foc

current task:
T3: ~B;p;C + B;p;~C = 0 |- ~B;p;C = 0

~B;p;C = 0
------

>cite id+R r

current task:
T3: ~B;p;C + B;p;~C = 0 |- ~B;p;C + 0 = 0

~B;p;C + 0 = 0
----------

>unf

current task:
T3: ~B;p;C + B;p;~C = 0 |- ~B;p;C + 0 = 0

>cite <elim

current task:
T10: ~B;p;C + B;p;~C = 0 |- ~B;p;C < 0

>cite trans<
y=? ~B p C + B p ~C

current task:
T11: ~B;p;C + B;p;~C = 0 |- ~B;p;C < ~B;p;C + B;p;~C

>cite supL
task completed

current task:
T12: ~B;p;C + B;p;~C = 0 |- ~B;p;C + B;p;~C < 0

>cite =<

current task:
T13: ~B;p;C + B;p;~C = 0 |- ~B;p;C + B;p;~C = 0

>use A0
task completed

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p = p;C

>foc

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p = p;C

B;p = p;C
---

>cite id.R r

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;1 = p;C

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

>d d r r

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;1 = p;C

B;p;1 = p;C
    -

>cite compl+ r
B=? C

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;(C + ~C) = p;C

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

>u

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;(C + ~C) = p;C

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

>cite distrL l

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;C + B;p;~C = p;C

B;p;C + B;p;~C = p;C
--------------

>d r

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;C + B;p;~C = p;C

B;p;C + B;p;~C = p;C
        ------

>use A1 l

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;C + 0 = p;C

B;p;C + 0 = p;C
        -

>u

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;C + 0 = p;C

B;p;C + 0 = p;C
---------

>cite id+R l

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;C = p;C

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

>r

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;C = p;C

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

>cite id.L r

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;C = 1;p;C

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

>d d

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;C = 1;p;C

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

>cite compl+ r
B=? B

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;C = (B + ~B);p;C

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

>u u

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;C = (B + ~B);p;C

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

>cite distrR l

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;C = B;p;C + ~B;p;C

B;p;C = B;p;C + ~B;p;C
        --------------

>d r

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;C = B;p;C + ~B;p;C

B;p;C = B;p;C + ~B;p;C
                ------

>use A0 l

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;C = B;p;C + 0

B;p;C = B;p;C + 0
                -

>u

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;C = B;p;C + 0

B;p;C = B;p;C + 0
        ---------

>cite id+R l

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;C = B;p;C

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

>unf

current task:
T4: ~B;p;C = 0, B;p;~C = 0 |- B;p;C = B;p;C

>cite ref=
task completed

no tasks

>