Nuprl Lemma : squash-causal-invariant_wf

[Info:Type]. ∀[R:Id ─→ Id ─→ Info List+ ─→ Info List+ ─→ ℙ]. ∀[P:Id ─→ Info List+ ─→ ℙ].
  (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) ∈ EO+(Info) ─→ ℙ)


Proof




Definitions occuring in Statement :  squash-causal-invariant: squash-causal-invariant(i,L.P[i; L];a,b,L1,L2.R[a; b; L1; L2]) event-ordering+: EO+(Info) Id: Id listp: List+ uall: [x:A]. B[x] prop: so_apply: x[s1;s2;s3;s4] so_apply: x[s1;s2] member: t ∈ T function: x:A ─→ B[x] universe: Type
Lemmas :  all_wf es-E_wf event-ordering+_subtype es-local-property_wf listp_wf Id_wf squash_wf exists_wf es-causl_wf es-local-relation_wf event-ordering+_wf
\mforall{}[Info:Type].  \mforall{}[R:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P:Id  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}].
    (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2])  \mmember{}  EO+(Info)  {}\mrightarrow{}  \mBbbP{})



Date html generated: 2015_07_17-PM-00_13_04
Last ObjectModification: 2015_01_28-AM-00_05_41

Home Index