### Nuprl Lemma : iseg-append-one

`∀[T:Type]. ∀L1,L2:T List. ∀x:T.  (L1 ≤ L2 @ [x] `⇐⇒` L1 ≤ L2 ∨ (L1 = (L2 @ [x]) ∈ (T List)))`

Proof

Definitions occuring in Statement :  iseg: `l1 ≤ l2` append: `as @ bs` cons: `[a / b]` nil: `[]` list: `T List` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` or: `P ∨ Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` rev_implies: `P `` Q` or: `P ∨ Q` guard: `{T}` exists: `∃x:A. B[x]` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` false: `False` cons: `[a / b]` top: `Top` bfalse: `ff` true: `True` subtype_rel: `A ⊆r B` uimplies: `b supposing a`
Lemmas referenced :  iseg_wf append_wf cons_wf nil_wf or_wf equal_wf list_wf iseg_append_iff iseg_single list-cases null_nil_lemma length_of_nil_lemma product_subtype_list null_cons_lemma length_of_cons_lemma squash_wf true_wf iff_weakening_equal iseg_append iseg_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality hypothesis universeEquality dependent_functionElimination productElimination independent_functionElimination unionElimination inlFormation sqequalRule inrFormation imageElimination voidElimination promote_hyp hypothesis_subsumption isect_memberEquality voidEquality applyEquality lambdaEquality equalityTransitivity equalitySymmetry because_Cache natural_numberEquality imageMemberEquality baseClosed independent_isectElimination hyp_replacement applyLambdaEquality

Latex:
\mforall{}[T:Type].  \mforall{}L1,L2:T  List.  \mforall{}x:T.    (L1  \mleq{}  L2  @  [x]  \mLeftarrow{}{}\mRightarrow{}  L1  \mleq{}  L2  \mvee{}  (L1  =  (L2  @  [x])))

Date html generated: 2017_04_17-AM-08_47_37
Last ObjectModification: 2017_02_27-PM-05_04_30

Theory : list_1

Home Index