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