PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

At: zero rank all vars 1 1 1 1 1 1 1 2 1 3

1. z: Formula
2. x1: Formula
3. x2: Formula

(x1)+(x2)+1 = 0 (v:Var. x1x2 = v)

By: GenConclOnAps

Generated subgoals:

None


About:
impliesequalintaddapplynatural_numberexists