### Nuprl Lemma : howard-bar-rec_wf

`∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ. ∀bar:∀s:ℕ ⟶ ℕ. ⇃(∃n:ℕ. B[n;s]). ∀mon:∀n:ℕ. ∀m:ℕn. ∀s:ℕn ⟶ ℕ.  (B[m;s] `` B[n;s]).`
`∀base:∀n:ℕ. ∀s:ℕn ⟶ ℕ.  (B[n;s] `` Q[n;s]). ∀ind:∀n:ℕ. ∀s:ℕn ⟶ ℕ.  ((∀m:ℕ. Q[n + 1;s.m@n]) `` Q[n;s]).`
`  ⇃(Q[0;seq-normalize(0;⊥)])`

Proof

Definitions occuring in Statement :  quotient: `x,y:A//B[x; y]` seq-normalize: `seq-normalize(n;s)` seq-add: `s.x@n` int_seg: `{i..j-}` nat: `ℕ` bottom: `⊥` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` true: `True` function: `x:A ⟶ B[x]` add: `n + m` natural_number: `\$n`
Definitions unfolded in proof :  so_lambda: `λ2x y.t[x; y]` lelt: `i ≤ j < k` guard: `{T}` int_seg: `{i..j-}` less_than': `less_than'(a;b)` le: `A ≤ B` subtype_rel: `A ⊆r B` so_apply: `x[s]` and: `P ∧ Q` top: `Top` not: `¬A` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` uimplies: `b supposing a` or: `P ∨ Q` decidable: `Dec(P)` ge: `i ≥ j ` so_apply: `x[s1;s2]` implies: `P `` Q` nat: `ℕ` so_lambda: `λ2x.t[x]` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` all: `∀x:A. B[x]` isl: `isl(x)` squash: `↓T` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` true: `True` howard-bar-rec: `howard-bar-rec(M;mon;base;ind;n;s)` bfalse: `ff` sq_stable: `SqStable(P)` ext2Baire: `ext2Baire(n;f;d)` bool: `𝔹` unit: `Unit` it: `⋅` uiff: `uiff(P;Q)` sq_type: `SQType(T)` bnot: `¬bb` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` seq-add: `s.x@n`
Lemmas referenced :  equiv_rel_true true_wf exists_wf quotient_wf subtype_rel_self int_formula_prop_less_lemma intformless_wf int_seg_properties int_seg_subtype subtype_rel_dep_function false_wf int_seg_subtype_nat seq-add_wf le_wf int_formula_prop_wf int_term_value_var_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermAdd_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_properties int_seg_wf nat_wf all_wf strong-continuity-rel-unique-pair subtype_rel_function istype-false istype-nat implies-quotient-true ext2Baire_wf full-omega-unsat istype-int istype-void istype-le unit_wf2 equal_wf assert_wf equal-wf-base set_subtype_base int_subtype_base seq-normalize_wf istype-assert btrue_wf bfalse_wf seq-normalize-equal isl_wf sq_stable__le le_weakening2 lt_int_wf eqtt_to_assert assert_of_lt_int eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot iff_weakening_uiff less_than_wf istype-less_than
Rules used in proof :  cumulativity productElimination universeEquality computeAll independent_pairFormation voidEquality voidElimination isect_memberEquality intEquality int_eqEquality dependent_pairFormation independent_isectElimination unionElimination dependent_functionElimination addEquality dependent_set_memberEquality hypothesisEquality functionExtensionality applyEquality because_Cache rename setElimination natural_numberEquality functionEquality lambdaEquality sqequalRule hypothesis thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution Error :lambdaEquality_alt,  Error :lambdaFormation_alt,  Error :functionIsType,  Error :inhabitedIsType,  closedConclusion unionEquality productEquality Error :dependent_set_memberEquality_alt,  approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  Error :isect_memberEquality_alt,  Error :universeIsType,  Error :inlEquality_alt,  Error :dependent_pairEquality_alt,  Error :equalityIstype,  equalityTransitivity equalitySymmetry Error :unionIsType,  Error :productIsType,  imageElimination SquashedBarInduction hyp_replacement applyLambdaEquality instantiate imageMemberEquality baseClosed Error :functionExtensionality_alt,  equalityElimination promote_hyp

Latex:
\mforall{}B,Q:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}.  \mforall{}bar:\mforall{}s:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \00D9(\mexists{}n:\mBbbN{}.  B[n;s]).  \mforall{}mon:\mforall{}n:\mBbbN{}.  \mforall{}m:\mBbbN{}n.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}.
(B[m;s]  {}\mRightarrow{}  B[n;s]).
\mforall{}base:\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}.    (B[n;s]  {}\mRightarrow{}  Q[n;s]).  \mforall{}ind:\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}.
((\mforall{}m:\mBbbN{}.  Q[n  +  1;s.m@n])  {}\mRightarrow{}  Q[n;s]).
\00D9(Q[0;seq-normalize(0;\mbot{})])

Date html generated: 2019_06_20-PM-03_06_11
Last ObjectModification: 2019_01_13-AM-09_04_24

Theory : continuity

Home Index