PrintForm
Definitions
sequent
valid
Sections
ClassicalProps(jlc)
Doc
At:
formula
valid
iff
sequent
valid
1
1
2
1
1
1.
F:
Formula
2.
|= F
3.
a:
Assignment
4.
True
5.
a |
F
6.
True
a |= < nil,[F] >
By:
UnfoldTopAb 2
Generated subgoal:
1
2.
a:Full(F). a |= F
3.
a:
Assignment
4.
True
5.
a |
F
6.
True
a |= < nil,[F] >
About:
a:Full(F). a |= F 
F
a |= < nil,[F] > F a |= < nil,[F] > a:Full(F). a |= F F a |= < nil,[F] > 
