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

`∀[F:Type ⟶ Type]`
`  (Monotone(T.F T)`
`  `` (((⋂n:ℕ. (F^n Top)) ⟶ 𝔹) ⊆r ⋃n:ℕ.((F^n Top) ⟶ 𝔹))`
`  `` (∀[T:Type]. (compact-type2(T) `` compact-type2(F T)))`
`  `` 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 :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` nat: `ℕ` false: `False` ge: `i ≥ j ` uimplies: `b supposing a` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` not: `¬A` all: `∀x:A. B[x]` top: `Top` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` compact-type2: `compact-type2(T)` sq_exists: `∃x:{A| B[x]}` p-selector: `p-selector(T;x;p)` squash: `↓T` true: `True` nat_plus: `ℕ+`
Lemmas referenced :  compact-type-corec-lemma0 uall_wf compact-type2_wf subtype_rel_wf nat_wf fun_exp_wf top_wf bool_wf tunion_wf type-monotone_wf nat_properties satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf less_than_wf fun_exp0_lemma decidable__le subtract_wf intformnot_wf itermSubtract_wf int_formula_prop_not_lemma int_term_value_subtract_lemma void_wf exists_wf equal-wf-T-base p-selector_wf equal_wf squash_wf true_wf fun_exp_unroll_1 le_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaFormation independent_functionElimination rename instantiate universeEquality sqequalRule lambdaEquality cumulativity functionEquality applyEquality functionExtensionality isectEquality because_Cache isect_memberEquality setElimination intWeakElimination natural_numberEquality independent_isectElimination dependent_pairFormation int_eqEquality intEquality dependent_functionElimination voidElimination voidEquality independent_pairFormation computeAll axiomEquality equalityTransitivity equalitySymmetry unionElimination dependent_set_memberEquality productElimination baseClosed addLevel hyp_replacement imageElimination equalityUniverse levelHypothesis imageMemberEquality

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{}  (\mforall{}[T:Type].  (compact-type2(T)  {}\mRightarrow{}  compact-type2(F  T)))
{}\mRightarrow{}  compact-type2(corec(T.F  T)))

Date html generated: 2016_10_25-AM-10_14_00
Last ObjectModification: 2016_07_12-AM-06_24_28

Theory : basic

Home Index