At:
discrete Formula with rank
1
5
1
1
1
1
1
1.
x: Formula
2.
y1: Formula
3.
y2: Formula
4.
y@0: Formula
5.
y3: Formula
6.
y4: Formula
7.
y1 = y3
8.
y2 = y4
Dec(y1
y2 = y3y4)
By:
TrueCase
THEN
FormulaEquality 0
THEN
Trivial
Generated subgoals:
None
About:
