### Nuprl Lemma : es-fix-test

`∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[f:E(X) ─→ E(X)].`
`  ∀[e:E(X)]`
`    (((f f**(e)) = f**(e) ∈ E(X))`
`    ∧ (f**(f e) = f**(e) ∈ E(X))`
`    ∧ (∀[a:E(X)]. f**(a) = f**(e) ∈ E(X) supposing a is f*(e))) `
`  supposing ∀x:E(X). f x c≤ x`

Proof

Definitions occuring in Statement :  es-E-interface: `E(X)` eclass: `EClass(A[eo; e])` event-ordering+: `EO+(Info)` es-fix: `f**(e)` es-causle: `e c≤ e'` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` top: `Top` all: `∀x:A. B[x]` and: `P ∧ Q` apply: `f a` function: `x:A ─→ B[x]` universe: `Type` equal: `s = t ∈ T` fun-connected: `y is f*(x)`
Lemmas :  es-fix_property es-E-interface-property es-fix_wf2 es-E_wf event-ordering+_subtype es-fix-step iff_weakening_equal assert_wf in-eclass_wf es-fix-connected fun-connected_wf all_wf es-causle_wf
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[f:E(X)  {}\mrightarrow{}  E(X)].
\mforall{}[e:E(X)]
(((f  f**(e))  =  f**(e))
\mwedge{}  (f**(f  e)  =  f**(e))
\mwedge{}  (\mforall{}[a:E(X)].  f**(a)  =  f**(e)  supposing  a  is  f*(e)))
supposing  \mforall{}x:E(X).  f  x  c\mleq{}  x

Date html generated: 2015_07_17-PM-01_01_05
Last ObjectModification: 2015_02_04-PM-05_29_44

Home Index