Nuprl Lemma : unsquashed-monotone-bar-induction8-false

¬(∀Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ
    ((∀n:ℕ. ∀s:ℕn ⟶ ℕ.  ((∀m:ℕQ[n 1;s.m@n])  Q[n;s]))  (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. Q[m;f]))  Q[0;λx.⊥]))


Proof




Definitions occuring in Statement :  quotient: x,y:A//B[x; y] seq-add: s.x@n int_upper: {i...} int_seg: {i..j-} nat: bottom: prop: so_apply: x[s1;s2] all: x:A. B[x] exists: x:A. B[x] not: ¬A implies:  Q true: True lambda: λx.A[x] function: x:A ⟶ B[x] add: m natural_number: $n
Definitions unfolded in proof :  not: ¬A implies:  Q all: x:A. B[x] member: t ∈ T false: False prop: uall: [x:A]. B[x] subtype_rel: A ⊆B nat: so_lambda: λ2x.t[x] so_apply: x[s1;s2] ge: i ≥  decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top and: P ∧ Q so_apply: x[s] int_upper: {i...} le: A ≤ B less_than': less_than'(a;b) so_lambda: λ2y.t[x; y] guard: {T} int_seg: {i..j-} lelt: i ≤ j < k squash: T true: True iff: ⇐⇒ Q rev_implies:  Q less_than: a < b
Lemmas referenced :  unsquashed-weak-continuity-false2 nat_wf all_wf int_seg_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermVar_wf int_formula_prop_and_lemma 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-add_wf quotient_wf exists_wf int_upper_wf int_upper_subtype_nat subtype_rel_dep_function int_seg_subtype_nat false_wf subtype_rel_self true_wf equiv_rel_true int_seg_properties intformless_wf int_formula_prop_less_lemma equal_wf rep-seq-from_wf int_upper_properties int_upper_subtype_int_upper rep-seq-from-prop3 squash_wf iff_weakening_equal strong-continuity2-implies-weak implies-quotient-true decidable__lt lelt_wf rep-seq-from-prop1 rep-seq-from-0
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution independent_functionElimination thin functionEquality hypothesis voidElimination instantiate isectElimination applyEquality lambdaEquality cumulativity hypothesisEquality universeEquality sqequalRule natural_numberEquality setElimination rename because_Cache functionExtensionality dependent_set_memberEquality addEquality dependent_functionElimination unionElimination independent_isectElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidEquality independent_pairFormation computeAll productElimination applyLambdaEquality equalityTransitivity equalitySymmetry imageElimination imageMemberEquality baseClosed hyp_replacement

Latex:
\mneg{}(\mforall{}Q:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}
        ((\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}.    ((\mforall{}m:\mBbbN{}.  Q[n  +  1;s.m@n])  {}\mRightarrow{}  Q[n;s]))
        {}\mRightarrow{}  (\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \00D9(\mexists{}n:\mBbbN{}.  \mforall{}m:\{n...\}.  Q[m;f]))
        {}\mRightarrow{}  Q[0;\mlambda{}x.\mbot{}]))



Date html generated: 2017_04_20-AM-07_21_25
Last ObjectModification: 2017_02_27-PM-05_57_33

Theory : continuity


Home Index