- 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