Nuprl Lemma : es-prior-fixedpoints-unequal

[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[f:E(X) ─→ E(X)].
    (f**(e) ∈ prior-f-fixedpoints(e'))) supposing ((¬(e' f**(e) ∈ E)) and (e' ∈ prior-f-fixedpoints(e))) 
  supposing ∀x:E(X). c≤ x


Definitions occuring in Statement :  es-prior-fixedpoints: prior-f-fixedpoints(e) es-E-interface: E(X) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-fix: f**(e) es-causle: c≤ e' es-E: E l_member: (x ∈ l) uimplies: supposing a uall: [x:A]. B[x] top: Top all: x:A. B[x] not: ¬A apply: a function: x:A ─→ B[x] universe: Type equal: t ∈ T
Lemmas :  l_member_wf es-prior-fixedpoints_wf subtype_rel_list es-E_wf event-ordering+_subtype all_wf es-causle_wf es-E-interface_wf eclass_wf top_wf event-ordering+_wf es-fix-last-prior-fixedpoints property-from-l_member equal_wf sq_stable__equal es-fix-sqequal es-fix-equal-E-interface and_wf in-eclass_wf assert_elim subtype_base_sq bool_wf bool_subtype_base assert_wf equal_functionality_wrt_subtype_rel2 not_wf es-prior-fixedpoints-iseg es-prior-fixedpoints-non-null es-prior-fixedpoints-no_repeats list_wf last_wf iseg_wf null_wf3 no_repeats_wf before_last iseg_is_sublist l_before_sublist last-not-before es-fix_wf2

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[f:E(X)  {}\mrightarrow{}  E(X)].
        (\mneg{}(f**(e)  \mmember{}  prior-f-fixedpoints(e')))  supposing 
              ((\mneg{}(e'  =  f**(e)))  and 
              (e'  \mmember{}  prior-f-fixedpoints(e))) 
    supposing  \mforall{}x:E(X).  f  x  c\mleq{}  x

Date html generated: 2015_07_21-PM-03_54_06
Last ObjectModification: 2015_01_27-PM-06_04_01

Home Index