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