Nuprl Lemma : until-class-nlp
A,B:ValueAllType'.
[X:EClass(A)]. [Y:EClass(B)].
(NormalLProgrammable'(A;X) 
NormalLProgrammable'(B;Y) NormalLProgrammable'(A;(X until Y)))
Proof not projected
Definitions occuring in Statement :
Message: Message,
normal-locally-programmable: NormalLProgrammable(A;X),
until-class: (X until Y),
eclass: EClass(A[eo; e]),
uall: [x:A]. B[x],
all: x:A. B[x],
implies: P Q,
vatype: ValueAllType
Definitions :
label: ...$L... t,
prop: 
,
member: t 
T,
implies: P Q,
uall: [x:A]. B[x],
vatype: ValueAllType,
all: x:A. B[x]
Lemmas :
vatype_wf,
eclass_wf2,
normal-locally-programmable_wf,
squash_wf,
Message-inhabited,
Message_wf,
until-class-locally-programmable-ext
\mforall{}A,B:ValueAllType'.
\mforall{}[X:EClass(A)]. \mforall{}[Y:EClass(B)].
(NormalLProgrammable'(A;X) {}\mRightarrow{} NormalLProgrammable'(B;Y) {}\mRightarrow{} NormalLProgrammable'(A;(X until Y)))
Date html generated:
2012_02_20-PM-02_51_11
Last ObjectModification:
2012_01_29-PM-03_17_23
Home
Index