Nuprl Lemma : propagation-rule-realizable

S:LimitedType.

T:Type.

P:S

.

f:Id

T

{v:S|

P[v]} .

g:T

(Id List).

h:Name.

A:EClass'(T).
(Programmable'(T;A)

(

Cs:Component List. assuming(env,r.reliable-env(env; r)) mk-init-sys(Cs) |= es.A

f

baseclass(h; S; v.P[v])@g))

Proof not projected

Error : references

\mforall{}S:LimitedType. \mforall{}T:Type. \mforall{}P:S {}\mrightarrow{} \mBbbB{}. \mforall{}f:Id {}\mrightarrow{} T {}\mrightarrow{} \{v:S| \muparrow{}P[v]\} . \mforall{}g:T {}\mrightarrow{} (Id List). \mforall{}h:Name. \mforall{}A:EClass'(T). (Programmable'(T;A) {}\mRightarrow{} (\mexists{}Cs:Component List assuming(env,r.reliable-env(env; r)) mk-init-sys(Cs) |= es.A {}f\mRightarrow{} baseclass(h; S; v.P[v])@g)) Date html generated: 2012_02_20-PM-07_50_49 Last ObjectModification: 2010_08_23-PM-01_04_03 Home Index