### Nuprl Lemma : compact-type-corec-lemma0

`∀[F:Type ⟶ Type]`
`  (Monotone(T.F T)`
`  `` (((⋂n:ℕ. (F^n Top)) ⟶ 𝔹) ⊆r ⋃n:ℕ.((F^n Top) ⟶ 𝔹))`
`  `` ((⋂n:ℕ. compact-type2(F^n Top)) ⊆r compact-type2(corec(T.F T))))`

Proof

Definitions occuring in Statement :  compact-type2: `compact-type2(T)` corec: `corec(T.F[T])` type-monotone: `Monotone(T.F[T])` fun_exp: `f^n` nat: `ℕ` bool: `𝔹` subtype_rel: `A ⊆r B` tunion: `⋃x:A.B[x]` uall: `∀[x:A]. B[x]` top: `Top` implies: `P `` Q` apply: `f a` isect: `⋂x:A. B[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  so_apply: `x[s]` so_lambda: `λ2x.t[x]` corec: `corec(T.F[T])` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` subtype_rel: `A ⊆r B` true: `True` squash: `↓T` compose: `f o g` assert: `↑b` bnot: `¬bb` guard: `{T}` sq_type: `SQType(T)` bfalse: `ff` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` or: `P ∨ Q` decidable: `Dec(P)` prop: `ℙ` and: `P ∧ Q` top: `Top` not: `¬A` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` uimplies: `b supposing a` ge: `i ≥ j ` false: `False` nat: `ℕ` member: `t ∈ T` all: `∀x:A. B[x]` implies: `P `` Q` uall: `∀[x:A]. B[x]` compact-type2: `compact-type2(T)` sq_exists: `∃x:A [B[x]]` tunion: `⋃x:A.B[x]` pi2: `snd(t)` p-selector: `p-selector(T;x;p)`
Lemmas referenced :  type-monotone_wf subtype_rel_self ext-eq_weakening subtype_rel_weakening subtype_rel_dep_function tunion_wf corec_wf subtype_rel_transitivity type-monotone_fun_exp_top subtype_rel_wf subtype_rel-equal int_seg_wf primrec_wf fun_exp_wf isect_subtype_rel_trivial nat_wf iff_weakening_equal true_wf squash_wf neg_assert_of_eq_int assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal equal_wf eqff_to_assert assert_of_eq_int eqtt_to_assert bool_wf eq_int_wf le_wf fun_exp_unroll primrec-unroll int_term_value_subtract_lemma int_formula_prop_not_lemma itermSubtract_wf intformnot_wf subtract_wf decidable__le top_wf fun_exp0_lemma primrec0_lemma less_than_wf ge_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_and_lemma intformless_wf itermVar_wf itermConstant_wf intformle_wf intformand_wf satisfiable-full-omega-tt nat_properties void_wf compact-type2_wf sq_exists_wf p-selector_wf full-omega-unsat exists_wf equal-wf-T-base pi2_wf pi1_wf
Rules used in proof :  functionEquality isectEquality baseClosed imageMemberEquality universeEquality functionExtensionality imageElimination applyEquality cumulativity instantiate promote_hyp productElimination equalitySymmetry equalityTransitivity equalityElimination because_Cache dependent_set_memberEquality unionElimination axiomEquality independent_functionElimination computeAll independent_pairFormation sqequalRule voidEquality voidElimination isect_memberEquality dependent_functionElimination intEquality int_eqEquality lambdaEquality dependent_pairFormation independent_isectElimination natural_numberEquality intWeakElimination rename setElimination hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution approximateComputation hyp_replacement applyLambdaEquality

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type]
(Monotone(T.F  T)
{}\mRightarrow{}  (((\mcap{}n:\mBbbN{}.  (F\^{}n  Top))  {}\mrightarrow{}  \mBbbB{})  \msubseteq{}r  \mcup{}n:\mBbbN{}.((F\^{}n  Top)  {}\mrightarrow{}  \mBbbB{}))
{}\mRightarrow{}  ((\mcap{}n:\mBbbN{}.  compact-type2(F\^{}n  Top))  \msubseteq{}r  compact-type2(corec(T.F  T))))

Date html generated: 2018_05_21-PM-06_18_40
Last ObjectModification: 2018_05_16-PM-01_57_03

Theory : basic

Home Index