Nuprl Lemma : prop-rule-realizer

Nuprl Lemma : prop-rule-realizer_wf

[S:LimitedType].

[T:Type].

[P:S

].

[f:Id

T

{v:S|

P[v]} ].

[g:T

(Id List)].

[hdr:Name].

[pr:x:Id fp-> {dfp:DataflowProgram(Message)| df-program-type(dfp) = (T + Top)} ].
(prop-rule-realizer(pr;S;f;g;hdr)

Component List)

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{}[hdr:Name]. \mforall{}[pr:x:Id fp-> \{dfp:DataflowProgram(Message)| df-program-type(dfp) = (T + Top)\} ]. (prop-rule-realizer(pr;S;f;g;hdr) \mmember{} Component List) Date html generated: 2012_02_20-PM-07_50_48 Last ObjectModification: 2010_11_12-PM-08_51_43 Home Index