Nuprl Lemma : fifo-information-flow_wf
∀[Info,T:Type]. ∀[S:Id List]. ∀[F:information-flow(T;S)]. ∀[es:EO+(Info)]. ∀[In,X:EClass(T)]. ∀[f:sys-antecedent(es;X)].
  (fifo-information-flow(es;T;S;F;In;X;f) ∈ ℙ)
Proof
Definitions occuring in Statement : 
fifo-information-flow: fifo-information-flow(es;T;S;F;In;X;f)
, 
sys-antecedent: sys-antecedent(es;Sys)
, 
eclass: EClass(A[eo; e])
, 
event-ordering+: EO+(Info)
, 
information-flow: information-flow(T;S)
, 
Id: Id
, 
list: T List
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
member: t ∈ T
, 
universe: Type
Lemmas : 
solves-information-flow_wf, 
all_wf, 
es-E-interface_wf, 
es-interface-subtype_rel2, 
es-E_wf, 
event-ordering+_subtype, 
event-ordering+_wf, 
top_wf, 
not_wf, 
equal_wf, 
es-locl_wf, 
Id_wf, 
es-loc_wf, 
sys-antecedent_wf, 
eclass_wf, 
information-flow_wf, 
list_wf
Latex:
\mforall{}[Info,T:Type].  \mforall{}[S:Id  List].  \mforall{}[F:information-flow(T;S)].  \mforall{}[es:EO+(Info)].  \mforall{}[In,X:EClass(T)].
\mforall{}[f:sys-antecedent(es;X)].
    (fifo-information-flow(es;T;S;F;In;X;f)  \mmember{}  \mBbbP{})
Date html generated:
2015_07_20-PM-03_54_56
Last ObjectModification:
2015_01_27-PM-09_58_54
Home
Index