Nuprl - Pf counter_lpower 1 1

PrintForm Definitions action sets Sections AutomataTheory Doc

At: counter lpower 1 1

1. e:
2. L: *

||e:(L0)|| = 0||e:L||

By: RW (RecUnfoldC `lpower`) 0 THEN Reduce 0

Generated subgoal:

1 ||e:nil|| = 0||e:L||

About: