Nuprl Lemma : strong-fun-connected-induction

∀[T:Type]
  ∀f:T ⟶ T
    ∀[R:T ⟶ T ⟶ ℙ]
      (retraction(T;f)
      ⇒ (∀x:T. R[x;x])
      ⇒ (∀x,y,z:T.
            (y is f*(z) ⇒ (∀u:T. (y is f*(u) ⇒ u is f*(z) ⇒ R[u;z])) ⇒ R[x;z]) supposing 
               ((¬(x = y ∈ T)) and 
               (x = (f y) ∈ T)))
      ⇒ {∀x,y:T.  (x is f*(y) ⇒ R[x;y])})


Proof



Definitions occuring in Statement :  retraction: retraction(T;f),  fun-connected: y is f*(x),  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  prop: ℙ,  guard: {T},  so_apply: x[s1;s2],  all: ∀x:A. B[x],  not: ¬A,  implies: P ⇒ Q,  apply: f a,  function: x:A ⟶ B[x],  universe: Type,  equal: s = t ∈ T
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  implies: P ⇒ Q,  guard: {T},  retraction: retraction(T;f),  exists: ∃x:A. B[x],  member: t ∈ T,  uimplies: b supposing a,  not: ¬A,  false: False,  prop: ℙ,  so_apply: x[s1;s2],  subtype_rel: A ⊆r B,  nat: ℕ,  so_lambda: λ2x.t[x],  so_apply: x[s],  fun-connected: y is f*(x),  or: P ∨ Q,  less_than: a < b,  squash: ↓T,  and: P ∧ Q,  satisfiable_int_formula: satisfiable_int_formula(fmla),  top: Top,  so_lambda: λ2x y.t[x; y],  decidable: Dec(P),  le: A ≤ B,  uiff: uiff(P;Q),  true: True,  less_than': less_than'(a;b)
Lemmas referenced :  istype-universe,  istype-void,  fun-connected_wf,  subtype_rel_self,  retraction_wf,  less_than_wf,  subtract_wf,  nat_wf,  istype-int,  primrec-wf2,  all_wf,  retraction-fun-path,  full-omega-unsat,  intformand_wf,  intformless_wf,  itermVar_wf,  itermSubtract_wf,  itermConstant_wf,  int_formula_prop_and_lemma,  int_formula_prop_less_lemma,  int_term_value_var_lemma,  int_term_value_subtract_lemma,  int_term_value_constant_lemma,  int_formula_prop_wf,  fun-connected-induction,  decidable__lt,  subtract-is-int-iff,  intformnot_wf,  intformle_wf,  int_formula_prop_not_lemma,  int_formula_prop_le_lemma,  false_wf,  decidable__le,  le_wf,  squash_wf,  true_wf,  itermAdd_wf,  int_term_value_add_lemma,  add_nat_wf,  subtract_nat_wf,  istype-false
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation_alt,  lambdaFormation_alt,  sqequalHypSubstitution,  productElimination,  thin,  sqequalRule,  functionIsType,  cut,  introduction,  extract_by_obid,  isectElimination,  hypothesisEquality,  hypothesis,  inhabitedIsType,  isectIsType,  equalityIsType1,  applyEquality,  because_Cache,  universeIsType,  instantiate,  universeEquality,  rename,  setElimination,  lambdaEquality_alt,  natural_numberEquality,  setIsType,  functionEquality,  dependent_functionElimination,  independent_functionElimination,  independent_isectElimination,  unionElimination,  imageElimination,  approximateComputation,  dependent_pairFormation_alt,  int_eqEquality,  isect_memberEquality_alt,  voidElimination,  independent_pairFormation,  hyp_replacement,  equalitySymmetry,  dependent_set_memberEquality_alt,  productIsType,  applyLambdaEquality,  axiomEquality,  functionIsTypeImplies,  equalityTransitivity,  pointwiseFunctionality,  promote_hyp,  baseApply,  closedConclusion,  baseClosed,  imageMemberEquality,  addEquality
Latex:
\mforall{}[T:Type]
    \mforall{}f:T  {}\mrightarrow{}  T
        \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}]
            (retraction(T;f)
            {}\mRightarrow{}  (\mforall{}x:T.  R[x;x])
            {}\mRightarrow{}  (\mforall{}x,y,z:T.
                        (y  is  f*(z)  {}\mRightarrow{}  (\mforall{}u:T.  (y  is  f*(u)  {}\mRightarrow{}  u  is  f*(z)  {}\mRightarrow{}  R[u;z]))  {}\mRightarrow{}  R[x;z])  supposing 
                              ((\mneg{}(x  =  y))  and 
                              (x  =  (f  y))))
            {}\mRightarrow{}  \{\mforall{}x,y:T.    (x  is  f*(y)  {}\mRightarrow{}  R[x;y])\})


Date html generated: 2019_10_15-AM-11_14_23
Last ObjectModification: 2018_10_09-PM-02_14_14

Theory : general


Home Index