PrintForm
Definitions
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
At:
assignment
monotone
1
1
1
1
1.
f:
Formula
2.
x:
Var
3.
a:
Assignment
4.
a':
Assignment
5.
a' extends a
6.
a |=
x
a' |=
x
By:
Inst
Thm*
a,a':Assignment. a' extends a
(
x:Var.
a(x) = 3
a(x) = a'(x)) [a;a';x]
Generated subgoals:
1
a(x) = 3
2
7.
a(x) = a'(x)
a' |=
x
About:
a(x) = 3
a' |= 
x
x a' |= x 
a,a':Assignment. a' extends a 
(x:Var. a(x) = 3 a(x) = a'(x))
[a;a';x] a(x) = 3 a' |= x 
