PrintForm
Definitions
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
At:
formula
and
falsifiable
lemma
1
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
