(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:
equalor

(2steps) PrintForm Definitions Kleene Sections ClassicalProps(jlc) Doc