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: List uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q exists: x:A. B[x] member: t ∈ T prop: so_lambda: λ2x.t[x] so_apply: x[s] rev_implies:  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 ⊆B uimplies: supposing a cand: 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