Nuprl Lemma : corec-value-type

[F:Type ⟶ Type]
  (value-type(corec(T.F[T]))) supposing ((∃n:ℕvalue-type(F^n Top)) and (∀A,B:Type.  (A ≡  F[A] ≡ F[B])))


Proof




Definitions occuring in Statement :  corec: corec(T.F[T]) fun_exp: f^n nat: value-type: value-type(T) ext-eq: A ≡ B uimplies: supposing a uall: [x:A]. B[x] top: Top so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] implies:  Q apply: a function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a value-type: value-type(T) sq_stable: SqStable(P) implies:  Q so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] has-value: (a)↓ exists: x:A. B[x] corec: corec(T.F[T]) subtype_rel: A ⊆B nat: prop: squash: T fun_exp: f^n false: False ge: i ≥  guard: {T} ext-eq: A ≡ B and: P ∧ Q top: Top decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ 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 sq_type: SQType(T) bnot: ¬bb assert: b compose: g nequal: a ≠ b ∈ 
Lemmas referenced :  sq_stable__has-value corec_wf subtype_rel_weakening primrec_wf top_wf int_seg_wf fun_exp_wf value-type-has-value equal_wf equal-wf-base base_wf exists_wf nat_wf value-type_wf all_wf ext-eq_wf nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf primrec0_lemma 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 eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int le_weakening eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int not-le-2 not-equal-2 le_wf compose_wf ext-eq_weakening primrec-unroll
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_functionElimination equalityTransitivity equalitySymmetry sqequalRule lambdaEquality applyEquality functionExtensionality universeEquality cumulativity lambdaFormation productElimination instantiate natural_numberEquality setElimination rename independent_isectElimination dependent_functionElimination imageMemberEquality baseClosed imageElimination because_Cache isect_memberEquality axiomSqleEquality functionEquality intWeakElimination voidElimination independent_pairEquality axiomEquality voidEquality unionElimination independent_pairFormation addEquality intEquality minusEquality equalityElimination dependent_pairFormation promote_hyp dependent_set_memberEquality

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type]
    (value-type(corec(T.F[T])))  supposing 
          ((\mexists{}n:\mBbbN{}.  value-type(F\^{}n  Top))  and 
          (\mforall{}A,B:Type.    (A  \mequiv{}  B  {}\mRightarrow{}  F[A]  \mequiv{}  F[B])))



Date html generated: 2017_04_14-AM-07_41_47
Last ObjectModification: 2017_02_27-PM-03_13_26

Theory : co-recursion


Home Index