% ./kat.cmd 
GenetiX hacked version
KAT interactive theorem prover version 03.9.12
>publish p;q = q;r -> p*;q = q;r*
L0: p;q = q;r -> p*;q = q;r*  (1 task)

Suggested Citations
-------------------
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
antisym: x < y -> y < x -> x = y  (proved)

current task:
T0:
     p;q = q;r
     -------------------------
     p*;q = q;r*

p*;q = q;r*
>cite antisym
cite antisym

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
*R: x;z + y < z -> x*;y < z  (axiom)
=<: x = y -> x < y  (proved)
trans<: x < y -> y < z -> x < z  (proved)
mono.LR: x < y -> z < w -> x;z < y;w  (proved)
app*R: x < y -> x < y;z*  (proved)

current task:
T3:
     p;q = q;r
     -------------------------
     p*;q < q;r*

p*;q < q;r*
>cite *R
cite *R

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
app*R: x < y -> x < y;z*  (proved)

current task:
T5:
     p;q = q;r
     -------------------------
     p;q;r* + q < q;r*

p;q;r* + q < q;r*
>focus

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
app*R: x < y -> x < y;z*  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong+R: x = y -> x + z = y + z  (axiom)
<elim: x < y -> x + y = y  (axiom)
commut+: x + y = y + x  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
cong+L: y = z -> x + y = x + z  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0: x = 0 -> y = 0 -> x + y = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T5:
     p;q = q;r
     -------------------------
     p;q;r* + q < q;r*

p;q;r* + q < q;r*
----------
>right

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
app*R: x < y -> x < y;z*  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong.L: y = z -> x;y = x;z  (axiom)
cong.R: x = y -> x;z = y;z  (axiom)
<elim: x < y -> x + y = y  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)
AL2: v;u = 0 -> w;u = 0 -> w;(u + v)* = w;v*  (proved)

current task:
T5:
     p;q = q;r
     -------------------------
     p;q;r* + q < q;r*

p;q;r* + q < q;r*
             ----
>down

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
app*R: x < y -> x < y;z*  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
<elim: x < y -> x + y = y  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T5:
     p;q = q;r
     -------------------------
     p;q;r* + q < q;r*

p;q;r* + q < q;r*
             -
>right

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
app*R: x < y -> x < y;z*  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong*: x = y -> x* = y*  (axiom)
<elim: x < y -> x + y = y  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
unwindL: 1 + x;x* = x*  (axiom)
unwindR: 1 + x*;x = x*  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T5:
     p;q = q;r
     -------------------------
     p;q;r* + q < q;r*

p;q;r* + q < q;r*
               --
>cite unwindL
which side? r
cite unwindL

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong+R: x = y -> x + z = y + z  (axiom)
<elim: x < y -> x + y = y  (axiom)
commut+: x + y = y + x  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
unwindL: 1 + x;x* = x*  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
cong+L: y = z -> x + y = x + z  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0: x = 0 -> y = 0 -> x + y = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T6:
     p;q = q;r
     -------------------------
     p;q;r* + q < q;(1 + r;r*)

p;q;r* + q < q;(1 + r;r*)
               ----------
>up

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong.L: y = z -> x;y = x;z  (axiom)
cong.R: x = y -> x;z = y;z  (axiom)
<elim: x < y -> x + y = y  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
distrL: x;(y + z) = x;y + x;z  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T6:
     p;q = q;r
     -------------------------
     p;q;r* + q < q;(1 + r;r*)

p;q;r* + q < q;(1 + r;r*)
             ------------
>cite distrL l
cite distrL

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
monosupR: x < z -> x < y + z  (proved)
monosupL: x < y -> x < y + z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong+R: x = y -> x + z = y + z  (axiom)
<elim: x < y -> x + y = y  (axiom)
commut+: x + y = y + x  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
distrL: x;(y + z) = x;y + x;z  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
cong+L: y = z -> x + y = x + z  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0: x = 0 -> y = 0 -> x + y = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T7:
     p;q = q;r
     -------------------------
     p;q;r* + q < q;1 + q;r;r*

p;q;r* + q < q;1 + q;r;r*
             ------------
>down

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
monosupR: x < z -> x < y + z  (proved)
monosupL: x < y -> x < y + z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong.L: y = z -> x;y = x;z  (axiom)
cong.R: x = y -> x;z = y;z  (axiom)
<elim: x < y -> x + y = y  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC3: p = p;~C -> p;C = 0  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T7:
     p;q = q;r
     -------------------------
     p;q;r* + q < q;1 + q;r;r*

p;q;r* + q < q;1 + q;r;r*
             ---
>cite id.R l
cite id.R

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
monosupR: x < z -> x < y + z  (proved)
monosupL: x < y -> x < y + z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
<elim: x < y -> x + y = y  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T8:
     p;q = q;r
     -------------------------
     p;q;r* + q < q + q;r;r*

p;q;r* + q < q + q;r;r*
             -
>unfocus

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
monosupR: x < z -> x < y + z  (proved)
monosupL: x < y -> x < y + z  (proved)

current task:
T8:
     p;q = q;r
     -------------------------
     p;q;r* + q < q + q;r;r*

p;q;r* + q < q + q;r;r*
>focus

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
monosupR: x < z -> x < y + z  (proved)
monosupL: x < y -> x < y + z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong+R: x = y -> x + z = y + z  (axiom)
<elim: x < y -> x + y = y  (axiom)
commut+: x + y = y + x  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
cong+L: y = z -> x + y = x + z  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0: x = 0 -> y = 0 -> x + y = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T8:
     p;q = q;r
     -------------------------
     p;q;r* + q < q + q;r;r*

p;q;r* + q < q + q;r;r*
----------
>right

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
monosupR: x < z -> x < y + z  (proved)
monosupL: x < y -> x < y + z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong+R: x = y -> x + z = y + z  (axiom)
<elim: x < y -> x + y = y  (axiom)
commut+: x + y = y + x  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
cong+L: y = z -> x + y = x + z  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0: x = 0 -> y = 0 -> x + y = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T8:
     p;q = q;r
     -------------------------
     p;q;r* + q < q + q;r;r*

p;q;r* + q < q + q;r;r*
             ----------
>cite commut+ r
cite commut+

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
mono+R: x < y -> x + z < y + z  (proved)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
monosupR: x < z -> x < y + z  (proved)
monosupL: x < y -> x < y + z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong+R: x = y -> x + z = y + z  (axiom)
<elim: x < y -> x + y = y  (axiom)
commut+: x + y = y + x  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
cong+L: y = z -> x + y = x + z  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0: x = 0 -> y = 0 -> x + y = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T9:
     p;q = q;r
     -------------------------
     p;q;r* + q < q;r;r* + q

p;q;r* + q < q;r;r* + q
             ----------
>unfocus

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
mono+R: x < y -> x + z < y + z  (proved)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
monosupR: x < z -> x < y + z  (proved)
monosupL: x < y -> x < y + z  (proved)

current task:
T9:
     p;q = q;r
     -------------------------
     p;q;r* + q < q;r;r* + q

p;q;r* + q < q;r;r* + q
>cite mono+R
cite mono+R

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
*L: z;y + x < z -> x;y* < z  (axiom)
mono.R: x < y -> x;z < y;z  (proved)
=<: x = y -> x < y  (proved)
trans<: x < y -> y < z -> x < z  (proved)
mono.LR: x < y -> z < w -> x;z < y;w  (proved)
app*R: x < y -> x < y;z*  (proved)

current task:
T10:
     p;q = q;r
     -------------------------
     p;q;r* < q;r;r*

p;q;r* < q;r;r*
>cite mono.R
cite mono.R

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
trans<: x < y -> y < z -> x < z  (proved)
mono.LR: x < y -> z < w -> x;z < y;w  (proved)

current task:
T11:
     p;q = q;r
     -------------------------
     p;q < q;r

p;q < q;r
>cite =<
cite =<

Suggested Citations
-------------------
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
antisym: x < y -> y < x -> x = y  (proved)

current task:
T12:
     p;q = q;r
     -------------------------
     p;q = q;r

p;q = q;r
>use A0
cite A0

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
*L: z;y + x < z -> x;y* < z  (axiom)
=<: x = y -> x < y  (proved)
trans<: x < y -> y < z -> x < z  (proved)
mono.LR: x < y -> z < w -> x;z < y;w  (proved)
app*L: y < z -> y < x*;z  (proved)

current task:
T15:
     p;q = q;r
     -------------------------
     q;r* < p*;q

q;r* < p*;q
>cite *L
cite *L

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
app*L: y < z -> y < x*;z  (proved)

current task:
T25:
     p;q = q;r
     -------------------------
     p*;q;r + q < p*;q

p*;q;r + q < p*;q
>focus

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
app*L: y < z -> y < x*;z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong+R: x = y -> x + z = y + z  (axiom)
<elim: x < y -> x + y = y  (axiom)
commut+: x + y = y + x  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
cong+L: y = z -> x + y = x + z  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0: x = 0 -> y = 0 -> x + y = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T25:
     p;q = q;r
     -------------------------
     p*;q;r + q < p*;q

p*;q;r + q < p*;q
----------
>right

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
app*L: y < z -> y < x*;z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong.L: y = z -> x;y = x;z  (axiom)
cong.R: x = y -> x;z = y;z  (axiom)
<elim: x < y -> x + y = y  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)
AL1: u;v = 0 -> u;w = 0 -> (u + v)*;w = v*;w  (proved)

current task:
T25:
     p;q = q;r
     -------------------------
     p*;q;r + q < p*;q

p*;q;r + q < p*;q
             ----
>down

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
app*L: y < z -> y < x*;z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong*: x = y -> x* = y*  (axiom)
<elim: x < y -> x + y = y  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
unwindL: 1 + x;x* = x*  (axiom)
unwindR: 1 + x*;x = x*  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T25:
     p;q = q;r
     -------------------------
     p*;q;r + q < p*;q

p*;q;r + q < p*;q
             --
>cite unwindR
which side? r
cite unwindR

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong+R: x = y -> x + z = y + z  (axiom)
<elim: x < y -> x + y = y  (axiom)
commut+: x + y = y + x  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
unwindR: 1 + x*;x = x*  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
cong+L: y = z -> x + y = x + z  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0: x = 0 -> y = 0 -> x + y = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T26:
     p;q = q;r
     -------------------------
     p*;q;r + q < (1 + p*;p);q

p*;q;r + q < (1 + p*;p);q
             ----------
>up

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong.L: y = z -> x;y = x;z  (axiom)
cong.R: x = y -> x;z = y;z  (axiom)
<elim: x < y -> x + y = y  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
distrR: (x + y);z = x;z + y;z  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T26:
     p;q = q;r
     -------------------------
     p*;q;r + q < (1 + p*;p);q

p*;q;r + q < (1 + p*;p);q
             ------------
>cite distrR l
cite distrR

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
monosupR: x < z -> x < y + z  (proved)
monosupL: x < y -> x < y + z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong+R: x = y -> x + z = y + z  (axiom)
<elim: x < y -> x + y = y  (axiom)
commut+: x + y = y + x  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
distrR: (x + y);z = x;z + y;z  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
cong+L: y = z -> x + y = x + z  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0: x = 0 -> y = 0 -> x + y = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T27:
     p;q = q;r
     -------------------------
     p*;q;r + q < 1;q + p*;p;q

p*;q;r + q < 1;q + p*;p;q
             ------------
>cite commut+ l
cite commut+

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
monosupR: x < z -> x < y + z  (proved)
monosupL: x < y -> x < y + z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong+R: x = y -> x + z = y + z  (axiom)
<elim: x < y -> x + y = y  (axiom)
commut+: x + y = y + x  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
distrR: (x + y);z = x;z + y;z  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
cong+L: y = z -> x + y = x + z  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0: x = 0 -> y = 0 -> x + y = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T28:
     p;q = q;r
     -------------------------
     p*;q;r + q < p*;p;q + 1;q

p*;q;r + q < p*;p;q + 1;q
             ------------
>down

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
monosupR: x < z -> x < y + z  (proved)
monosupL: x < y -> x < y + z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong.L: y = z -> x;y = x;z  (axiom)
cong.R: x = y -> x;z = y;z  (axiom)
<elim: x < y -> x + y = y  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)
AL1: u;v = 0 -> u;w = 0 -> (u + v)*;w = v*;w  (proved)

current task:
T28:
     p;q = q;r
     -------------------------
     p*;q;r + q < p*;p;q + 1;q

p*;q;r + q < p*;p;q + 1;q
             ------
>right

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
monosupR: x < z -> x < y + z  (proved)
monosupL: x < y -> x < y + z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
cong.L: y = z -> x;y = x;z  (axiom)
cong.R: x = y -> x;z = y;z  (axiom)
<elim: x < y -> x + y = y  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
Bp3: p = ~B;p -> B;p = 0  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T28:
     p;q = q;r
     -------------------------
     p*;q;r + q < p*;p;q + 1;q

p*;q;r + q < p*;p;q + 1;q
                      ---
>cite id.L l
cite id.L

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
mono+R: x < y -> x + z < y + z  (proved)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
monosupR: x < z -> x < y + z  (proved)
monosupL: x < y -> x < y + z  (proved)

Focused Citations
-------------------
ref=: x = x  (axiom)
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
<elim: x < y -> x + y = y  (axiom)
id+R: x + 0 = x  (axiom)
idemp+: x + x = x  (axiom)
id.L: 1;x = x  (axiom)
id.R: x;1 = x  (axiom)
antisym: x < y -> y < x -> x = y  (proved)
id+L: 0 + x = x  (proved)
Bp2: ~B;p = 0 -> p = B;p  (proved)
Bp4: B;p = 0 -> p = ~B;p  (proved)
pC4: p;C = 0 -> p = p;~C  (proved)
pC2: p;~C = 0 -> p = p;C  (proved)
<=: x < 0 -> x = 0  (proved)
sup0L: x + y = 0 -> x = 0  (proved)
sup0R: x + y = 0 -> y = 0  (proved)

current task:
T29:
     p;q = q;r
     -------------------------
     p*;q;r + q < p*;p;q + q

p*;q;r + q < p*;p;q + q
                      -
>unfocus

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
mono+R: x < y -> x + z < y + z  (proved)
=<: x = y -> x < y  (proved)
sup: x < z -> y < z -> x + y < z  (proved)
trans<: x < y -> y < z -> x < z  (proved)
monosupR: x < z -> x < y + z  (proved)
monosupL: x < y -> x < y + z  (proved)

current task:
T29:
     p;q = q;r
     -------------------------
     p*;q;r + q < p*;p;q + q

p*;q;r + q < p*;p;q + q
>cite mono+R
cite mono+R

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
*R: x;z + y < z -> x*;y < z  (axiom)
mono.L: y < z -> x;y < x;z  (proved)
=<: x = y -> x < y  (proved)
trans<: x < y -> y < z -> x < z  (proved)
mono.LR: x < y -> z < w -> x;z < y;w  (proved)
app*L: y < z -> y < x*;z  (proved)

current task:
T30:
     p;q = q;r
     -------------------------
     p*;q;r < p*;p;q

p*;q;r < p*;p;q
>cite mono.L
cite mono.L

Suggested Citations
-------------------
<intro: x + y = y -> x < y  (axiom)
=<: x = y -> x < y  (proved)
trans<: x < y -> y < z -> x < z  (proved)
mono.LR: x < y -> z < w -> x;z < y;w  (proved)

current task:
T31:
     p;q = q;r
     -------------------------
     q;r < p;q

q;r < p;q
>cite =<
cite =<

Suggested Citations
-------------------
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
antisym: x < y -> y < x -> x = y  (proved)

current task:
T32:
     p;q = q;r
     -------------------------
     q;r = p;q

q;r = p;q
>cite sym
cite sym

Suggested Citations
-------------------
sym: x = y -> y = x  (axiom)
trans=: x = y -> y = z -> x = z  (axiom)
antisym: x < y -> y < x -> x = y  (proved)

current task:
T33:
     p;q = q;r
     -------------------------
     p;q = q;r

p;q = q;r
>use A0
cite A0

no tasks
>verify
cite antisym
cite *R
cite unwindL
cite distrL
cite id.R
cite commut+
cite mono+R
cite mono.R
cite =<
cite A0
cite *L
cite unwindR
cite distrR
cite commut+
cite id.L
cite mono+R
cite mono.L
cite =<
cite sym
cite A0
Proof verified.

no tasks
>rename bisimulation

no tasks
>save bisimulation.xml

no tasks
>dump bisimulation.kat
cite antisym
cite *R
cite unwindL
cite distrL
cite id.R
cite commut+
cite mono+R
cite mono.R
cite =<
cite A0
cite *L
cite unwindR
cite distrR
cite commut+
cite id.L
cite mono+R
cite mono.L
cite =<
cite sym
cite A0

no tasks
>export bisimulation.tex
cite antisym
cite *R
cite unwindL
cite distrL
cite id.R
cite commut+
cite mono+R
cite mono.R
cite =<
cite A0
cite *L
cite unwindR
cite distrR
cite commut+
cite id.L
cite mono+R
cite mono.L
cite =<
cite sym
cite A0
Proof verified.

no tasks
>