### Nuprl Lemma : append-finite-nat-seq-1

`∀n,a,b:finite-nat-seq(). ∀x:ℕ.`
`  ((↑init-seg-nat-seq(n**λi.x^(1);a**b)) `` ((↑init-seg-nat-seq(a;n)) ∨ (↑init-seg-nat-seq(n**λi.x^(1);a))))`

Proof

Definitions occuring in Statement :  init-seg-nat-seq: `init-seg-nat-seq(f;g)` append-finite-nat-seq: `f**g` mk-finite-nat-seq: `f^(n)` finite-nat-seq: `finite-nat-seq()` nat: `ℕ` assert: `↑b` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` lambda: `λx.A[x]` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` nat: `ℕ` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` finite-nat-seq: `finite-nat-seq()` decidable: `Dec(P)` or: `P ∨ Q` mk-finite-nat-seq: `f^(n)` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` append-finite-nat-seq: `f**g` pi1: `fst(t)` pi2: `snd(t)` int_seg: `{i..j-}` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` uimplies: `b supposing a` less_than: `a < b` top: `Top` true: `True` squash: `↓T` lelt: `i ≤ j < k` bfalse: `ff` exists: `∃x:A. B[x]` sq_type: `SQType(T)` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b` ge: `i ≥ j ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  assert_wf init-seg-nat-seq_wf append-finite-nat-seq_wf mk-finite-nat-seq_wf false_wf le_wf int_seg_wf nat_wf finite-nat-seq_wf decidable__le assert-init-seg-nat-seq2 lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int top_wf less_than_wf lelt_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot int_seg_properties nat_properties decidable__equal_int full-omega-unsat intformand_wf intformnot_wf intformless_wf itermVar_wf itermAdd_wf itermConstant_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf subtype_rel_function int_seg_subtype add-is-int-iff set_subtype_base int_subtype_base subtype_rel_self intformeq_wf itermSubtract_wf int_formula_prop_eq_lemma int_term_value_subtract_lemma decidable__lt
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_set_memberEquality natural_numberEquality sqequalRule independent_pairFormation hypothesis lambdaEquality productElimination rename dependent_functionElimination addEquality setElimination unionElimination inrFormation functionExtensionality applyEquality because_Cache independent_functionElimination equalityElimination equalityTransitivity equalitySymmetry independent_isectElimination lessCases isect_memberFormation axiomSqEquality isect_memberEquality voidElimination voidEquality imageMemberEquality baseClosed imageElimination dependent_pairFormation promote_hyp instantiate cumulativity approximateComputation int_eqEquality intEquality hyp_replacement applyLambdaEquality functionEquality baseApply closedConclusion inlFormation

Latex:
\mforall{}n,a,b:finite-nat-seq().  \mforall{}x:\mBbbN{}.
((\muparrow{}init-seg-nat-seq(n**\mlambda{}i.x\^{}(1);a**b))
{}\mRightarrow{}  ((\muparrow{}init-seg-nat-seq(a;n))  \mvee{}  (\muparrow{}init-seg-nat-seq(n**\mlambda{}i.x\^{}(1);a))))

Date html generated: 2019_06_20-PM-03_03_42
Last ObjectModification: 2018_08_20-PM-09_41_20

Theory : continuity

Home Index