42 lines
318 B
Text
42 lines
318 B
Text
a0 --> a3
|
|
| |
|
|
| |
|
|
v v
|
|
a1 --> a4
|
|
|
|
|
|
(Abs a3) >>* a2
|
|
|
|
Abs a0 ----> (Abs a3) >>* a2
|
|
| |
|
|
| |
|
|
Abs a1 ----> (Abs a4) >>*
|
|
|
|
|
|
a0 >> a1
|
|
| |
|
|
| |
|
|
v v
|
|
b0 >> b1
|
|
|
|
|
|
prov x (x, x)
|
|
|
|
prov x b
|
|
|
|
|
|
a => b
|
|
|
|
prov x a
|
|
|
|
prov y b
|
|
|
|
prov x c
|
|
prov y c
|
|
|
|
extract c = x
|
|
extract c = y
|
|
|
|
prov x b
|
|
|
|
pr
|