Nuprl Lemma : mutual-corec-ext2

[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type].
  (mutual-corec(T.F[T]) ≡ F[mutual-corec(T.F[T])]) supposing 
     ((∀i,j:ℕk. ∀Z:ℕk ⟶ Type.  Continuous(X.F[λi.if (i =z j) then else fi i)) and 


Definitions occuring in Statement :  mutual-corec: mutual-corec(T.F[T]) k-monotone: k-Monotone(T.F[T]) k-ext: A ≡ B type-continuous: Continuous(T.F[T]) int_seg: {i..j-} nat: ifthenelse: if then else fi  eq_int: (i =z j) uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] apply: a lambda: λx.A[x] function: x:A ⟶ B[x] natural_number: $n 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] implies:  Q k-ext: A ≡ B and: P ∧ Q k-subtype: A ⊆ B all: x:A. B[x] subtype_rel: A ⊆B nat: prop: int_seg: {i..j-} bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff uiff: uiff(P;Q) exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False
Lemmas referenced :  mutual-corec-ext implies-k-continuous int_seg_wf all_wf type-continuous_wf eq_int_wf bool_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int k-monotone_wf nat_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination because_Cache sqequalRule independent_functionElimination productElimination independent_pairEquality lambdaEquality dependent_functionElimination axiomEquality natural_numberEquality setElimination rename instantiate applyEquality cumulativity universeEquality functionEquality functionExtensionality lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry dependent_pairFormation promote_hyp voidElimination isect_memberEquality

\mforall{}[k:\mBbbN{}].  \mforall{}[F:(\mBbbN{}k  {}\mrightarrow{}  Type)  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type].
    (mutual-corec(T.F[T])  \mequiv{}  F[mutual-corec(T.F[T])])  supposing 
          ((\mforall{}i,j:\mBbbN{}k.  \mforall{}Z:\mBbbN{}k  {}\mrightarrow{}  Type.    Continuous(X.F[\mlambda{}i.if  (i  =\msubz{}  j)  then  X  else  Z  i  fi  ]  i))  and 

Date html generated: 2018_05_21-PM-00_10_50
Last ObjectModification: 2017_10_18-PM-02_45_04

Theory : co-recursion

Home Index