### Nuprl Lemma : corec-ext

[F:Type ⟶ Type]. corec(T.F[T]) ≡ F[corec(T.F[T])] supposing ContinuousMonotone(T.F[T])

Proof

Definitions occuring in Statement :  corec: corec(T.F[T]) continuous-monotone: ContinuousMonotone(T.F[T]) ext-eq: A ≡ B uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] nat: implies:  Q false: False ge: i ≥  guard: {T} prop: subtype_rel: A ⊆B top: Top so_apply: x[s] decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q and: P ∧ Q not: ¬A rev_implies:  Q uiff: uiff(P;Q) subtract: m le: A ≤ B less_than': less_than'(a;b) true: True bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] sq_type: SQType(T) bnot: ¬bb assert: b continuous-monotone: ContinuousMonotone(T.F[T]) type-monotone: Monotone(T.F[T]) nequal: a ≠ b ∈  squash: T ext-eq: A ≡ B so_lambda: λ2x.t[x] corec: corec(T.F[T]) type-continuous: Continuous(T.F[T]) sq_stable: SqStable(P)
Lemmas referenced :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf primrec0_lemma primrec1_lemma top_wf decidable__le subtract_wf false_wf not-ge-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-one-mul-top minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel primrec-unroll eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int le_antisymmetry_iff eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int add-subtract-cancel primrec_wf le_weakening2 le_wf int_seg_wf not-le-2 not-equal-2 subtract-add-cancel subtype_rel_self subtype_rel_transitivity subtype_rel_wf squash_wf true_wf le_weakening nat_wf continuous-monotone_wf sq_stable__le subtype_rel-equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination natural_numberEquality independent_isectElimination independent_functionElimination voidElimination sqequalRule lambdaEquality dependent_functionElimination axiomEquality isect_memberEquality voidEquality applyEquality functionExtensionality universeEquality unionElimination independent_pairFormation productElimination addEquality intEquality minusEquality because_Cache equalityElimination equalityTransitivity equalitySymmetry dependent_pairFormation promote_hyp instantiate cumulativity dependent_set_memberEquality hyp_replacement imageElimination imageMemberEquality baseClosed independent_pairEquality functionEquality isectEquality

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type].  corec(T.F[T])  \mequiv{}  F[corec(T.F[T])]  supposing  ContinuousMonotone(T.F[T])

Date html generated: 2017_04_14-AM-07_41_52
Last ObjectModification: 2017_02_27-PM-03_14_15

Theory : co-recursion

Home Index