Nuprl Lemma : urec_induction

∀[F:Type ⟶ Type]
  (destructor{i:l}(T.F[T])
     ⇒ (∀[P:urec(F) ⟶ ℙ]
           ((∀[T:Type]. ((∀x:T ⋂ urec(F). P[x]) ⇒ (∀x:F T ⋂ urec(F). P[x]))) ⇒ (∀x:urec(F). P[x])))) supposing 
     ((∀T:Type. ((T ⊆r Base) ⇒ ((F T) ⊆r Base))) and 
     Monotone(T.F[T]))


Proof



Definitions occuring in Statement :  destructor: destructor{i:l}(T.F[T]),  urec: urec(F),  type-monotone: Monotone(T.F[T]),  isect2: T1 ⋂ T2,  uimplies: b supposing a,  subtype_rel: A ⊆r B,  uall: ∀[x:A]. B[x],  prop: ℙ,  so_apply: x[s],  all: ∀x:A. B[x],  implies: P ⇒ Q,  apply: f a,  function: x:A ⟶ B[x],  base: Base,  universe: Type
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  uimplies: b supposing a,  member: t ∈ T,  type-monotone: Monotone(T.F[T]),  subtype_rel: A ⊆r B,  all: ∀x:A. B[x],  implies: P ⇒ Q,  so_apply: x[s],  prop: ℙ,  so_lambda: λ2x.t[x],  le: A ≤ B,  and: P ∧ Q,  less_than': less_than'(a;b),  false: False,  not: ¬A,  nat: ℕ,  top: Top,  exists: ∃x:A. B[x],  satisfiable_int_formula: satisfiable_int_formula(fmla),  lelt: i ≤ j < k,  int_seg: {i..j-},  guard: {T},  tunion: ⋃x:A.B[x],  isect2: T1 ⋂ T2,  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  ifthenelse: if b then t else f fi ,  bfalse: ff,  union-continuous: union-continuous{i:l}(T.F[T]),  ext-eq: A ≡ B,  pi2: snd(t),  decidable: Dec(P),  or: P ∨ Q,  sq_type: SQType(T),  nat_plus: ℕ+,  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  uiff: uiff(P;Q),  true: True,  subtract: n - m,  rev_uimplies: rev_uimplies(P;Q),  ge: i ≥ j 
Lemmas referenced :  urec_wf,  istype-universe,  isect2_wf,  isect2_subtype_rel2,  subtype_rel_self,  destructor_wf,  subtype_rel_wf,  base_wf,  type-monotone_wf,  tunion_wf,  int_seg_wf,  subtract_wf,  fun_exp_wf,  int_seg_subtype_nat,  istype-false,  istype-int,  istype-less_than,  primrec-wf2,  all_wf,  istype-nat,  isect2_subtype_rel,  int_formula_prop_wf,  int_formula_prop_le_lemma,  int_term_value_constant_lemma,  int_term_value_var_lemma,  int_formula_prop_less_lemma,  istype-void,  int_formula_prop_and_lemma,  intformle_wf,  itermConstant_wf,  itermVar_wf,  intformless_wf,  intformand_wf,  full-omega-unsat,  int_seg_properties,  bool_wf,  subtype_rel_transitivity,  type-monotone-union-continuous,  decidable__equal_int,  subtype_base_sq,  int_subtype_base,  fun_exp0_lemma,  decidable__le,  intformnot_wf,  itermSubtract_wf,  intformeq_wf,  int_formula_prop_not_lemma,  int_term_value_subtract_lemma,  int_formula_prop_eq_lemma,  decidable__lt,  istype-le,  subtype_rel-equal,  fun_exp_add1_sub,  not-lt-2,  not-equal-2,  add_functionality_wrt_le,  add-associates,  add-zero,  zero-add,  le-add-cancel,  condition-implies-le,  add-commutes,  minus-add,  minus-zero,  add-member-int_seg2,  itermAdd_wf,  int_term_value_add_lemma,  fun_exp_apply_add1,  subtype_rel_functionality_wrt_iff,  ext-eq_weakening,  urec-level-property,  le_wf,  nat_properties,  urec-level_wf,  void_wf,  less_than_wf,  urec_subtype_base,  base-member-prop
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation_alt,  cut,  introduction,  sqequalRule,  sqequalHypSubstitution,  isect_memberEquality_alt,  isectElimination,  thin,  hypothesisEquality,  axiomEquality,  hypothesis,  isectIsTypeImplies,  inhabitedIsType,  rename,  lambdaEquality_alt,  dependent_functionElimination,  functionIsTypeImplies,  lambdaFormation_alt,  universeIsType,  extract_by_obid,  isectIsType,  instantiate,  universeEquality,  functionIsType,  applyEquality,  because_Cache,  setElimination,  closedConclusion,  natural_numberEquality,  independent_isectElimination,  independent_pairFormation,  voidEquality,  setIsType,  independent_functionElimination,  equalitySymmetry,  equalityTransitivity,  equalityIsType1,  voidElimination,  int_eqEquality,  dependent_pairFormation_alt,  approximateComputation,  productElimination,  imageElimination,  isect_memberEquality,  unionElimination,  equalityElimination,  cumulativity,  intEquality,  imageMemberEquality,  dependent_pairEquality_alt,  dependent_set_memberEquality_alt,  productIsType,  addEquality,  minusEquality,  baseClosed,  applyLambdaEquality
Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type]
    (destructor\{i:l\}(T.F[T])
          {}\mRightarrow{}  (\mforall{}[P:urec(F)  {}\mrightarrow{}  \mBbbP{}]
                      ((\mforall{}[T:Type].  ((\mforall{}x:T  \mcap{}  urec(F).  P[x])  {}\mRightarrow{}  (\mforall{}x:F  T  \mcap{}  urec(F).  P[x])))
                      {}\mRightarrow{}  (\mforall{}x:urec(F).  P[x]))))  supposing 
          ((\mforall{}T:Type.  ((T  \msubseteq{}r  Base)  {}\mRightarrow{}  ((F  T)  \msubseteq{}r  Base)))  and 
          Monotone(T.F[T]))


Date html generated: 2019_10_15-AM-11_31_53
Last ObjectModification: 2018_10_31-PM-02_25_57

Theory : general


Home Index