Nuprl Lemma : init-seg-nat-seq-append-implies-left

a,b,s:finite-nat-seq().  ((↑init-seg-nat-seq(a**b;s))  (↑init-seg-nat-seq(a;s)))


Proof




Definitions occuring in Statement :  init-seg-nat-seq: init-seg-nat-seq(f;g) append-finite-nat-seq: f**g finite-nat-seq: finite-nat-seq() assert: b all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q uall: [x:A]. B[x] exists: x:A. B[x] squash: T prop: true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  assert-init-seg-nat-seq append-finite-nat-seq_wf equal_wf squash_wf true_wf finite-nat-seq_wf append-finite-nat-seq-assoc iff_weakening_equal exists_wf assert_wf init-seg-nat-seq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis productElimination independent_functionElimination isectElimination because_Cache dependent_pairFormation applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality natural_numberEquality sqequalRule imageMemberEquality baseClosed independent_isectElimination hyp_replacement applyLambdaEquality

Latex:
\mforall{}a,b,s:finite-nat-seq().    ((\muparrow{}init-seg-nat-seq(a**b;s))  {}\mRightarrow{}  (\muparrow{}init-seg-nat-seq(a;s)))



Date html generated: 2017_04_20-AM-07_30_09
Last ObjectModification: 2017_02_27-PM-06_00_43

Theory : continuity


Home Index