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: 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