- LENGTH_0
-
|- (LENGTH l = 0) ⇔ (l = [])
- IS_SUFFIX_MEM
-
|- IS_SUFFIX s (h::t) ⇒ MEM h s
- IS_PREFIX_MEM
-
|- ∀y. x ≼ y ⇒ ∀e. MEM e x ⇒ MEM e y
- MEM_LAST'
-
|- seq ≠ [] ⇒ MEM (LAST seq) seq
- lemma_2_1_1_2
-
|- ∀l1 l2. LENGTH l1 > LENGTH l2 ⇒ l1 ≠ l2
- LENGTH_INJ_PREFIXES
-
|- ∀x1 x2. x1 ≼ y ∧ x2 ≼ y ⇒ ((LENGTH x1 = LENGTH x2) ⇔ (x1 = x2))
- lemma_2_3_1_4
-
|- ∀l. l ≠ [] ⇒ FRONT l ≼ l
- non_empty_list
-
|- ∀l. l ≠ [] ⇒ ∃h t. l = h::t
- lemma_2_3_2_1
-
|- ∀l. LENGTH l ≥ 0
- lemma_2_3_2
-
|- ∀l l1 l2. LENGTH l2 > LENGTH l1 ∧ l1 ≼ l ∧ l2 ≼ l ⇒ l1 ≼ l2
- lemma_3_1
-
|- ∀l1 l2 l3. l2 ≠ [] ⇒ LENGTH (l1 ⧺ l3) < LENGTH (l1 ⧺ l2 ⧺ l3)
- graph_plan_lemma_19
-
|- ∀as s. set as ⊆ s ⇒ ∀a. MEM a as ⇒ a ∈ s
- twosorted_list_length
-
|- ∀P1 P2 l k1 k2.
(∀x. MEM x l ⇒ (¬P1 x ⇔ P2 x)) ∧ LENGTH (FILTER P1 l) < k1 ∧
(∀l'.
(∃pfx sfx. pfx ⧺ l' ⧺ sfx = l) ∧ (∀x. MEM x l' ⇒ P2 x) ⇒
LENGTH l' < k2) ⇒
LENGTH l < k1 * k2
- graph_plan_lemma_6_2
-
|- ∀P l s. set l ⊆ s ⇒ set (FILTER P l) ⊆ s
- graph_plan_lemma_8_1_1
-
|- ∀f1 f2 as1 as2 p.
(as1 ⧺ as2 = FILTER f1 (MAP f2 p)) ⇒
∃p_1 p_2.
(p_1 ⧺ p_2 = p) ∧ (as1 = FILTER f1 (MAP f2 p_1)) ∧
(as2 = FILTER f1 (MAP f2 p_2))
- graph_plan_lemma_8_1
-
|- ∀f1 f2 as1 as2 as3 p.
(as1 ⧺ as2 ⧺ as3 = FILTER f1 (MAP f2 p)) ⇒
∃p_1 p_2 p_3.
(p_1 ⧺ p_2 ⧺ p_3 = p) ∧ (as1 = FILTER f1 (MAP f2 p_1)) ∧
(as2 = FILTER f1 (MAP f2 p_2)) ∧ (as3 = FILTER f1 (MAP f2 p_3))
- graph_plan_lemma_8_1_1_light
-
|- ∀f1 f2 as1 as2 p.
(as1 ⧺ as2 = MAP f2 p) ⇒
∃p_1 p_2. (p_1 ⧺ p_2 = p) ∧ (as1 = MAP f2 p_1) ∧ (as2 = MAP f2 p_2)
- graph_plan_lemma_8_1_light
-
|- ∀f1 f2 as1 as2 as3 p.
(as1 ⧺ as2 ⧺ as3 = MAP f2 p) ⇒
∃p_1 p_2 p_3.
(p_1 ⧺ p_2 ⧺ p_3 = p) ∧ (as1 = MAP f2 p_1) ∧ (as2 = MAP f2 p_2) ∧
(as3 = MAP f2 p_3)
- graph_plan_lemma_14
-
|- ∀l f1 f2 x.
MEM x (MAP f1 l) ∧ f2 x ∧ (∀g. SND (f1 g) = SND g) ∧
(∀g h. (SND g = SND h) ⇒ (f2 g ⇔ f2 h)) ⇒
∃y. MEM y l ∧ f2 y
- graph_plan_lemma_15_1
-
|- ∀l1 l2 l3 P.
LENGTH (FILTER P l3) < LENGTH (FILTER P l2) ⇒
LENGTH (FILTER P (l1 ⧺ l3)) < LENGTH (FILTER P (l1 ⧺ l2))
- graph_plan_lemma_15_2
-
|- ∀l1 l2 l3 P.
LENGTH (FILTER P l3) < LENGTH (FILTER P l2) ⇒
LENGTH (FILTER P (l3 ⧺ l1)) < LENGTH (FILTER P (l2 ⧺ l1))
- graph_plan_lemma_15
-
|- ∀l1 l2 l3 l4 P.
LENGTH (FILTER P l2) < LENGTH (FILTER P l3) ⇒
LENGTH (FILTER P (l1 ⧺ l2 ⧺ l4)) < LENGTH (FILTER P (l1 ⧺ l3 ⧺ l4))
- graph_plan_lemma_20
-
|- ∀l P. EVERY P l ⇒ (LENGTH (FILTER P l) = LENGTH l)
- graph_plan_lemma_21
-
|- ∀P1 P2 l. EVERY P1 l ∧ EVERY P2 l ⇔ EVERY (λa. P1 a ∧ P2 a) l
- two_children_parent_bound_main_lemma_3_1_3
-
|- ∀P l. LENGTH (FILTER (λa. P a) l) + LENGTH (FILTER (λa. ¬P a) l) = LENGTH l
- child_parent_lemma_2_1_1_1_2
-
|- ∀P l. (∃x. MEM x l ∧ P x) ⇒ LENGTH (FILTER (λx. ¬P x) l) < LENGTH l
- FILTER_P_NOT_P_EMPTY
-
|- ∀P l. FILTER (λa. P a) (FILTER (λa. ¬P a) l) = []
- child_parent_lemma_2_1_1_1_3_1_1
-
|- ∀P l. LENGTH (FILTER (λa. P a) (FILTER (λa. ¬P a) l)) = 0
- child_parent_lemma_2_1_1_1_3_1
-
|- ∀P P2 l.
(∃a. MEM a l ∧ P a) ⇒
LENGTH (FILTER (λa. P a) (FILTER (λa. ¬P a ∧ P2 a) l)) <
LENGTH (FILTER (λa. P a) l)
- child_parent_lemma_2_1_2_2_2
-
|- ∀P l. (FILTER (λx. P x) l = []) ⇔ EVERY (λx. ¬P x) l
- list_frag_rec_ind
-
|- ∀P.
(∀h l h' l' h_orig l_original.
(h ≠ h' ∧ h ≠ h_orig ⇒ P (l,h_orig::l_original,h_orig::l_original)) ∧
(h ≠ h' ∧ (h = h_orig) ⇒ P (l,l_original,h_orig::l_original)) ∧
((h = h') ⇒ P (l,l',h_orig::l_original)) ⇒
P (h::l,h'::l',h_orig::l_original)) ∧ (∀l l'. P (l,[],l')) ∧
(∀h l l'. P ([],h::l,l')) ∧ (∀v8 v9 v4 v5. P (v8::v9,v4::v5,[])) ⇒
∀v v1 v2. P (v,v1,v2)
- list_frag_rec_def
-
|- (∀l_original l' l h_orig h' h.
list_frag_rec (h::l,h'::l',h_orig::l_original) ⇔
if h = h' then list_frag_rec (l,l',h_orig::l_original)
else if h = h_orig then list_frag_rec (l,l_original,h_orig::l_original)
else list_frag_rec (l,h_orig::l_original,h_orig::l_original)) ∧
(∀l' l. list_frag_rec (l,[],l') ⇔ T) ∧
(∀l' l h. list_frag_rec ([],h::l,l') ⇔ F) ∧
∀v9 v8 v5 v4. list_frag_rec (v8::v9,v4::v5,[]) ⇔ T
- child_parent_lemma_2_1_3_1_1_1_1
-
|- ∀l la x lb P.
list_frag (la ⧺ [x] ⧺ lb,l) ∧ ¬MEM x l ⇒
list_frag (la,l) ∨ list_frag (lb,l)
- child_parent_lemma_2_1_3_1_1_1
-
|- ∀l la x lb P.
list_frag (la ⧺ [x] ⧺ lb,l) ∧ ¬P x ∧ EVERY P l ⇒
list_frag (la,l) ∨ list_frag (lb,l)
- child_parent_lemma_2_1_3_1_1_2
-
|- ∀l' l. list_frag (l,l') ⇒ LENGTH l' ≤ LENGTH l
- child_parent_lemma_2_1_3_1_1
-
|- ∀Ch k1 Par f s l PProbs PProbl.
PProbs s ∧ PProbl l ∧
(∀l s.
PProbs s ∧ PProbl l ∧ EVERY Par l ⇒
∃l'.
(f (s,l') = f (s,l)) ∧ LENGTH l' ≤ k1 ∧ EVERY Par l' ∧ PProbl l') ∧
(∀a l. PProbl l ∧ MEM a l ⇒ (Ch a ⇔ ¬Par a)) ∧
(∀s l1 l2. f (f (s,l1),l2) = f (s,l1 ⧺ l2)) ∧
(∀l1 l2. PProbl (l1 ⧺ l2) ⇔ PProbl l1 ∧ PProbl l2) ∧
(∀s l. PProbs s ∧ PProbl l ⇒ PProbs (f (s,l))) ⇒
∃l'.
(f (s,l') = f (s,l)) ∧ (LENGTH (FILTER Ch l') = LENGTH (FILTER Ch l)) ∧
(∀l''. list_frag (l',l'') ∧ EVERY Par l'' ⇒ LENGTH l'' ≤ k1) ∧
PProbl l'
- child_parent_lemma_2_1_3_1
-
|- ∀k1 k2 s Par Ch f l PProbs PProbl.
PProbs s ∧ PProbl l ∧
(∀l s.
PProbs s ∧ PProbl l ∧ EVERY Par l ⇒
∃l'.
(f (s,l') = f (s,l)) ∧ LENGTH l' ≤ k1 ∧ EVERY Par l' ∧ PProbl l') ∧
(∀l s.
PProbs s ∧ PProbl l ⇒
∃l'. (f (s,l') = f (s,l)) ∧ LENGTH (FILTER Ch l') ≤ k2 ∧ PProbl l') ∧
(∀a l. PProbl l ∧ MEM a l ⇒ (Ch a ⇔ ¬Par a)) ∧
(∀s l1 l2. f (f (s,l1),l2) = f (s,l1 ⧺ l2)) ∧
(∀l1 l2. PProbl (l1 ⧺ l2) ⇔ PProbl l1 ∧ PProbl l2) ∧
(∀s l. PProbs s ∧ PProbl l ⇒ PProbs (f (s,l))) ⇒
∃l'.
(f (s,l') = f (s,l)) ∧ LENGTH (FILTER Ch l') ≤ k2 ∧
(∀l''. list_frag (l',l'') ∧ EVERY Par l'' ⇒ LENGTH l'' ≤ k1) ∧
PProbl l'
- EVERY_ABSORB
-
|- ∀P1 P2 l. EVERY P2 l ⇒ (FILTER (λx. P1 x ∧ P2 x) l = FILTER (λx. P1 x) l)
- parent_children_lemma_1_1_1_11_5_1
-
|- ∀P1 P2.
(∀x. P1 x ⇒ P2 x) ⇒
∀l. LENGTH (FILTER (λa. P1 a) (FILTER (λa. ¬P2 a) l)) = 0
- parent_children_lemma_1_1_1_11_5_2
-
|- ∀P1 P2 P3.
(∀x. P1 x ∧ P2 x ⇒ P3 x) ⇒
∀l. EVERY P2 l ⇒ (LENGTH (FILTER (λa. P1 a) (FILTER (λa. ¬P3 a) l)) = 0)
- parent_children_lemma_1_1_1_11_8
-
|- ∀l s. set l ⊆ s ⇒ EVERY (λx. x ∈ s) l
- parent_children_lemma_1_1_2_1
-
|- ∀P l' l. list_frag (l,l') ⇒ LENGTH (FILTER P l') ≤ LENGTH (FILTER P l)
- threesorted_list_length_1
-
|- ∀l. list_frag (l,l)
- threesorted_list_length_2
-
|- ∀l l'. list_frag (l ⧺ l',l)
- threesorted_list_length_3
-
|- ∀l l' l''. list_frag (l',l) ⇒ list_frag (l'' ⧺ l',l)
- threesorted_list_length
-
|- ∀P1 P2 l k1 k2.
LENGTH (FILTER P1 l) ≤ k1 ∧ (∀x. MEM x l ⇒ P1 x ⇒ ¬P2 x) ∧
(∀l'.
list_frag (l,l') ∧ EVERY (λx. ¬P1 x) l' ⇒
LENGTH (FILTER P2 l') ≤ k2) ⇒
LENGTH (FILTER P2 l) ≤ (k1 + 1) * k2
- parent_children_main_lemma_1_1_2_1
-
|- ∀x l. MEM x l ⇔ MEM x l
- parent_children_main_lemma_1_1_5_1_1
-
|- ∀P acc l. FOLDL (λx y. x ∧ P y) acc l ⇒ acc
- parent_children_main_lemma_1_1_5_1_2
-
|- ∀P acc acc' l.
(acc ⇒ acc') ∧ FOLDL (λx y. x ∧ P y) acc l ⇒ FOLDL (λx y. x ∧ P y) acc' l
- parent_children_main_lemma_1_1_5_1_3
-
|- ∀P acc l. FOLDL (λx y. x ∧ P y) T l ∧ acc ⇒ FOLDL (λx y. x ∧ P y) acc l
- parent_children_main_lemma_1_1_5_1
-
|- ∀P P' l.
(∀x. P x ⇒ P' x) ∧ FOLDL (λx y. x ∧ P y) T l ⇒ FOLDL (λx y. x ∧ P' y) T l
- parent_children_main_lemma_1_1_8_6
-
|- ∀x x' l.
MEM x l ∧ MEM x' l ∧ x ≠ x' ⇒
(∃pfx mid sfx. l = pfx ⧺ [x] ⧺ mid ⧺ [x'] ⧺ sfx) ∨
∃pfx mid sfx. l = pfx ⧺ [x'] ⧺ mid ⧺ [x] ⧺ sfx
- parent_children_main_lemma_1_1_9
-
|- ∀P P' lvs.
(∀vs. MEM vs lvs ∧ P vs ⇒ P' vs) ∧ EVERY (λvs'. P vs') lvs ⇒
EVERY (λvs'. P' vs') lvs
- parent_children_main_lemma_1_1_16_2
-
|- ∀f1 f2 P l.
EVERY (λx. ¬P x) l ⇒
(MAP (λx. if P x then f1 x else f2 x) l = MAP (λx. f2 x) l)
- parent_children_main_lemma_1_3
-
|- ∀l. FILTER (λx. T) l = l
- nondistinct_repeated_segment
-
|- ∀l. ¬ALL_DISTINCT l ⇒ ∃e l1 l2 l3. l = l1 ⧺ e::l2 ⧺ e::l3
- TAKE_isPREFIX
-
|- ∀m n l. m ≤ n ∧ n ≤ LENGTH l ⇒ TAKE m l ≼ TAKE n l
- N_gen_valid_thm_2
-
|- ∀f1 f2 l. (∀x. f1 x ≤ f2 x) ⇒ SUM (MAP f1 l) ≤ SUM (MAP f2 l)
- N_super_gen_valid_thm_2
-
|- ∀f1 f2 l. (∀x. MEM x l ⇒ f1 x ≤ f2 x) ⇒ SUM (MAP f1 l) ≤ SUM (MAP f2 l)
- MAP_LAMBDA_ABSTRACTION_thm
-
|- MAP f l = MAP (λx. f x) l
- FOLDL_TRUE_eq_EVERY_TRUE
-
|- FOLDL (λx y. x ∧ P y) T l ⇔ EVERY (λy. P y) l