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