Origin
Sections
ClassicalProps(jlc)
Doc
normalization
Nuprl Section: normalization - The normalization lemma.
Selected Objects
THM
normalization_lemma
G:Sequent.
L:Sequent List.
s
L.(
(s) = 0) & (
s
L.|= s
|= G ) & (
a:Assignment.
s
L.a |
s
a |
G)
G:Sequent.
L:Sequent List. s
L.(
(s) = 0) & (sL.|= s 
|= G ) & (a:Assignment. sL.a |
s a | G)G:Sequent.
L:Sequent List. sL.((s) = 0) & (sL.|= s |= G ) & (a:Assignment. sL.a | s a | G)