Nuprl - Pf en_ubound 1

PrintForm Definitions exponent Sections AutomataTheory Doc

At: en ubound 1

1. n:
2. l: n*

en(nil) < (n0)

By: RecUnfold `en` 0 THEN RecUnfold `exp` 0 THEN Reduce 0

Generated subgoals:

None

About: