(42steps) PrintForm Definitions formula equality Sections ClassicalProps(jlc) Doc

At: discrete Formula 1
1. x: Formula

y:Formula. Dec(x = y)
By: FormulaElimination 1
Generated subgoals:

11. Q: FormulaProp
2. x:{x:Formula| Q(x) }, y:Formula. Dec(x = y)
3. x1: Var
y:Formula. Dec(x1 = y)
21. Q: FormulaProp
2. x:{x:Formula| Q(x) }, y:Formula. Dec(x = y)
3. x: Formula
4. Q(x)
y@0:Formula. Dec(x = y@0)
31. Q: FormulaProp
2. x:{x:Formula| Q(x) }, y:Formula. Dec(x = y)
3. x1: {x:Formula| Q(x) }
4. x2: Formula
5. Q(x2)
y@0:Formula. Dec(x1x2 = y@0)
41. Q: FormulaProp
2. x:{x:Formula| Q(x) }, y:Formula. Dec(x = y)
3. x1: {x:Formula| Q(x) }
4. x2: Formula
5. Q(x2)
y@0:Formula. Dec(x1x2 = y@0)
51. Q: FormulaProp
2. x:{x:Formula| Q(x) }, y:Formula. Dec(x = y)
3. y2: {x:Formula| Q(x) }
4. y3: Formula
5. Q(y3)
y@0:Formula. Dec(y2y3 = y@0)

About:
decidableequalall

(42steps) PrintForm Definitions formula equality Sections ClassicalProps(jlc) Doc