Nuprl Lemma : monotone-bar-induction1

[B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ].
  ((∀n:ℕ. ∀s:ℕn ⟶ ℕ.  (B[n;s]  (∀m:ℕB[n 1;s.m@n])))
   (∀n:ℕ. ∀s:ℕn ⟶ ℕ.  (B[n;s]  (↓Q[n;s])))
   (∀n:ℕ. ∀s:ℕn ⟶ ℕ.  ((∀m:ℕ(↓Q[n 1;s.m@n]))  (↓Q[n;s])))
   (∀alpha:ℕ ⟶ ℕ. ∃m:ℕB[m;alpha])
   (↓Q[0;λx.⊥]))


Proof




Definitions occuring in Statement :  seq-add: s.x@n int_seg: {i..j-} nat: bottom: uall: [x:A]. B[x] prop: so_apply: x[s1;s2] all: x:A. B[x] exists: x:A. B[x] squash: T implies:  Q lambda: λx.A[x] function: x:A ⟶ B[x] add: m natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  Q exists: x:A. B[x] squash: T so_lambda: λ2y.t[x; y] nat: so_apply: x[s1;s2] all: x:A. B[x] prop: ge: i ≥  decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) false: False top: Top and: P ∧ Q subtype_rel: A ⊆B le: A ≤ B less_than': less_than'(a;b) guard: {T} pi1: fst(t) bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  int_seg: {i..j-} lelt: i ≤ j < k bfalse: ff sq_type: SQType(T) bnot: ¬bb assert: b rev_implies:  Q iff: ⇐⇒ Q so_lambda: λ2x.t[x] so_apply: x[s] true: True cand: c∧ B outl: outl(x) sq_stable: SqStable(P) less_than: a < b subtract: m seq-add: s.x@n nequal: a ≠ b ∈  seq-adjoin: s++t seq-append: seq-append(n;m;s1;s2) isl: isl(x)
Lemmas referenced :  strong-continuity-implies3 basic_bar_induction assert_wf isl_wf int_seg_wf unit_wf2 nat_wf squash_wf decidable__assert nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermVar_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_wf le_wf seq-adjoin_wf subtype_rel_function int_seg_subtype_nat istype-false subtype_rel_self seq-add_wf decidable__equal_int intformeq_wf int_formula_prop_eq_lemma lt_int_wf eqtt_to_assert assert_of_lt_int less_than_wf eqff_to_assert int_subtype_base bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot iff_weakening_uiff true_wf set_subtype_base lelt_wf int_seg_properties intformless_wf int_formula_prop_less_lemma equal_wf iff_imp_equal_bool btrue_wf bfalse_wf btrue_neq_bfalse decidable__lt equal-wf-base-T int_seg_subtype sq_stable__le le_weakening2 subtract_wf itermSubtract_wf int_term_value_subtract_lemma primrec-wf2 add-zero not-le-2 condition-implies-le minus-add minus-one-mul add-swap minus-one-mul-top add-commutes add-associates add_functionality_wrt_le le-add-cancel2 add-member-int_seg2 subtract-add-cancel eq_int_wf assert_of_eq_int decidable__equal_nat neg_assert_of_eq_int add-mul-special zero-mul zero-add istype-top
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut Error :lambdaFormation_alt,  hypothesis promote_hyp thin sqequalHypSubstitution productElimination extract_by_obid isectElimination hypothesisEquality imageElimination because_Cache sqequalRule Error :lambdaEquality_alt,  natural_numberEquality setElimination rename applyEquality functionExtensionality Error :functionIsType,  Error :universeIsType,  Error :inhabitedIsType,  independent_functionElimination dependent_functionElimination imageMemberEquality baseClosed Error :dependent_set_memberEquality_alt,  addEquality unionElimination independent_isectElimination approximateComputation Error :dependent_pairFormation_alt,  int_eqEquality Error :isect_memberEquality_alt,  voidElimination independent_pairFormation Error :productIsType,  instantiate universeEquality equalityTransitivity equalitySymmetry Error :functionIsTypeImplies,  functionEquality Error :equalityIsType1,  equalityElimination Error :equalityIsType2,  baseApply closedConclusion cumulativity hyp_replacement Error :unionIsType,  Error :functionExtensionality_alt,  intEquality unionEquality applyLambdaEquality Error :equalityIsType4,  Error :inrEquality_alt,  Error :setIsType,  minusEquality int_eqReduceTrueSq int_eqReduceFalseSq lessCases axiomSqEquality

Latex:
\mforall{}[B,Q:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}.    (B[n;s]  {}\mRightarrow{}  (\mforall{}m:\mBbbN{}.  B[n  +  1;s.m@n])))
    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}.    (B[n;s]  {}\mRightarrow{}  (\mdownarrow{}Q[n;s])))
    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}.    ((\mforall{}m:\mBbbN{}.  (\mdownarrow{}Q[n  +  1;s.m@n]))  {}\mRightarrow{}  (\mdownarrow{}Q[n;s])))
    {}\mRightarrow{}  (\mforall{}alpha:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}m:\mBbbN{}.  B[m;alpha])
    {}\mRightarrow{}  (\mdownarrow{}Q[0;\mlambda{}x.\mbot{}]))



Date html generated: 2019_06_20-PM-02_54_11
Last ObjectModification: 2018_10_04-PM-11_40_07

Theory : continuity


Home Index