Nuprl Theory sequent_falsification
(only non hidden objects are presented)
DISP
sequent_falsifiable_df
<a:Assignment:L> |
<S:Sequent:L>== <a> |
<S>
ABS
sequent_falsifiable
a |
S ==
F
S.H.a |= F
F
S.C.a |
F
THM
sequent_falsifiable_wf
a:Assignment.
S:Sequent. a |
S
THM
decidable__sequent_falsifiable
S:Sequent.
a:Assignment. Dec(a |
S)
THM
sq_stable__sequent_falsifiable
a:Assignment.
S:Sequent. SqStable(a |
S)
the other theories