Nuprl Lemma : null-process

{

[M:Type

Type]. (null-process()

lvProcess(lp.M[lp])) }

{ Proof }

Definitions occuring in Statement : lvProcess: lvProcess(lp.M[lp]), uall:

[x:A]. B[x], so_apply: x[s], member: t

T, function: x:A

B[x], universe: Type
Definitions : uall:

[x:A]. B[x], member: t

T, lvProcess: lvProcess(lp.M[lp]), so_apply: x[s], nat:

, le: A

B, not:

A, implies: P

Q, false: False, so_lambda:

x.t[x], prop:

Lemmas : le_wf, lvprocess_wf, null-process_wf

\mforall{}[M:Type {}\mrightarrow{} Type]. (null-process() \mmember{} lvProcess(lp.M[lp])) Date html generated: 2011_08_17-PM-06_38_07 Last ObjectModification: 2011_06_18-PM-12_02_21 Home Index