Theory "sublist"

Parents     list_utils

Signature

Constant Type
sublist :α list -> α list -> bool

Theorems

sublist_every
|- ∀l1 l2 P. sublist l1 l2 ∧ EVERY P l2 ⇒ EVERY P l1
sublist_cons_2
|- ∀l1 l2 h. sublist (h::l1) (h::l2) ⇔ sublist l1 l2
sublist_cons_3
|- ∀l1 l2. sublist (h::l1) l2 ⇒ sublist l1 l2
sublist_filter
|- ∀l P. sublist (FILTER P l) l
sublist_subset
|- ∀l1 l2. sublist l1 l2 ⇒ set l1 ⊆ set l2
append_sublist
|- ∀l1 l2 l3 l. sublist (l1 ⧺ l2 ⧺ l3) l ⇒ sublist (l1 ⧺ l3) l
sublist_append_2
|- ∀l1 l2 l3. sublist l1 l2 ⇒ sublist l1 (l2 ⧺ l3)
sublist_append
|- ∀l1 l1' l2 l2'.
     sublist l1 l1' ∧ sublist l2 l2' ⇒ sublist (l1 ⧺ l2) (l1' ⧺ l2')
sublist_append_both_I
|- sublist a b ∧ sublist c d ⇒ sublist (a ⧺ c) (b ⧺ d)
sublist_SING_MEM
|- sublist [h] l ⇔ MEM h l
sublist_ind
|- ∀P.
     (∀l1. P [] l1) ∧ (∀h t. P (h::t) []) ∧
     (∀x l1 y l2. P l1 l2 ∧ P (x::l1) l2 ⇒ P (x::l1) (y::l2)) ⇒
     ∀v v1. P v v1
sublist_def
|- (∀l1. sublist [] l1 ⇔ T) ∧ (∀t h. sublist (h::t) [] ⇔ F) ∧
   ∀y x l2 l1.
     sublist (x::l1) (y::l2) ⇔ (x = y) ∧ sublist l1 l2 ∨ sublist (x::l1) l2
sublist_EQNS
|- (sublist [] l ⇔ T) ∧ (sublist (h::t) [] ⇔ F)
sublist_refl
|- ∀l. sublist l l
sublist_cons
|- ∀l1 l2 h. sublist l1 l2 ⇒ sublist l1 (h::l2)
sublist_NIL
|- sublist l1 [] ⇔ (l1 = [])
sublist_trans
|- ∀l1 l2 l3. sublist l1 l2 ∧ sublist l2 l3 ⇒ sublist l1 l3
sublist_length
|- ∀l l'. sublist l l' ⇒ LENGTH l ≤ LENGTH l'
sublist_CONS1_E
|- ∀l1 l2. sublist (h::l1) l2 ⇒ sublist l1 l2
sublist_equal_lengths
|- ∀l1 l2. sublist l1 l2 ∧ (LENGTH l1 = LENGTH l2) ⇒ (l1 = l2)
sublist_antisym
|- sublist l1 l2 ∧ sublist l2 l1 ⇒ (l1 = l2)
sublist_append_I
|- ∀l1 l2. sublist l1 (l2 ⧺ l1)
sublist_snoc
|- ∀l1 l2 h. sublist l1 l2 ⇒ sublist l1 (l2 ⧺ [h])
sublist_append_front
|- ∀l1 l2. sublist l1 (l1 ⧺ l2)
sublist_append1_E
|- sublist (l1 ⧺ l2) l ⇒ sublist l1 l ∧ sublist l2 l
append_sublist_1
|- sublist (l1 ⧺ l2) l ⇒ sublist l1 l ∧ sublist l2 l
sublist_cons_exists
|- ∀h l1 l2.
     sublist (h::l1) l2 ⇔
     ∃l2a l2b. (l2 = l2a ⧺ [h] ⧺ l2b) ∧ ¬MEM h l2a ∧ sublist l1 l2b
sublist_append_exists
|- ∀l1 l2 h. sublist (h::l1) l2 ⇒ ∃l3 l4. (l2 = l3 ⧺ [h] ⧺ l4) ∧ sublist l1 l4
sublist_append_4
|- ∀l l1 l2 h.
     sublist (h::l) (l1 ⧺ [h] ⧺ l2) ∧ EVERY (λx. h ≠ x) l1 ⇒ sublist l l2
sublist_append_5
|- ∀l l1 l2 h.
     sublist (h::l) (l1 ⧺ l2) ∧ EVERY (λx. h ≠ x) l1 ⇒ sublist (h::l) l2
sublist_append_6
|- ∀l l1 l2 h. sublist (h::l) (l1 ⧺ l2) ∧ ¬MEM h l1 ⇒ sublist (h::l) l2
sublist_MEM
|- ∀h l1 l2. sublist (h::l1) l2 ⇒ MEM h l2
graph_plan_lemma_7_8_1
|- ∀l h l'. sublist l l' ⇒ sublist l (h::l')
parent_children_main_lemma_1_1_13
|- ∀P l l'. sublist l' l ⇒ LENGTH (FILTER P l') ≤ LENGTH (FILTER P l)
parent_children_lemma_1_1_2
|- ∀P1 P2 P3 k1 f PProbs PProbl s l.
     PProbs s ∧ PProbl l ∧
     (∀l s.
        PProbs s ∧ PProbl l ∧ EVERY P1 l ⇒
        ∃l'.
          (f (s,l') = f (s,l)) ∧ LENGTH (FILTER P2 l') ≤ k1 ∧
          LENGTH (FILTER P3 l') ≤ LENGTH (FILTER P3 l) ∧ EVERY P1 l' ∧
          sublist l' l) ∧ (∀s l1 l2. f (f (s,l1),l2) = f (s,l1 ⧺ l2)) ∧
     (∀s l. PProbs s ∧ PProbl l ⇒ PProbs (f (s,l))) ∧
     (∀l1 l2. sublist l1 l2 ∧ PProbl l2 ⇒ PProbl l1) ∧
     (∀l1 l2. PProbl (l1 ⧺ l2) ⇔ PProbl l1 ∧ PProbl l2) ⇒
     ∃l'.
       (f (s,l') = f (s,l)) ∧ LENGTH (FILTER P3 l') ≤ LENGTH (FILTER P3 l) ∧
       (∀l''.
          list_frag (l',l'') ∧ EVERY P1 l'' ⇒ LENGTH (FILTER P2 l'') ≤ k1) ∧
       sublist l' l
isPREFIX_sublist
|- ∀x y. x ≼ y ⇒ sublist x y