Nuprl Lemma : embedding-preserves-local-relation

`∀[Info:Type]. ∀[R:Id ─→ Id ─→ Info List+ ─→ Info List+ ─→ ℙ]. ∀[eo1:EO+(Info)].`
`  ∀eo2:EO+(Info). ∀f:E ─→ E.`
`    (es-local-embedding(Info;eo1;eo2;f)`
`    `` (∀[e1,e2:E].`
`          (es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo1;e1;e2)`
`          `⇐⇒` es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo2;f e1;f e2))))`

Proof

Definitions occuring in Statement :  es-local-relation: `es-local-relation(i,j,L1,L2.R[i; j; L1; L2];es;e1;e2)` es-local-embedding: `es-local-embedding(Info;eo1;eo2;f)` event-ordering+: `EO+(Info)` es-E: `E` Id: `Id` listp: `A List+` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2;s3;s4]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` apply: `f a` function: `x:A ─→ B[x]` universe: `Type`
Lemmas :  assert_of_lt_int map-length length-append length_wf es-before_wf cons_wf nil_wf length_nil non_neg_length length_wf_nil length_wf_nat length_cons assert_wf lt_int_wf es-local-relation_wf listp_wf Id_wf es-E_wf event-ordering+_subtype es-local-embedding_wf event-ordering+_wf
\mforall{}[Info:Type].  \mforall{}[R:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[eo1:EO+(Info)].
\mforall{}eo2:EO+(Info).  \mforall{}f:E  {}\mrightarrow{}  E.
(es-local-embedding(Info;eo1;eo2;f)
{}\mRightarrow{}  (\mforall{}[e1,e2:E].
(es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo1;e1;e2)
\mLeftarrow{}{}\mRightarrow{}  es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo2;f  e1;f  e2))))

Date html generated: 2015_07_17-PM-00_12_19
Last ObjectModification: 2015_01_28-AM-00_13_05

Home Index