### Nuprl Lemma : AF-uniform-induction

`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].`
`  (∀[Q:T ⟶ ℙ]. uniform-TI(T;x,y.¬R[x;y];t.Q[t])) supposing `
`     (AFx,y:T.R[x;y] and `
`     (∀x,y,z:T.  ((¬R[x;y]) `` (¬R[y;z]) `` (¬R[x;z]))))`

Proof

Definitions occuring in Statement :  almost-full: `AFx,y:T.R[x; y]` uniform-TI: `uniform-TI(T;x,y.R[x; y];t.Q[t])` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` so_apply: `x[s]` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` all: `∀x:A. B[x]` implies: `P `` Q` not: `¬A` false: `False` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` prop: `ℙ` almost-full: `AFx,y:T.R[x; y]` squash: `↓T` uniform-TI: `uniform-TI(T;x,y.R[x; y];t.Q[t])` nat: `ℕ` decidable: `Dec(P)` consistent-seq: `R-consistent-seq(n)` so_lambda: `λ2x.t[x]` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` so_apply: `x[s]` int_seg: `{i..j-}` lelt: `i ≤ j < k` guard: `{T}` eq_int: `(i =z j)` subtract: `n - m` ifthenelse: `if b then t else f fi ` btrue: `tt` so_lambda: `λ2x y.t[x; y]` AFbar: `AFbar()` or: `P ∨ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uiff: `uiff(P;Q)` top: `Top` true: `True` isr: `isr(x)` assert: `↑b` bfalse: `ff` exposed-it: `exposed-it` bool: `𝔹` unit: `Unit` it: `⋅` exists: `∃x:A. B[x]` sq_type: `SQType(T)` bnot: `¬bb` ge: `i ≥ j ` nequal: `a ≠ b ∈ T ` int_upper: `{i...}` sq_stable: `SqStable(P)` AF-spread-law: `AF-spread-law(x,y.R[x; y])` cand: `A c∧ B` outl: `outl(x)` isl: `isl(x)` less_than: `a < b`
Lemmas referenced :  not_wf nat_wf AF-spread-law_wf AFbar_wf unit_wf2 int_seg_wf decidable__AFbar all_wf int_seg_subtype_nat false_wf subtype_rel_dep_function subtype_rel_sets and_wf le_wf less_than_wf less_than_transitivity2 le_weakening2 subtype_rel_self AF-path-barred uall_wf almost-full_wf subtract_wf decidable__le not-le-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-one-mul-top minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel decidable__lt not-lt-2 add-mul-special zero-mul le-add-cancel-alt eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int less_than_transitivity1 le_weakening less_than_irreflexivity eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base iff_transitivity assert_wf bnot_wf equal-wf-T-base iff_weakening_uiff assert_of_bnot int_upper_subtype_nat nat_properties nequal-le-implies true_wf sq_stable__le le_antisymmetry_iff not-equal-2 set_wf isl_wf int_upper_wf le-add-cancel2 outl_wf int_subtype_base set_subtype_base decidable__int_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality voidElimination applyEquality functionExtensionality cumulativity hypothesis universeEquality extract_by_obid isectElimination rename imageElimination imageMemberEquality baseClosed functionEquality isect_memberEquality because_Cache strong_bar_Induction unionEquality natural_numberEquality setElimination dependent_set_memberEquality equalityTransitivity equalitySymmetry independent_isectElimination independent_pairFormation lambdaFormation intEquality setEquality productElimination independent_functionElimination unionElimination addEquality voidEquality minusEquality equalityElimination dependent_pairFormation promote_hyp instantiate impliesFunctionality hypothesis_subsumption axiomEquality int_eqReduceTrueSq int_eqReduceFalseSq multiplyEquality inlEquality productEquality isectEquality hyp_replacement applyLambdaEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
(\mforall{}[Q:T  {}\mrightarrow{}  \mBbbP{}].  uniform-TI(T;x,y.\mneg{}R[x;y];t.Q[t]))  supposing
(AFx,y:T.R[x;y]  and
(\mforall{}x,y,z:T.    ((\mneg{}R[x;y])  {}\mRightarrow{}  (\mneg{}R[y;z])  {}\mRightarrow{}  (\mneg{}R[x;z]))))

Date html generated: 2017_04_14-AM-07_28_07
Last ObjectModification: 2017_02_27-PM-02_58_25

Theory : bar-induction

Home Index