### Nuprl Lemma : concat-decomp

`∀[T:Type]`
`  ∀ll:T List List. ∀x:T.`
`    ((x ∈ concat(ll))`
`    `⇐⇒` ∃ll1,ll2:T List List`
`         ∃l1,l2:T List`
`          ((concat(ll) = (concat(ll1) @ (l1 @ [x] @ l2) @ concat(ll2)) ∈ (T List))`
`          ∧ (ll = (ll1 @ [l1 @ [x] @ l2] @ ll2) ∈ (T List List))))`

Proof

Definitions occuring in Statement :  l_member: `(x ∈ l)` concat: `concat(ll)` append: `as @ bs` cons: `[a / b]` nil: `[]` list: `T List` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` and: `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` exists: `∃x:A. B[x]` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` rev_implies: `P `` Q` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` cand: `A c∧ B` or: `P ∨ Q` guard: `{T}`
Lemmas referenced :  exists_wf list_wf l_member_wf equal_wf concat_wf append_wf cons_wf nil_wf length_wf list_ind_cons_lemma list_ind_nil_lemma length-append member-concat iff_wf l_member_decomp length_wf_nat nat_wf concat_append concat-cons concat-nil append_nil_sq subtype_rel_list top_wf or_wf member_wf cons_member member_append
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut independent_pairFormation sqequalHypSubstitution productElimination thin introduction extract_by_obid isectElimination hypothesisEquality hypothesis sqequalRule lambdaEquality productEquality applyLambdaEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality addLevel independent_functionElimination because_Cache universeEquality dependent_set_memberEquality equalityTransitivity equalitySymmetry applyEquality independent_isectElimination hyp_replacement setElimination rename dependent_pairFormation unionElimination inlFormation inrFormation

Latex:
\mforall{}[T:Type]
\mforall{}ll:T  List  List.  \mforall{}x:T.
((x  \mmember{}  concat(ll))
\mLeftarrow{}{}\mRightarrow{}  \mexists{}ll1,ll2:T  List  List
\mexists{}l1,l2:T  List
((concat(ll)  =  (concat(ll1)  @  (l1  @  [x]  @  l2)  @  concat(ll2)))
\mwedge{}  (ll  =  (ll1  @  [l1  @  [x]  @  l2]  @  ll2))))

Date html generated: 2019_06_20-PM-01_46_25
Last ObjectModification: 2018_08_24-PM-11_48_13

Theory : list_1

Home Index