diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean index 99e7ecfe24..1d6ae04b9d 100644 --- a/library/data/finset/basic.lean +++ b/library/data/finset/basic.lean @@ -238,54 +238,54 @@ calc ∅ ∪ s = s ∪ ∅ : union.comm ... = s : union_empty end union -/- intersection -/ -section intersection +/- inter -/ +section inter variable [h : decidable_eq A] include h -definition intersection (s₁ s₂ : finset A) : finset A := +definition inter (s₁ s₂ : finset A) : finset A := quot.lift_on₂ s₁ s₂ (λ l₁ l₂, - to_finset_of_nodup (list.intersection (elt_of l₁) (elt_of l₂)) - (nodup_intersection_of_nodup _ (has_property l₁))) - (λ v₁ v₂ w₁ w₂ p₁ p₂, quot.sound (perm_intersection p₁ p₂)) + to_finset_of_nodup (list.inter (elt_of l₁) (elt_of l₂)) + (nodup_inter_of_nodup _ (has_property l₁))) + (λ v₁ v₂ w₁ w₂ p₁ p₂, quot.sound (perm_inter p₁ p₂)) -notation s₁ ∩ s₂ := intersection s₁ s₂ +notation s₁ ∩ s₂ := inter s₁ s₂ -theorem mem_of_mem_intersection_left {a : A} {s₁ s₂ : finset A} : a ∈ s₁ ∩ s₂ → a ∈ s₁ := -quot.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁l₂, list.mem_of_mem_intersection_left ainl₁l₂) +theorem mem_of_mem_inter_left {a : A} {s₁ s₂ : finset A} : a ∈ s₁ ∩ s₂ → a ∈ s₁ := +quot.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁l₂, list.mem_of_mem_inter_left ainl₁l₂) -theorem mem_of_mem_intersection_right {a : A} {s₁ s₂ : finset A} : a ∈ s₁ ∩ s₂ → a ∈ s₂ := -quot.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁l₂, list.mem_of_mem_intersection_right ainl₁l₂) +theorem mem_of_mem_inter_right {a : A} {s₁ s₂ : finset A} : a ∈ s₁ ∩ s₂ → a ∈ s₂ := +quot.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁l₂, list.mem_of_mem_inter_right ainl₁l₂) -theorem mem_intersection_of_mem_of_mem {a : A} {s₁ s₂ : finset A} : a ∈ s₁ → a ∈ s₂ → a ∈ s₁ ∩ s₂ := -quot.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁ ainl₂, list.mem_intersection_of_mem_of_mem ainl₁ ainl₂) +theorem mem_inter_of_mem_of_mem {a : A} {s₁ s₂ : finset A} : a ∈ s₁ → a ∈ s₂ → a ∈ s₁ ∩ s₂ := +quot.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁ ainl₂, list.mem_inter_of_mem_of_mem ainl₁ ainl₂) -theorem mem_intersection_eq (a : A) (s₁ s₂ : finset A) : (a ∈ s₁ ∩ s₂) = (a ∈ s₁ ∧ a ∈ s₂) := +theorem mem_inter_eq (a : A) (s₁ s₂ : finset A) : (a ∈ s₁ ∩ s₂) = (a ∈ s₁ ∧ a ∈ s₂) := propext (iff.intro - (λ h, and.intro (mem_of_mem_intersection_left h) (mem_of_mem_intersection_right h)) - (λ h, mem_intersection_of_mem_of_mem (and.elim_left h) (and.elim_right h))) + (λ h, and.intro (mem_of_mem_inter_left h) (mem_of_mem_inter_right h)) + (λ h, mem_inter_of_mem_of_mem (and.elim_left h) (and.elim_right h))) -theorem intersection.comm (s₁ s₂ : finset A) : s₁ ∩ s₂ = s₂ ∩ s₁ := -ext (λ a, by rewrite [*mem_intersection_eq]; exact and.comm) +theorem inter.comm (s₁ s₂ : finset A) : s₁ ∩ s₂ = s₂ ∩ s₁ := +ext (λ a, by rewrite [*mem_inter_eq]; exact and.comm) -theorem intersection.assoc (s₁ s₂ s₃ : finset A) : (s₁ ∩ s₂) ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) := -ext (λ a, by rewrite [*mem_intersection_eq]; exact and.assoc) +theorem inter.assoc (s₁ s₂ s₃ : finset A) : (s₁ ∩ s₂) ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) := +ext (λ a, by rewrite [*mem_inter_eq]; exact and.assoc) -theorem intersection_self (s : finset A) : s ∩ s = s := +theorem inter_self (s : finset A) : s ∩ s = s := ext (λ a, iff.intro - (λ h, mem_of_mem_intersection_right h) - (λ h, mem_intersection_of_mem_of_mem h h)) + (λ h, mem_of_mem_inter_right h) + (λ h, mem_inter_of_mem_of_mem h h)) -theorem intersection_empty (s : finset A) : s ∩ ∅ = ∅ := +theorem inter_empty (s : finset A) : s ∩ ∅ = ∅ := ext (λ a, iff.intro - (λ h : a ∈ s ∩ ∅, absurd (mem_of_mem_intersection_right h) !not_mem_empty) + (λ h : a ∈ s ∩ ∅, absurd (mem_of_mem_inter_right h) !not_mem_empty) (λ h : a ∈ ∅, absurd h !not_mem_empty)) -theorem empty_intersection (s : finset A) : ∅ ∩ s = ∅ := -calc ∅ ∩ s = s ∩ ∅ : intersection.comm - ... = ∅ : intersection_empty -end intersection +theorem empty_inter (s : finset A) : ∅ ∩ s = ∅ := +calc ∅ ∩ s = s ∩ ∅ : inter.comm + ... = ∅ : inter_empty +end inter /- subset -/ definition subset (s₁ s₂ : finset A) : Prop := @@ -330,3 +330,4 @@ theorem mem_upto_of_lt {n a : nat} : a < n → a ∈ upto n := list.mem_upto_of_lt end upto end finset +abbreviation finset := finset.finset diff --git a/library/data/finset/comb.lean b/library/data/finset/comb.lean index 89fb3ce96f..ceb24da023 100644 --- a/library/data/finset/comb.lean +++ b/library/data/finset/comb.lean @@ -59,11 +59,11 @@ quot.induction_on s (λ l h₁ h₂, list.all_insert_of_all h₁ h₂) theorem all_erase_of_all {p : A → Prop} (a : A) {s : finset A}: all s p → all (erase a s) p := quot.induction_on s (λ l h, list.all_erase_of_all a h) -theorem all_intersection_of_all_left {p : A → Prop} {s₁ : finset A} (s₂ : finset A) : all s₁ p → all (s₁ ∩ s₂) p := -quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h, list.all_intersection_of_all_left _ h) +theorem all_inter_of_all_left {p : A → Prop} {s₁ : finset A} (s₂ : finset A) : all s₁ p → all (s₁ ∩ s₂) p := +quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h, list.all_inter_of_all_left _ h) -theorem all_intersection_of_all_right {p : A → Prop} {s₁ : finset A} (s₂ : finset A) : all s₂ p → all (s₁ ∩ s₂) p := -quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h, list.all_intersection_of_all_right _ h) +theorem all_inter_of_all_right {p : A → Prop} {s₁ : finset A} (s₂ : finset A) : all s₂ p → all (s₁ ∩ s₂) p := +quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h, list.all_inter_of_all_right _ h) end all section cross_product diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index 32176a6478..3c2a234eba 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -641,48 +641,48 @@ assume p, by_cases by rewrite [insert_eq_of_not_mem nainl₁, insert_eq_of_not_mem nainl₂]; exact (skip _ p)) end perm_insert -section perm_intersection +section perm_inter variable [H : decidable_eq A] include H -theorem perm_intersection_left {l₁ l₂ : list A} (t₁ : list A) : l₁ ~ l₂ → (intersection l₁ t₁) ~ (intersection l₂ t₁) := +theorem perm_inter_left {l₁ l₂ : list A} (t₁ : list A) : l₁ ~ l₂ → (inter l₁ t₁) ~ (inter l₂ t₁) := assume p, perm.induction_on p !refl (λ x l₁ l₂ p₁ r₁, by_cases - (λ xint₁ : x ∈ t₁, by rewrite [*intersection_cons_of_mem _ xint₁]; exact (skip x r₁)) - (λ nxint₁ : x ∉ t₁, by rewrite [*intersection_cons_of_not_mem _ nxint₁]; exact r₁)) + (λ xint₁ : x ∈ t₁, by rewrite [*inter_cons_of_mem _ xint₁]; exact (skip x r₁)) + (λ nxint₁ : x ∉ t₁, by rewrite [*inter_cons_of_not_mem _ nxint₁]; exact r₁)) (λ x y l, by_cases (λ yint : y ∈ t₁, by_cases (λ xint : x ∈ t₁, - by rewrite [*intersection_cons_of_mem _ xint, *intersection_cons_of_mem _ yint, *intersection_cons_of_mem _ xint]; + by rewrite [*inter_cons_of_mem _ xint, *inter_cons_of_mem _ yint, *inter_cons_of_mem _ xint]; exact !swap) (λ nxint : x ∉ t₁, - by rewrite [*intersection_cons_of_mem _ yint, *intersection_cons_of_not_mem _ nxint, intersection_cons_of_mem _ yint]; + by rewrite [*inter_cons_of_mem _ yint, *inter_cons_of_not_mem _ nxint, inter_cons_of_mem _ yint]; exact !refl)) (λ nyint : y ∉ t₁, by_cases (λ xint : x ∈ t₁, - by rewrite [*intersection_cons_of_mem _ xint, *intersection_cons_of_not_mem _ nyint, intersection_cons_of_mem _ xint]; + by rewrite [*inter_cons_of_mem _ xint, *inter_cons_of_not_mem _ nyint, inter_cons_of_mem _ xint]; exact !refl) (λ nxint : x ∉ t₁, - by rewrite [*intersection_cons_of_not_mem _ nxint, *intersection_cons_of_not_mem _ nyint, - intersection_cons_of_not_mem _ nxint]; + by rewrite [*inter_cons_of_not_mem _ nxint, *inter_cons_of_not_mem _ nyint, + inter_cons_of_not_mem _ nxint]; exact !refl))) (λ l₁ l₂ l₃ p₁ p₂ r₁ r₂, trans r₁ r₂) -theorem perm_intersection_right (l : list A) {t₁ t₂ : list A} : t₁ ~ t₂ → (intersection l t₁) ~ (intersection l t₂) := +theorem perm_inter_right (l : list A) {t₁ t₂ : list A} : t₁ ~ t₂ → (inter l t₁) ~ (inter l t₂) := list.induction_on l - (λ p, by rewrite [*intersection_nil]; exact !refl) + (λ p, by rewrite [*inter_nil]; exact !refl) (λ x xs r p, by_cases (λ xint₁ : x ∈ t₁, assert xint₂ : x ∈ t₂, from mem_perm p xint₁, - by rewrite [intersection_cons_of_mem _ xint₁, intersection_cons_of_mem _ xint₂]; exact (skip _ (r p))) + by rewrite [inter_cons_of_mem _ xint₁, inter_cons_of_mem _ xint₂]; exact (skip _ (r p))) (λ nxint₁ : x ∉ t₁, assert nxint₂ : x ∉ t₂, from not_mem_perm p nxint₁, - by rewrite [intersection_cons_of_not_mem _ nxint₁, intersection_cons_of_not_mem _ nxint₂]; exact (r p))) + by rewrite [inter_cons_of_not_mem _ nxint₁, inter_cons_of_not_mem _ nxint₂]; exact (r p))) -theorem perm_intersection {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (intersection l₁ t₁) ~ (intersection l₂ t₂) := -assume p₁ p₂, trans (perm_intersection_left t₁ p₁) (perm_intersection_right l₂ p₂) -end perm_intersection +theorem perm_inter {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (inter l₁ t₁) ~ (inter l₂ t₂) := +assume p₁ p₂, trans (perm_inter_left t₁ p₁) (perm_inter_right l₂ p₂) +end perm_inter /- extensionality -/ section ext diff --git a/library/data/list/set.lean b/library/data/list/set.lean index 3a3f9cb42c..f05bb96784 100644 --- a/library/data/list/set.lean +++ b/library/data/list/set.lean @@ -652,103 +652,103 @@ assume h₁ h₂, by_cases (λ nainl : a ∉ l, by rewrite [insert_eq_of_not_mem nainl]; exact (all_cons_of_all h₁ h₂)) end insert -/- intersection -/ -section intersection +/- inter -/ +section inter variable {A : Type} variable [H : decidable_eq A] include H -definition intersection : list A → list A → list A +definition inter : list A → list A → list A | [] l₂ := [] -| (a::l₁) l₂ := if a ∈ l₂ then a :: intersection l₁ l₂ else intersection l₁ l₂ +| (a::l₁) l₂ := if a ∈ l₂ then a :: inter l₁ l₂ else inter l₁ l₂ -theorem intersection_nil (l : list A) : intersection [] l = [] +theorem inter_nil (l : list A) : inter [] l = [] -theorem intersection_cons_of_mem {a : A} (l₁ : list A) {l₂} : a ∈ l₂ → intersection (a::l₁) l₂ = a :: intersection l₁ l₂ := +theorem inter_cons_of_mem {a : A} (l₁ : list A) {l₂} : a ∈ l₂ → inter (a::l₁) l₂ = a :: inter l₁ l₂ := assume i, if_pos i -theorem intersection_cons_of_not_mem {a : A} (l₁ : list A) {l₂} : a ∉ l₂ → intersection (a::l₁) l₂ = intersection l₁ l₂ := +theorem inter_cons_of_not_mem {a : A} (l₁ : list A) {l₂} : a ∉ l₂ → inter (a::l₁) l₂ = inter l₁ l₂ := assume i, if_neg i -theorem mem_of_mem_intersection_left : ∀ {l₁ l₂} {a : A}, a ∈ intersection l₁ l₂ → a ∈ l₁ +theorem mem_of_mem_inter_left : ∀ {l₁ l₂} {a : A}, a ∈ inter l₁ l₂ → a ∈ l₁ | [] l₂ a i := absurd i !not_mem_nil | (b::l₁) l₂ a i := by_cases (λ binl₂ : b ∈ l₂, - have aux : a ∈ b :: intersection l₁ l₂, by rewrite [intersection_cons_of_mem _ binl₂ at i]; exact i, + have aux : a ∈ b :: inter l₁ l₂, by rewrite [inter_cons_of_mem _ binl₂ at i]; exact i, or.elim (eq_or_mem_of_mem_cons aux) (λ aeqb : a = b, by rewrite [aeqb]; exact !mem_cons) - (λ aini, mem_cons_of_mem _ (mem_of_mem_intersection_left aini))) + (λ aini, mem_cons_of_mem _ (mem_of_mem_inter_left aini))) (λ nbinl₂ : b ∉ l₂, - have ainl₁ : a ∈ l₁, by rewrite [intersection_cons_of_not_mem _ nbinl₂ at i]; exact (mem_of_mem_intersection_left i), + have ainl₁ : a ∈ l₁, by rewrite [inter_cons_of_not_mem _ nbinl₂ at i]; exact (mem_of_mem_inter_left i), mem_cons_of_mem _ ainl₁) -theorem mem_of_mem_intersection_right : ∀ {l₁ l₂} {a : A}, a ∈ intersection l₁ l₂ → a ∈ l₂ +theorem mem_of_mem_inter_right : ∀ {l₁ l₂} {a : A}, a ∈ inter l₁ l₂ → a ∈ l₂ | [] l₂ a i := absurd i !not_mem_nil | (b::l₁) l₂ a i := by_cases (λ binl₂ : b ∈ l₂, - have aux : a ∈ b :: intersection l₁ l₂, by rewrite [intersection_cons_of_mem _ binl₂ at i]; exact i, + have aux : a ∈ b :: inter l₁ l₂, by rewrite [inter_cons_of_mem _ binl₂ at i]; exact i, or.elim (eq_or_mem_of_mem_cons aux) (λ aeqb : a = b, by rewrite [aeqb]; exact binl₂) - (λ aini : a ∈ intersection l₁ l₂, mem_of_mem_intersection_right aini)) + (λ aini : a ∈ inter l₁ l₂, mem_of_mem_inter_right aini)) (λ nbinl₂ : b ∉ l₂, - by rewrite [intersection_cons_of_not_mem _ nbinl₂ at i]; exact (mem_of_mem_intersection_right i)) + by rewrite [inter_cons_of_not_mem _ nbinl₂ at i]; exact (mem_of_mem_inter_right i)) -theorem mem_intersection_of_mem_of_mem : ∀ {l₁ l₂} {a : A}, a ∈ l₁ → a ∈ l₂ → a ∈ intersection l₁ l₂ +theorem mem_inter_of_mem_of_mem : ∀ {l₁ l₂} {a : A}, a ∈ l₁ → a ∈ l₂ → a ∈ inter l₁ l₂ | [] l₂ a i₁ i₂ := absurd i₁ !not_mem_nil | (b::l₁) l₂ a i₁ i₂ := by_cases (λ binl₂ : b ∈ l₂, or.elim (eq_or_mem_of_mem_cons i₁) (λ aeqb : a = b, - by rewrite [intersection_cons_of_mem _ binl₂, aeqb]; exact !mem_cons) + by rewrite [inter_cons_of_mem _ binl₂, aeqb]; exact !mem_cons) (λ ainl₁ : a ∈ l₁, - by rewrite [intersection_cons_of_mem _ binl₂]; + by rewrite [inter_cons_of_mem _ binl₂]; apply mem_cons_of_mem; - exact (mem_intersection_of_mem_of_mem ainl₁ i₂))) + exact (mem_inter_of_mem_of_mem ainl₁ i₂))) (λ nbinl₂ : b ∉ l₂, or.elim (eq_or_mem_of_mem_cons i₁) (λ aeqb : a = b, absurd (aeqb ▸ i₂) nbinl₂) (λ ainl₁ : a ∈ l₁, - by rewrite [intersection_cons_of_not_mem _ nbinl₂]; exact (mem_intersection_of_mem_of_mem ainl₁ i₂))) + by rewrite [inter_cons_of_not_mem _ nbinl₂]; exact (mem_inter_of_mem_of_mem ainl₁ i₂))) -theorem nodup_intersection_of_nodup : ∀ {l₁ : list A} (l₂), nodup l₁ → nodup (intersection l₁ l₂) +theorem nodup_inter_of_nodup : ∀ {l₁ : list A} (l₂), nodup l₁ → nodup (inter l₁ l₂) | [] l₂ d := nodup_nil | (a::l₁) l₂ d := - have d₁ : nodup l₁, from nodup_of_nodup_cons d, - assert d₂ : nodup (intersection l₁ l₂), from nodup_intersection_of_nodup _ d₁, - have nainl₁ : a ∉ l₁, from not_mem_of_nodup_cons d, - assert naini : a ∉ intersection l₁ l₂, from λ i, absurd (mem_of_mem_intersection_left i) nainl₁, + have d₁ : nodup l₁, from nodup_of_nodup_cons d, + assert d₂ : nodup (inter l₁ l₂), from nodup_inter_of_nodup _ d₁, + have nainl₁ : a ∉ l₁, from not_mem_of_nodup_cons d, + assert naini : a ∉ inter l₁ l₂, from λ i, absurd (mem_of_mem_inter_left i) nainl₁, by_cases - (λ ainl₂ : a ∈ l₂, by rewrite [intersection_cons_of_mem _ ainl₂]; exact (nodup_cons naini d₂)) - (λ nainl₂ : a ∉ l₂, by rewrite [intersection_cons_of_not_mem _ nainl₂]; exact d₂) + (λ ainl₂ : a ∈ l₂, by rewrite [inter_cons_of_mem _ ainl₂]; exact (nodup_cons naini d₂)) + (λ nainl₂ : a ∉ l₂, by rewrite [inter_cons_of_not_mem _ nainl₂]; exact d₂) -theorem intersection_eq_nil_of_disjoint : ∀ {l₁ l₂ : list A}, disjoint l₁ l₂ → intersection l₁ l₂ = [] +theorem inter_eq_nil_of_disjoint : ∀ {l₁ l₂ : list A}, disjoint l₁ l₂ → inter l₁ l₂ = [] | [] l₂ d := rfl | (a::l₁) l₂ d := - assert aux_eq : intersection l₁ l₂ = [], from intersection_eq_nil_of_disjoint (disjoint_of_disjoint_cons_left d), - assert nainl₂ : a ∉ l₂, from disjoint_left d !mem_cons, - by rewrite [intersection_cons_of_not_mem _ nainl₂, aux_eq] + assert aux_eq : inter l₁ l₂ = [], from inter_eq_nil_of_disjoint (disjoint_of_disjoint_cons_left d), + assert nainl₂ : a ∉ l₂, from disjoint_left d !mem_cons, + by rewrite [inter_cons_of_not_mem _ nainl₂, aux_eq] -theorem all_intersection_of_all_left {p : A → Prop} : ∀ {l₁} (l₂), all l₁ p → all (intersection l₁ l₂) p +theorem all_inter_of_all_left {p : A → Prop} : ∀ {l₁} (l₂), all l₁ p → all (inter l₁ l₂) p | [] l₂ h := trivial | (a::l₁) l₂ h := - have h₁ : all l₁ p, from all_of_all_cons h, - assert h₂ : all (intersection l₁ l₂) p, from all_intersection_of_all_left _ h₁, - have pa : p a, from of_all_cons h, - assert h₃ : all (a :: intersection l₁ l₂) p, from all_cons_of_all pa h₂, + have h₁ : all l₁ p, from all_of_all_cons h, + assert h₂ : all (inter l₁ l₂) p, from all_inter_of_all_left _ h₁, + have pa : p a, from of_all_cons h, + assert h₃ : all (a :: inter l₁ l₂) p, from all_cons_of_all pa h₂, by_cases - (λ ainl₂ : a ∈ l₂, by rewrite [intersection_cons_of_mem _ ainl₂]; exact h₃) - (λ nainl₂ : a ∉ l₂, by rewrite [intersection_cons_of_not_mem _ nainl₂]; exact h₂) + (λ ainl₂ : a ∈ l₂, by rewrite [inter_cons_of_mem _ ainl₂]; exact h₃) + (λ nainl₂ : a ∉ l₂, by rewrite [inter_cons_of_not_mem _ nainl₂]; exact h₂) -theorem all_intersection_of_all_right {p : A → Prop} : ∀ (l₁) {l₂}, all l₂ p → all (intersection l₁ l₂) p +theorem all_inter_of_all_right {p : A → Prop} : ∀ (l₁) {l₂}, all l₂ p → all (inter l₁ l₂) p | [] l₂ h := trivial | (a::l₁) l₂ h := - assert h₁ : all (intersection l₁ l₂) p, from all_intersection_of_all_right _ h, + assert h₁ : all (inter l₁ l₂) p, from all_inter_of_all_right _ h, by_cases (λ ainl₂ : a ∈ l₂, - have pa : p a, from of_mem_of_all ainl₂ h, - assert h₂ : all (a :: intersection l₁ l₂) p, from all_cons_of_all pa h₁, - by rewrite [intersection_cons_of_mem _ ainl₂]; exact h₂) - (λ nainl₂ : a ∉ l₂, by rewrite [intersection_cons_of_not_mem _ nainl₂]; exact h₁) + have pa : p a, from of_mem_of_all ainl₂ h, + assert h₂ : all (a :: inter l₁ l₂) p, from all_cons_of_all pa h₁, + by rewrite [inter_cons_of_mem _ ainl₂]; exact h₂) + (λ nainl₂ : a ∉ l₂, by rewrite [inter_cons_of_not_mem _ nainl₂]; exact h₁) -end intersection +end inter end list