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]))))


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: 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:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T all: x:A. B[x] implies:  Q not: ¬A false: False so_apply: x[s1;s2] subtype_rel: A ⊆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: m ifthenelse: if then else fi  btrue: tt so_lambda: λ2y.t[x; y] AFbar: AFbar() or: P ∨ Q iff: ⇐⇒ Q rev_implies:  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 ≥  nequal: a ≠ b ∈  int_upper: {i...} sq_stable: SqStable(P) AF-spread-law: AF-spread-law(x,y.R[x; y]) cand: 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

\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