PrintForm Definitions valuation Sections ClassicalProps(jlc) Doc

At: valuation wf 1 1
1. F: Formula

a:Assignment. (F under a)
By:
FormulaElimination 1
THEN
Analyze 0
THEN
Reduce 0
Generated subgoals:

11. Q: FormulaProp
2. F:{F:Formula| Q(F) }, a:Assignment. (F under a)
3. x: Var
4. a: Assignment
a(x)
21. Q: FormulaProp
2. F:{F:Formula| Q(F) }, a:Assignment. (F under a)
3. x: Formula
4. Q(x)
5. a: Assignment
(x under a)
31. Q: FormulaProp
2. F:{F:Formula| Q(F) }, a:Assignment. (F under a)
3. x1: {F:Formula| Q(F) }
4. x2: Formula
5. Q(x2)
6. a: Assignment
(x1 under a) (x2 under a)
41. Q: FormulaProp
2. F:{F:Formula| Q(F) }, a:Assignment. (F under a)
3. x1: {F:Formula| Q(F) }
4. x2: Formula
5. Q(x2)
6. a: Assignment
(x1 under a) (x2 under a)
51. Q: FormulaProp
2. F:{F:Formula| Q(F) }, a:Assignment. (F under a)
3. y2: {F:Formula| Q(F) }
4. y3: Formula
5. Q(y3)
6. a: Assignment
(y2 under a) (y3 under a)

About:
allmemberapply