Nuprl Lemma : fun-connected-induction2

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

Proof

Definitions occuring in Statement : 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, member: t ∈ T, prop: ℙ, so_lambda: λ₂x.t[x], uimplies: b supposing a, so_apply: x[s1;s2], subtype_rel: A ⊆r B, so_apply: x[s], nat: ℕ, not: ¬A, ge: i ≥ j , le: A ≤ B, and: P ∧ Q, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], false: False, top: Top, decidable: Dec(P), or: P ∨ Q, less_than: a < b, squash: ↓T, sq_type: SQType(T), guard: {T}, cons: [a / b], fun-path: y=f*(x) via L, subtract: n - m, last: last(L), select: L[n], uiff: uiff(P;Q), int_seg: {i..j^-}, lelt: i ≤ j < k, less_than': less_than'(a;b), true: True, iff: P ⇐⇒ Q, rev_implies: P ⇐ Q, fun-connected: y is f*(x)
Lemmas referenced : all_wf, isect_wf, not_wf, equal_wf, fun-connected_wf, list_wf, less_than_wf, length_wf, subtract_wf, fun-path_wf, set_wf, primrec-wf2, nat_wf, non_neg_length, 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, decidable__lt, decidable__equal_int, intformnot_wf, intformeq_wf, itermSubtract_wf, int_formula_prop_not_lemma, int_formula_prop_eq_lemma, int_term_value_subtract_lemma, subtype_base_sq, int_subtype_base, list-cases, length_of_nil_lemma, product_subtype_list, length_of_cons_lemma, itermAdd_wf, int_term_value_add_lemma, nil_wf, and_wf, reduce_hd_cons_lemma, decidable__le, length2-decomp, fun-path-append, cons_wf, false_wf, lelt_wf, squash_wf, true_wf, iff_weakening_equal, append_wf, length-append, equal-wf-T-base, length_append, subtype_rel_list, top_wf, add-is-int-iff, add_nat_wf, length_wf_nat, le_wf, nat_properties
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, isect_memberFormation, lambdaFormation, cut, introduction, extract_by_obid, sqequalHypSubstitution, isectElimination, thin, cumulativity, hypothesisEquality, sqequalRule, lambdaEquality, because_Cache, applyEquality, functionExtensionality, hypothesis, functionEquality, universeEquality, rename, setElimination, natural_numberEquality, intEquality, dependent_functionElimination, independent_isectElimination, productElimination, dependent_pairFormation, int_eqEquality, isect_memberEquality, voidElimination, voidEquality, independent_pairFormation, computeAll, independent_functionElimination, unionElimination, imageElimination, instantiate, promote_hyp, hypothesis_subsumption, equalityTransitivity, equalitySymmetry, hyp_replacement, dependent_set_memberEquality, applyLambdaEquality, imageMemberEquality, baseClosed, baseApply, closedConclusion, addEquality, pointwiseFunctionality

Latex:
\mforall{}[T:Type] \mforall{}f:T {}\mrightarrow{} T \mforall{}[R:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}] ((\mforall{}x:T. R[x;x]) {}\mRightarrow{} (\mforall{}x,y:T. x is f*(f y) {}\mRightarrow{} R[x;f y] {}\mRightarrow{} R[x;y] supposing \mneg{}((f y) = y)) {}\mRightarrow{} \{\mforall{}x,y:T. (x is f*(y) {}\mRightarrow{} R[x;y])\}) Date html generated: 2018_05_21-PM-07_44_24 Last ObjectModification: 2017_07_26-PM-05_21_59 Theory : general Home Index