### Nuprl Lemma : fix_wf_corec_parameter2

`∀[F,A:Type ⟶ Type].`
`  ∀[G:Top ⟶ Top ⟶ Top ⋂ ⋂T:Type. ((A[T] ⟶ T) ⟶ A[F[T]] ⟶ F[T])]. ∀[a:A[corec(T.F[T])]].`
`    (fix(G) a ∈ corec(T.F[T])) `
`  supposing Continuous+(T.A[T])`

Proof

Definitions occuring in Statement :  corec: `corec(T.F[T])` strong-type-continuous: `Continuous+(T.F[T])` isect2: `T1 ⋂ T2` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s]` member: `t ∈ T` apply: `f a` 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: `b supposing a` corec: `corec(T.F[T])` so_lambda: `λ2x.t[x]` so_apply: `x[s]` strong-type-continuous: `Continuous+(T.F[T])` type-continuous: `Continuous(T.F[T])` isect2: `T1 ⋂ T2` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` subtype_rel: `A ⊆r B` guard: `{T}` or: `P ∨ Q` bfalse: `ff` top: `Top` nat: `ℕ` prop: `ℙ`
Lemmas referenced :  fix_wf_corec2 continuous-function continuous-id subtype_rel_self nat_wf isect2_subtype_rel3 top_wf subtype_rel_wf bool_wf primrec_wf int_seg_wf corec_wf isect2_wf strong-type-continuous_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule isect_memberEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality functionEquality applyEquality universeEquality independent_isectElimination hypothesis isectEquality cumulativity unionElimination equalityElimination instantiate inrFormation equalityTransitivity equalitySymmetry functionExtensionality voidElimination voidEquality natural_numberEquality setElimination rename axiomEquality because_Cache

Latex:
\mforall{}[F,A:Type  {}\mrightarrow{}  Type].
\mforall{}[G:Top  {}\mrightarrow{}  Top  {}\mrightarrow{}  Top  \mcap{}  \mcap{}T:Type.  ((A[T]  {}\mrightarrow{}  T)  {}\mrightarrow{}  A[F[T]]  {}\mrightarrow{}  F[T])].  \mforall{}[a:A[corec(T.F[T])]].
(fix(G)  a  \mmember{}  corec(T.F[T]))
supposing  Continuous+(T.A[T])

Date html generated: 2016_05_14-AM-06_19_21
Last ObjectModification: 2015_12_26-PM-00_02_34

Theory : co-recursion

Home Index