Nuprl Lemma : Q-R-glues-trivial-restrict

`∀[Info:Type]. ∀[P:es:EO+(Info) ─→ E ─→ ℙ].`
`  ∀p:∀es:EO+(Info). ∀e:E.  Dec(P[es;e])`
`    ∀[A,B:Type].`
`      ∀Ia:EClass(A). ∀Ib:EClass(B).`
`        ((∀es:EO+(Info). ∀e:E.  (Ib es e) = {} ∈ bag(B) supposing ¬P[es;e])`
`        `` (∀es:EO+(Info)`
`              ∀[Q,R:E ─→ E ─→ ℙ].`
`                ∀f:E(Ia) ─→ B. ∀g:E(Ib) ─→ E.  (g glues Ia:Q ──f─→ (Ib|p):R `` g glues Ia:Q ──f─→ Ib:R)))`

Proof

Definitions occuring in Statement :  Q-R-glues: `g glues Ia:Qa ──f─→ Ib:Rb` es-interface-restrict: `(I|p)` es-E-interface: `E(X)` eclass: `EClass(A[eo; e])` event-ordering+: `EO+(Info)` es-E: `E` decidable: `Dec(P)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` apply: `f a` function: `x:A ─→ B[x]` universe: `Type` equal: `s = t ∈ T` empty-bag: `{}` bag: `bag(T)`
Lemmas :  Q-R-glues_wf squash_wf true_wf es-E-interface_wf es-interface-subtype_rel2 es-E_wf event-ordering+_subtype event-ordering+_wf top_wf eclass_wf event-ordering+_cumulative2 es-interface-restrict-trivial bag_wf empty-bag_wf iff_weakening_equal not_wf subtype_rel_dep_function es-interface-restrict_wf es-E-interface-restrict subtype_rel_self all_wf isect_wf equal-wf-T-base decidable_wf

Latex:
\mforall{}[Info:Type].  \mforall{}[P:es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].
\mforall{}p:\mforall{}es:EO+(Info).  \mforall{}e:E.    Dec(P[es;e])
\mforall{}[A,B:Type].
\mforall{}Ia:EClass(A).  \mforall{}Ib:EClass(B).
((\mforall{}es:EO+(Info).  \mforall{}e:E.    (Ib  es  e)  =  \{\}  supposing  \mneg{}P[es;e])
{}\mRightarrow{}  (\mforall{}es:EO+(Info)
\mforall{}[Q,R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].
\mforall{}f:E(Ia)  {}\mrightarrow{}  B.  \mforall{}g:E(Ib)  {}\mrightarrow{}  E.
(g  glues  Ia:Q  {}{}f{}\mrightarrow{}  (Ib|p):R  {}\mRightarrow{}  g  glues  Ia:Q  {}{}f{}\mrightarrow{}  Ib:R)))

Date html generated: 2015_07_21-PM-04_11_14
Last ObjectModification: 2015_02_04-PM-06_04_27

Home Index