Nuprl Lemma : equiv-on-corec-2

F:𝕌' ⟶ 𝕌'
  (continuous-monotone{i':l}(T.F[T])
   (∀G:⋂T:𝕌'. ((T ⟶ T ⟶ ℙ) ⟶ F[T] ⟶ F[T] ⟶ ℙ)
        ((∀T:𝕌'. ∀E:T ⟶ T ⟶ ℙ.  (EquivRel(T;x,y.E y)  EquivRel(F[T];x,y.G y)))
         EquivRel(corec(T.F[T]);x,y.corec-rel(G) y))))


Proof




Definitions occuring in Statement :  corec-rel: corec-rel(G) corec: corec(T.F[T]) equiv_rel: EquivRel(T;x,y.E[x; y]) continuous-monotone: ContinuousMonotone(T.F[T]) prop: so_apply: x[s] all: x:A. B[x] implies:  Q apply: a isect: x:A. B[x] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q uall: [x:A]. B[x] member: t ∈ T nat: false: False ge: i ≥  guard: {T} uimplies: supposing a prop: le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) not: ¬A top: Top lt_int: i <j subtract: m eq_int: (i =z j) ifthenelse: if then else fi  btrue: tt decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q) subtype_rel: A ⊆B true: True squash: T nequal: a ≠ b ∈  sq_type: SQType(T) assert: b bfalse: ff compose: g so_apply: x[s] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] so_lambda: λ2x.t[x] equiv_rel: EquivRel(T;x,y.E[x; y]) refl: Refl(T;x,y.E[x; y]) corec-rel: corec-rel(G) cand: c∧ B sym: Sym(T;x,y.E[x; y]) trans: Trans(T;x,y.E[x; y]) corec: corec(T.F[T])
Lemmas referenced :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf fun_exp_unroll false_wf le_wf primrec-unroll true_wf top_wf decidable__le subtract_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 le_weakening2 subtype_base_sq bool_subtype_base equal_wf eq_int_eq_false le_weakening subtype_rel_self iff_weakening_equal iff_imp_equal_bool lt_int_wf le-add-cancel2 assert_of_lt_int assert_wf iff_wf primrec_wf not-le-2 int_seg_wf nat_wf equiv_rel_true bool_wf bfalse_wf equiv_rel_wf set_wf primrec-wf2 all_wf continuous-monotone_wf corec-rel-wf2 corec_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination natural_numberEquality independent_isectElimination independent_functionElimination voidElimination sqequalRule lambdaEquality dependent_functionElimination axiomEquality equalityTransitivity equalitySymmetry dependent_set_memberEquality independent_pairFormation isect_memberEquality voidEquality because_Cache unionElimination productElimination addEquality applyEquality intEquality minusEquality instantiate imageElimination imageMemberEquality baseClosed universeEquality addLevel impliesFunctionality cumulativity functionExtensionality isectEquality functionEquality

Latex:
\mforall{}F:\mBbbU{}'  {}\mrightarrow{}  \mBbbU{}'
    (continuous-monotone\{i':l\}(T.F[T])
    {}\mRightarrow{}  (\mforall{}G:\mcap{}T:\mBbbU{}'.  ((T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  F[T]  {}\mrightarrow{}  F[T]  {}\mrightarrow{}  \mBbbP{})
                ((\mforall{}T:\mBbbU{}'.  \mforall{}E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.    (EquivRel(T;x,y.E  x  y)  {}\mRightarrow{}  EquivRel(F[T];x,y.G  E  x  y)))
                {}\mRightarrow{}  EquivRel(corec(T.F[T]);x,y.corec-rel(G)  x  y))))



Date html generated: 2018_07_25-PM-01_30_47
Last ObjectModification: 2018_05_31-AM-11_23_45

Theory : co-recursion


Home Index