PrintForm
Definitions
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
At:
formula
imp
sat
lemma
1
1
1
1
1.
a:
Assignment
2.
q:
Formula
3.
r:
Formula
4.
(q under a)
(r under a) = 3
a |
q
a |= r
By:
MoveToConcl -1
THEN
GenConcl ((q under a) = n)
THEN
GenConcl ((r under a) = m)
THEN
UnivCD
Generated subgoal:
1
4.
n:
5.
(q under a) = n
6.
m:
7.
(r under a) = m
8.
n
m = 3
a |
q
a |= r
About:
m = 3
a |
q 
a |= r (r under a) = 3 a | q a |= r m = 3 a | q a |= r 
