(2steps)
PrintForm
Definitions
Kleene
Sections
ClassicalProps(jlc)
Doc
At:
K
or
equal
Three
2
1
1.
x:
2.
y:
3.
x
y = 3
x = 3
y = 3
By:
ThreeInd 2 THEN ThreeInd 1 THEN AbReduce 1 THENL [ThreeNEQ 1;ThreeNEQ 1;Choose [1];ThreeNEQ 1;ThreeNEQ 1;Choose [1];Choose [2];Choose [2];Choose [2]]
Generated subgoals:
None
About:
(2steps)
PrintForm
Definitions
Kleene
Sections
ClassicalProps(jlc)
Doc