At:
discrete Formula with rank
1
3
1
1
1
1
1
1.
x: Formula
2.
x2: Formula
3.
x3: Formula
4.
y@0: Formula
5.
x5: Formula
6.
x6: Formula
7.
x2 = x5
8.
x3 = x6
Dec(x2
x3 = x5x6)
By:
TrueCase
THEN
FormulaEquality 0
THEN
Trivial
Generated subgoals:
None
About:
