PrintForm
Definitions
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
At:
formula
imp
falsifiable
lemma
1
1
2
1.
a:
Assignment
2.
q:
Formula
3.
r:
Formula
4.
a |
q
r
a |
r
By:
OnHyps [-1;0] (
i.UnfoldTopAb i)
Generated subgoal:
1
4.
(q
r under a) = 3
(r under a) = 3
About:
r under a) = 3
(r under a) = 3
qr a | r
i.UnfoldTopAb i)r under a) = 3 (r under a) = 3