2. x :
k
3. y :
k
4. z :
k
5.
y = z
6.
x = y
7. x1 :
k
8.
x1 = x
9. x1 = y
x
=
if if y=
y
z ; y=z y else y fi=x z
i; if y=y z ; y=z y else y fi=z x
i; y=y z
i; y=z y
else y fi
k
k
k
y = z
x = y
k
x1 = x
x
=
if if y=y z ; y=z y else y fi=x z
i; if y=y z ; y=z y else y fi=z x
i; y=y z
i; y=z y
else y fi| By: |
y) = true) 0 THEN Reduce 0
THEN Try (BackThru Thm*  i,j: . i = j   (i=j) = true)
THEN Repeat SplitOnConclITE |
None
About:
 |  |  |  |  |  |  |  |