PrintForm
Definitions
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
At:
assignment
monotone
1
1
1
2
2
1.
f:
Formula
2.
x:
Var
3.
a:
Assignment
4.
a':
Assignment
5.
a' extends a
6.
a |
x
7.
a(x) = a'(x)
a' |
x
By:
OnHyps [-2;0] (
i.UnfoldTopAb i THEN Reduce i)
Generated subgoal:
1
6.
a(x) = 3
7.
a(x) = a'(x)
a'(x) = 3
About:
a'(x) = 3
x
a' | x
i.UnfoldTopAb i THEN Reduce i) a'(x) = 3
