PrintForm
Definitions
elimination
Sections
ClassicalProps(jlc)
Doc
At:
formula
not
left
sat
2
1
1.
concl:
Formula List
2.
M:
Formula List
3.
N:
Formula List
4.
f2:
Formula
5.
a:
Assignment
6.
F
M.a |
F
a |
f2
F
N.a |
F
F
concl.a |= F
F
M.a |
F
F
N.a |
F
a |= f2
F
concl.a |= F
By:
Analyze -1
Generated subgoals:
1
6.
F
M.a |
F
a |
f2
F
N.a |
F
F
M.a |
F
F
N.a |
F
a |= f2
F
concl.a |= F
2
6.
F
concl.a |= F
F
M.a |
F
F
N.a |
F
a |= f2
F
concl.a |= F
About: