Nuprl Lemma : fix_wf_corec-partial1

  (∀[F:Type ⟶ Type]
     ∀[f:⋂T:Type. ((T ⟶ partial(A)) ⟶ F[T] ⟶ partial(A))]. (fix(f) ∈ corec(T.F[T]) ⟶ partial(A)) 
     supposing ContinuousMonotone(T.F[T])) supposing 
     (mono(A) and 


Definitions occuring in Statement :  corec: corec(T.F[T]) partial: partial(T) mono: mono(T) continuous-monotone: ContinuousMonotone(T.F[T]) value-type: value-type(T) uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] member: t ∈ T fix: fix(F) isect: x:A. B[x] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B all: x:A. B[x] implies:  Q continuous-monotone: ContinuousMonotone(T.F[T]) and: P ∧ Q prop:
Lemmas referenced :  fix-corec-partial1 corec_wf partial_wf subtype_rel_dep_function corec_subtype subtype_rel_self equal_wf continuous-monotone_wf mono_wf value-type_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination hypothesis sqequalRule lambdaEquality applyEquality functionExtensionality universeEquality cumulativity equalityTransitivity equalitySymmetry functionEquality lambdaFormation productElimination because_Cache dependent_functionElimination independent_functionElimination isectEquality axiomEquality isect_memberEquality

    (\mforall{}[F:Type  {}\mrightarrow{}  Type]
          \mforall{}[f:\mcap{}T:Type.  ((T  {}\mrightarrow{}  partial(A))  {}\mrightarrow{}  F[T]  {}\mrightarrow{}  partial(A))]
              (fix(f)  \mmember{}  corec(T.F[T])  {}\mrightarrow{}  partial(A)) 
          supposing  ContinuousMonotone(T.F[T]))  supposing 
          (mono(A)  and 

Date html generated: 2017_04_14-AM-07_48_35
Last ObjectModification: 2017_02_27-PM-03_18_06

Theory : co-recursion

Home Index