PrintForm
Definitions
elimination
Sections
ClassicalProps(jlc)
Doc
At:
formula
imp
right
sat
1
1
2
2
1.
hyp:
Formula List
2.
M:
Formula List
3.
N:
Formula List
4.
q:
Formula
5.
r:
Formula
6.
a:
Assignment
7.
a |= q
r
F
N.a |= F
a |
q
F
hyp.a |
F
a |= r
F
M.a |= F
F
N.a |= F
By:
Analyze -1
Generated subgoals:
1
7.
a |= q
r
a |
q
F
hyp.a |
F
a |= r
F
M.a |= F
F
N.a |= F
2
7.
F
N.a |= F
a |
q
F
hyp.a |
F
a |= r
F
M.a |= F
F
N.a |= F
About: