---

Definition: eq_list
as =b bs ==
  Y 
  (λeq_list,as,bs. case as of 
                     [] => null(bs) 
                     a::as' =>
                      case bs of [] => ff | b::bs' => (a (=b) b) ∧b (eq_list as' bs') esac 
                  esac) 
  as 
  bs

Lemma: eq_list_wf
∀s:DSet. ∀as,bs:|s| List.  (as =b bs ∈ 𝔹)

Lemma: assert_of_eq_list
∀s:DSet. ∀as,bs:|s| List.  (↑(as =b bs) ⇐⇒ as = bs ∈ (|s| List))

Definition: dset_list
s List ==  mk_dset(|s| List, λx,y. (x =b y))

Lemma: dset_list_wf
∀s:DSet. (s List ∈ DSet)

Definition: mem_f
mem_f(T;a;bs) ==  Y (λmem_f,bs. case bs of [] => False | b::bs' => (b = a ∈ T) ∨ (mem_f bs') esac) bs

Lemma: mem_f_wf
∀T:Type. ∀a:T. ∀bs:T List.  (mem_f(T;a;bs) ∈ ℙ)

Lemma: list_in_mem_f_list
∀T:Type. ∀as:T List.  (as ∈ {x:T| mem_f(T;x;as)}  List)

Definition: mon_reduce
Π as ==  reduce(*;e;as)

Lemma: mon_reduce_wf
∀g:IMonoid. ∀as:|g| List.  (Π as ∈ |g|)

Lemma: comb_for_mon_reduce_wf
λg,as,z. (Π as) ∈ g:IMonoid ⟶ as:(|g| List) ⟶ (↓True) ⟶ |g|

Lemma: extend_perm_over_itcomp
∀n:ℕ. ∀ps:Sym(n) List.  (↑{n}(Π ps) = (Π map(λp.↑{n}(p);ps)) ∈ Sym(n + 1))

Lemma: sym_grp_is_swaps
∀n:ℕ. ∀p:Sym(n).  ∃abs:(ℕn × ℕn) List. (p = (Π map(λab.let a,b = ab in txpose_perm(a;b);abs)) ∈ Sym(n))

Lemma: sym_grp_is_swaps_a
∀n:{1...}. ∀p:Sym(n).
  ∃abs:{ab:ℕn × ℕn| fst(ab) < snd(ab)}  List. (p = (Π map(λab.let a,b = ab in txpose_perm(a;b);abs)) ∈ Sym(n))

Lemma: perm_induction
∀n:ℕ. ∀Q:Sym(n) ⟶ ℙ.  (Q[id_perm()] ⇒ (∀p:Sym(n). (Q[p] ⇒ (∀i,j:ℕn.  Q[txpose_perm(i;j) O p]))) ⇒ {∀p:Sym(n). Q[p]})

Lemma: perm_induction_a
∀n:ℕ. ∀Q:Sym(n) ⟶ ℙ.  (Q[id_perm()] ⇒ (∀p:Sym(n). (Q[p] ⇒ (∀i:ℕ+n. Q[txpose_perm(i;0) O p]))) ⇒ {∀p:Sym(n). Q[p]})

Lemma: perm_induction_b
∀n:ℕ. ∀Q:Sym(n) ⟶ ℙ.  (Q[id_perm()] ⇒ (∀p:Sym(n). (Q[p] ⇒ (∀i:ℕ+n. Q[p O txpose_perm(i;0)]))) ⇒ {∀p:Sym(n). Q[p]})

Lemma: mon_itop_perm_invar
∀g:IAbMonoid. ∀n:ℕ. ∀E:ℕn ⟶ |g|. ∀p:Sym(n).  ((Π 0 ≤ j < n. E[p.f j]) = (Π 0 ≤ j < n. E[j]) ∈ |g|)

Lemma: mon_reduce_append
∀g:IMonoid. ∀as,bs:|g| List.  ((Π as @ bs) = ((Π as) * (Π bs)) ∈ |g|)

Lemma: mon_reduce_eq_itop
∀g:IMonoid. ∀as:|g| List.  ((Π as) = (Π 0 ≤ i < ||as||. as[i]) ∈ |g|)

Definition: mon_for
For{g} x ∈ as. f[x] ==  For{T,*,e} x ∈ as. f[x]

Lemma: mon_for_wf
∀g:IMonoid. ∀A:Type. ∀as:A List. ∀f:A ⟶ |g|.  (For{g} x ∈ as. f[x] ∈ |g|)

Lemma: comb_for_mon_for_wf
λg,A,as,f,z. For{g} x ∈ as. f[x] ∈ g:IMonoid ⟶ A:Type ⟶ as:(A List) ⟶ f:(A ⟶ |g|) ⟶ (↓True) ⟶ |g|

Lemma: mon_for_nil_lemma
∀f,g,T:Top.  (For{g} x ∈ []. f[x] ~ e)

Lemma: mon_for_cons_lemma
∀f,as,a,g,T:Top.  (For{g} x ∈ [a / as]. f[x] ~ f[a] * (For{g} x ∈ as. f[x]))

Lemma: mon_for_eq_itop
∀g:IMonoid. ∀A:Type. ∀as:A List. ∀f:A ⟶ |g|.  ((For{g} x ∈ as. f[x]) = (Π 0 ≤ i < ||as||. f[as[i]]) ∈ |g|)

Lemma: mon_for_append
∀g:IMonoid. ∀A:Type. ∀f:A ⟶ |g|. ∀as,as':A List.
  ((For{g} x ∈ as @ as'. f[x]) = ((For{g} x ∈ as. f[x]) * (For{g} x ∈ as'. f[x])) ∈ |g|)

Lemma: select_reject_permr
∀T:Type. ∀as:T List. ∀i:ℕ||as||.  ([as[i] / as\[i]] ≡(T) as)

Lemma: mon_reduce_functionality_wrt_permr
∀g:IAbMonoid. ∀xs,ys:|g| List.  ((xs ≡(|g|) ys) ⇒ ((Π xs) = (Π ys) ∈ |g|))

Lemma: map_permr_func
∀A,B:Type. ∀f:A ⟶ B. ∀as,as':A List.  ((as ≡(A) as') ⇒ (map(f;as) ≡(B) map(f;as')))

Lemma: map_functionality
∀A,B:Type. ∀f,f':A ⟶ B. ∀as,as':A List.  ((f = f' ∈ (A ⟶ B)) ⇒ (as ≡(A) as') ⇒ (map(f;as) ≡(B) map(f';as')))

Lemma: map_functionality_2
∀A,B:Type. ∀as:A List. ∀f,f':A ⟶ B. ∀as:A List.
  ((f = f' ∈ ({x:A| mem_f(A;x;as)}  ⟶ B)) ⇒ (map(f;as) = map(f';as) ∈ (B List)))

Lemma: mon_for_functionality_wrt_permr
∀g:IAbMonoid. ∀A:Type. ∀as,as':A List. ∀f,f':A ⟶ |g|.
  ((as ≡(A) as')
  ⇒ (∀x:A. (mem_f(A;x;as) ⇒ (f[x] = f'[x] ∈ |g|)))
  ⇒ ((For{g} x ∈ as. f[x]) = (For{g} x ∈ as'. f'[x]) ∈ |g|))

Lemma: length_mon_for_char
∀A:Type. ∀as:A List.  (||as|| = (For{<ℤ+>} x ∈ as. 1) ∈ ℤ)

Lemma: length_functionality_wrt_permr
∀A:Type. ∀as,as':A List.  ((as ≡(A) as') ⇒ (||as|| = ||as'|| ∈ ℤ))

Definition: mon_htfor
HTFor{g} h::t ∈ as. f[h; t] ==  ForHdTl{A,*,e} h::t ∈ as. f[h; t]

Lemma: mon_htfor_wf
∀g:IMonoid. ∀A:Type. ∀as:A List. ∀f:A ⟶ (A List) ⟶ |g|.  (HTFor{g} h::t ∈ as. f[h;t] ∈ |g|)

Lemma: mon_htfor_nil_lemma
∀f,g,T:Top.  (HTFor{g} h::t ∈ []. f[h;t] ~ e)

Lemma: mon_htfor_cons_lemma
∀f,as,a,g,T:Top.  (HTFor{g} h::t ∈ [a / as]. f[h;t] ~ f[a;as] * (HTFor{g} h::t ∈ as. f[h;t]))

Lemma: mon_for_map
∀g:IAbMonoid. ∀A,B:Type. ∀e:A ⟶ B. ∀f:B ⟶ |g|. ∀as:A List.
  ((For{g} y ∈ map(e;as). f[y]) = (For{g} x ∈ as. f[e x]) ∈ |g|)

Lemma: mon_for_of_id
∀g:IAbMonoid. ∀A:Type. ∀as:A List.  ((For{g} x ∈ as. e) = e ∈ |g|)

Lemma: mon_for_of_op
∀g:IAbMonoid. ∀A:Type. ∀e,f:A ⟶ |g|. ∀as:A List.
  ((For{g} x ∈ as. (e[x] * f[x])) = ((For{g} x ∈ as. e[x]) * (For{g} x ∈ as. f[x])) ∈ |g|)

Lemma: mon_for_swap
∀g:IAbMonoid. ∀A,B:Type. ∀f:A ⟶ B ⟶ |g|. ∀as:A List. ∀bs:B List.
  ((For{g} x ∈ as. For{g} y ∈ bs. f[x;y]) = (For{g} y ∈ bs. For{g} x ∈ as. f[x;y]) ∈ |g|)

Lemma: mon_for_when_swap
∀g:Mon. ∀A:Type. ∀as:A List. ∀b:𝔹. ∀f:A ⟶ |g|.
  ((For{g} x ∈ as. (when b. f[x])) = (when b. (For{g} x ∈ as. f[x])) ∈ |g|)

Definition: mem
a ∈b as ==  ∃b x(:|s|) ∈ as. x (=b) a

Lemma: mem_wf
∀s:DSet. ∀a:|s|. ∀bs:|s| List.  (a ∈b bs ∈ 𝔹)

Lemma: mem_nil_lemma
∀a,s:Top.  (a ∈b [] ~ ff)

Lemma: mem_cons_lemma
∀bs,b,a,s:Top.  (a ∈b [b / bs] ~ (b (=b) a) ∨b(a ∈b bs))

Lemma: comb_for_mem_wf
λs,a,bs,z. (a ∈b bs) ∈ s:DSet ⟶ a:|s| ⟶ bs:(|s| List) ⟶ (↓True) ⟶ 𝔹

Lemma: mon_for_when_none
∀s:DSet. ∀g:IMonoid. ∀f:|s| ⟶ |g|. ∀b:|s| ⟶ 𝔹. ∀as:|s| List.
  ((∀x:|s|. ((↑(x ∈b as)) ⇒ (¬↑b[x]))) ⇒ ((For{g} x ∈ as. (when b[x]. f[x])) = e ∈ |g|))

Definition: ball
∀bx(:A) ∈ as. f[x] ==  For{<𝔹,∧b>} x ∈ as. f[x]

Lemma: ball_wf
∀A:Type. ∀as:A List. ∀f:A ⟶ 𝔹.  (∀bx(:A) ∈ as. f[x] ∈ 𝔹)

Lemma: ball_nil_lemma
∀f,T:Top.  (∀bx(:T) ∈ []. f[x] ~ tt)

Lemma: ball_cons_lemma
∀f,as,a,T:Top.  (∀bx(:T) ∈ [a / as]. f[x] ~ f[a] ∧b (∀bx(:T) ∈ as. f[x]))

Lemma: comb_for_ball_wf
λA,as,f,z. ∀bx(:A) ∈ as. f[x] ∈ A:Type ⟶ as:(A List) ⟶ f:(A ⟶ 𝔹) ⟶ (↓True) ⟶ 𝔹

Lemma: ball_char
∀s:DSet. ∀as:|s| List. ∀f:|s| ⟶ 𝔹.  (↑(∀bx(:|s|) ∈ as. f[x]) ⇐⇒ ∀x:|s|. ((↑(x ∈b as)) ⇒ (↑f[x])))

Definition: distinct
distinct{s}(ps) ==  HTFor{<𝔹,∧b>} q::qs ∈ ps. ∀br(:|s|) ∈ qs. (¬b(r (=b) q))

Lemma: distinct_wf
∀s:DSet. ∀ps:|s| List.  (distinct{s}(ps) ∈ 𝔹)

Lemma: distinct_nil_lemma
∀s:Top. (distinct{s}([]) ~ tt)

Lemma: distinct_cons_lemma
∀as,a,s:Top.  (distinct{s}([a / as]) ~ (∀br(:|s|) ∈ as. (¬b(r (=b) a))) ∧b distinct{s}(as))

Lemma: mon_for_when_unique
∀s:DSet. ∀g:IMonoid. ∀f:|s| ⟶ |g|. ∀b:|s| ⟶ 𝔹. ∀u:|s|.
  ((↑b[u])
  ⇒ (∀as:|s| List
        ((↑distinct{s}(as))
        ⇒ (↑(u ∈b as))
        ⇒ (∀v:|s|. ((↑b[v]) ⇒ (↑(v ∈b as)) ⇒ (v = u ∈ |s|)))
        ⇒ ((For{g} x ∈ as. (when b[x]. f[x])) = f[u] ∈ |g|))))

Definition: lapp_imon
<T List,@> ==  <T List, λx,y. tt, λx,y. tt, λx,y. (x @ y), [], λx.x>

Lemma: lapp_imon_wf
∀T:Type. (<T List,@> ∈ IMonoid)

Definition: lapp_mon
<s List, @> ==  <|s| List, λx,y. (x =b y), λx,y. tt, λx,y. (x @ y), [], λx.x>

Lemma: lapp_mon_wf
∀s:DSet. (<s List, @> ∈ Mon)

Lemma: lapp_fact
∀s:DSet. ∀as:|s| List.  (as = (For{<s List, @>} x ∈ as. [x]) ∈ (|s| List))

Lemma: lapp_fact_a
∀T:Type. ∀as:T List.  (as = (For{<T List,@>} x ∈ as. [x]) ∈ (T List))

Lemma: lapp_fact_b
∀T:Type. ∀as:T List.  (as = (Π 0 ≤ i < ||as||. [as[i]]) ∈ (T List))

Lemma: dist_hom_over_mon_for
∀T:Type. ∀m,n:IMonoid. ∀f:MonHom(m,n). ∀a:T List. ∀g:T ⟶ |m|.
  ((f (For{m} x ∈ a. g[x])) = (For{n} x ∈ a. (f g[x])) ∈ |n|)

Definition: bexists
∃bx(:A) ∈ as. f[x] ==  ∃b x(:A) ∈ as. f[x]

Lemma: bexists_wf
∀A:Type. ∀as:A List. ∀f:A ⟶ 𝔹.  (∃bx(:A) ∈ as. f[x] ∈ 𝔹)

Lemma: bexists_nil_lemma
∀f,T:Top.  (∃bx(:T) ∈ []. f[x] ~ ff)

Lemma: bexists_cons_lemma
∀f,as,a,T:Top.  (∃bx(:T) ∈ [a / as]. f[x] ~ f[a] ∨b(∃bx(:T) ∈ as. f[x]))

Lemma: ball_functionality_wrt_permr
∀T:Type. ∀as,bs:T List. ∀P,Q:T ⟶ 𝔹.  ((as ≡(T) bs) ⇒ (∀x:T. P[x] = Q[x]) ⇒ ∀bx(:T) ∈ as. P[x] = ∀bx(:T) ∈ bs. Q[x])

Lemma: bexists_iff_exists_nth
∀s:DSet. ∀f:|s| ⟶ 𝔹. ∀as:|s| List.  (↑∃b x(:|s|) ∈ as. f[x] ⇐⇒ ∃n:ℕ||as||. (↑f[as[n]]))

Lemma: bnot_thru_exists
∀A:Type. ∀as:A List. ∀f:A ⟶ 𝔹.  ¬b(∃bx(:A) ∈ as. f[x]) = ∀bx(:A) ∈ as. (¬bf[x])

Lemma: mem_iff_mem_f
∀s:DSet. ∀a:|s|. ∀bs:|s| List.  (↑(a ∈b bs) ⇐⇒ mem_f(|s|;a;bs))

Lemma: mem_functionality_wrt_permr
∀s:DSet. ∀a,b:|s|. ∀as,bs:|s| List.  ((a = b ∈ |s|) ⇒ (as ≡(|s|) bs) ⇒ a ∈b as = b ∈b bs)

Lemma: bexists_char
∀s:DSet. ∀as:|s| List. ∀f:|s| ⟶ 𝔹.  (↑(∃bx(:|s|) ∈ as. f[x]) ⇐⇒ ∃x:|s|. ((↑(x ∈b as)) ∧ (↑f[x])))

Lemma: mem_iff_exists
∀s:DSet. ∀a:|s|. ∀bs:|s| List.  (↑(a ∈b bs) ⇐⇒ ∃n:ℕ||bs||. (bs[n] = a ∈ |s|))

Lemma: cons_permr_mem
∀s:DSet. ∀a:|s|. ∀as,bs:|s| List.  (([a / as] ≡(|s|) bs) ⇒ (↑(a ∈b bs)))

Definition: remove1
as \ a ==  Y (λremove1,as. case as of [] => [] | a'::as' => if a' (=b) a then as' else [a' / (remove1 as')] fi  esac) as

Lemma: remove1_wf
∀s:DSet. ∀a:|s|. ∀bs:|s| List.  (bs \ a ∈ |s| List)

Lemma: comb_for_remove1_wf
λs,a,bs,z. (bs \ a) ∈ s:DSet ⟶ a:|s| ⟶ bs:(|s| List) ⟶ (↓True) ⟶ (|s| List)

Lemma: remove1_nil_lemma
∀a,s:Top.  ([] \ a ~ [])

Lemma: remove1_cons_lemma
∀bs,b,a,s:Top.  ([b / bs] \ a ~ if b (=b) a then bs else [b / (bs \ a)] fi )

Lemma: cons_remove1_permr
∀s:DSet. ∀a:|s|. ∀bs:|s| List.  ((↑(a ∈b bs)) ⇒ ([a / (bs \ a)] ≡(|s|) bs))

Lemma: not_mem_remove1
∀s:DSet. ∀a:|s|. ∀bs:|s| List.  ((¬↑(a ∈b bs)) ⇒ ((bs \ a) = bs ∈ (|s| List)))

Lemma: remove1_functionality_wrt_permr
∀s:DSet. ∀a,a':|s|. ∀bs,bs':|s| List.  ((a = a' ∈ |s|) ⇒ (bs ≡(|s|) bs') ⇒ ((bs \ a) ≡(|s|) (bs' \ a')))

Definition: bpermr
as ≡b bs ==  Y (λbpermr,as,bs. case as of [] => null(bs) | a::as' => (a ∈b bs) ∧b (bpermr as' (bs \ a)) esac) as bs

Lemma: bpermr_wf
∀s:DSet. ∀as,bs:|s| List.  (as ≡b bs ∈ 𝔹)

Lemma: assert_of_bpermr
∀s:DSet. ∀as,bs:|s| List.  (↑(as ≡b bs) ⇐⇒ as ≡(|s|) bs)

Lemma: null_functionality_wrt_permr
∀T:Type. ∀as,bs:T List.  ((as ≡(T) bs) ⇒ null(as) = null(bs))

Definition: count
a #∈ as ==  For{<ℤ+>} x ∈ as. b2i(x (=b) a)

Lemma: count_wf
∀s:DSet. ∀a:|s|. ∀bs:|s| List.  (a #∈ bs ∈ ℤ)

Lemma: count_nil_lemma
∀a,s:Top.  (a #∈ [] ~ 0)

Lemma: count_cons_lemma
∀bs,b,a,s:Top.  (a #∈ [b / bs] ~ b2i(b (=b) a) + (a #∈ bs))

Lemma: comb_for_count_wf
λs,a,bs,z. (a #∈ bs) ∈ s:DSet ⟶ a:|s| ⟶ bs:(|s| List) ⟶ (↓True) ⟶ ℤ

Lemma: count_functionality
∀s:DSet. ∀a,a':|s|. ∀bs,bs':|s| List.  ((a = a' ∈ |s|) ⇒ (bs ≡(|s|) bs') ⇒ ((a #∈ bs) = (a' #∈ bs') ∈ ℤ))

Lemma: count_bounds
∀s:DSet. ∀a:|s|. ∀bs:|s| List.  ((0 ≤ (a #∈ bs)) ∧ ((a #∈ bs) ≤ ||bs||))

Lemma: mem_iff_count_nzero
∀s:DSet. ∀a:|s|. ∀bs:|s| List.  (↑(a ∈b bs) ⇐⇒ (a #∈ bs) > 0)

Lemma: permr_iff_eq_counts
∀s:DSet. ∀as,bs:|s| List.  (as ≡(|s|) bs ⇐⇒ ∀x:|s|. ((x #∈ as) = (x #∈ bs) ∈ ℤ))

Lemma: permr_iff_eq_counts_a
∀s:DSet. ∀as,bs:|s| List.  (as ≡(|s|) bs ⇐⇒ {∀x:|s|. ((x #∈ as) = (x #∈ bs) ∈ ℤ)})

Definition: dislist
DisList{s} ==  {as:|s| List| ∀x:|s|. ((x #∈ as) ≤ 1)} 

Lemma: dislist_wf
∀s:DSet. (DisList{s} ∈ Type)

Lemma: dislist_properties
∀s:DSet. ∀as:DisList{s}.  {∀x:|s|. ((x #∈ as) ≤ 1)}

Definition: diff
as - bs ==  Y (λdiff,as,bs. case bs of [] => as | b::bs' => diff (as \ b) bs' esac) as bs

Lemma: diff_wf
∀s:DSet. ∀as,bs:|s| List.  (as - bs ∈ |s| List)

Lemma: diff_nil_lemma
∀as,s:Top.  (as - [] ~ as)

Lemma: diff_cons_lemma
∀bs,b,as,s:Top.  (as - [b / bs] ~ (as \ b) - bs)

Lemma: count_append
∀s:DSet. ∀as,bs:|s| List. ∀c:|s|.  ((c #∈ (as @ bs)) = ((c #∈ as) + (c #∈ bs)) ∈ ℤ)

Lemma: mem_append
∀s:DSet. ∀as,bs:|s| List. ∀c:|s|.  c ∈b (as @ bs) = (c ∈b as) ∨b(c ∈b bs)

Lemma: mem_map
∀s,s':DSet. ∀f:|s| ⟶ |s'|. ∀x:|s|. ∀as:|s| List.  ((↑(x ∈b as)) ⇒ (↑((f x) ∈b map(f;as))))

Lemma: count_remove1
∀s:DSet. ∀as:|s| List. ∀b,c:|s|.  ((c #∈ (as \ b)) = ((c #∈ as) -- b2i(b (=b) c)) ∈ ℤ)

Lemma: count_diff
∀s:DSet. ∀as,bs:|s| List. ∀c:|s|.  ((c #∈ (as - bs)) = ((c #∈ as) -- (c #∈ bs)) ∈ ℤ)

Lemma: mem_diff
∀s:DSet. ∀as:DisList{s}. ∀bs:|s| List. ∀c:|s|.  c ∈b (as - bs) = (c ∈b as) ∧b (¬b(c ∈b bs))

Lemma: diff_functionality_wrt_permr
∀s:DSet. ∀as,as',bs,bs':|s| List.  ((as ≡(|s|) as') ⇒ (bs ≡(|s|) bs') ⇒ ((as - bs) ≡(|s|) (as' - bs')))

Definition: lmin
lmin(s;as;bs) ==  as - (as - bs)

Lemma: lmin_wf
∀s:DSet. ∀as,bs:|s| List.  (lmin(s;as;bs) ∈ |s| List)

Lemma: count_lmin
∀s:DSet. ∀as,bs:|s| List. ∀c:|s|.  ((c #∈ lmin(s;as;bs)) = imin(c #∈ as;c #∈ bs) ∈ ℤ)

Lemma: mem_lmin
∀s:DSet. ∀as,bs:|s| List. ∀c:|s|.  c ∈b lmin(s;as;bs) = (c ∈b as) ∧b (c ∈b bs)

Lemma: lmin_functionality_wrt_permr
∀s:DSet. ∀as,as',bs,bs':|s| List.  ((as ≡(|s|) as') ⇒ (bs ≡(|s|) bs') ⇒ (lmin(s;as;bs) ≡(|s|) lmin(s;as';bs')))

Lemma: lmin_com
∀s:DSet. ∀as,bs:|s| List.  (lmin(s;as;bs) ≡(|s|) lmin(s;bs;as))

Lemma: lmin_assoc
∀s:DSet. ∀as,bs,cs:|s| List.  (lmin(s;as;lmin(s;bs;cs)) ≡(|s|) lmin(s;lmin(s;as;bs);cs))

Definition: lmax
lmax(s;as;bs) ==  (as - bs) @ bs

Lemma: lmax_wf
∀s:DSet. ∀as,bs:|s| List.  (lmax(s;as;bs) ∈ |s| List)

Lemma: count_lmax
∀s:DSet. ∀as,bs:|s| List. ∀c:|s|.  ((c #∈ lmax(s;as;bs)) = imax(c #∈ as;c #∈ bs) ∈ ℤ)

Lemma: mem_lmax
∀s:DSet. ∀as,bs:|s| List. ∀c:|s|.  c ∈b lmax(s;as;bs) = (c ∈b as) ∨b(c ∈b bs)

Lemma: lmax_functionality_wrt_permr
∀s:DSet. ∀as,as',bs,bs':|s| List.  ((as ≡(|s|) as') ⇒ (bs ≡(|s|) bs') ⇒ (lmax(s;as;bs) ≡(|s|) lmax(s;as';bs')))

Lemma: lmax_com
∀s:DSet. ∀as,bs:|s| List.  (lmax(s;as;bs) ≡(|s|) lmax(s;bs;as))

Lemma: lmax_assoc
∀s:DSet. ∀as,bs,cs:|s| List.  (lmax(s;as;lmax(s;bs;cs)) ≡(|s|) lmax(s;lmax(s;as;bs);cs))

Definition: bsublist
bsublist(s;as;bs) ==  null(as - bs)

Lemma: bsublist_wf
∀s:DSet. ∀as,bs:|s| List.  (bsublist(s;as;bs) ∈ 𝔹)

Definition: bsuplist
bsuplist(s;as;bs) ==  bsublist(s;bs;as)

Lemma: bsuplist_wf
∀s:DSet. ∀as,bs:|s| List.  (bsuplist(s;as;bs) ∈ 𝔹)

Lemma: count_bsublist
∀s:DSet. ∀as,bs:|s| List.  (↑bsublist(s;as;bs) ⇐⇒ {∀c:|s|. ((c #∈ as) ≤ (c #∈ bs))})

Lemma: count_bsublist_a
∀s:DSet. ∀as,bs:|s| List.  (↑bsublist(s;as;bs) ⇐⇒ ∀c:|s|. ((c #∈ as) ≤ (c #∈ bs)))

Lemma: mem_bsublist_imp
∀s:DSet. ∀as,bs:|s| List.  ((↑bsublist(s;as;bs)) ⇒ (∀c:|s|. ((↑(c ∈b as)) ⇒ (↑(c ∈b bs)))))

Lemma: mem_bsublist
∀s:DSet. ∀as:DisList{s}. ∀bs:|s| List.  (↑bsublist(s;as;bs) ⇐⇒ ∀c:|s|. ((↑(c ∈b as)) ⇒ (↑(c ∈b bs))))

Lemma: bsublist_weakening
∀s:DSet. ∀as,bs:|s| List.  ((as ≡(|s|) bs) ⇒ (↑bsublist(s;as;bs)))

Lemma: bsublist_transitivity
∀s:DSet. ∀us,vs,ws:|s| List.  ((↑bsublist(s;us;vs)) ⇒ (↑bsublist(s;vs;ws)) ⇒ (↑bsublist(s;us;ws)))

Lemma: bsublist_functionality_wrt_permr
∀s:DSet. ∀as,bs,as',bs':|s| List.  ((as ≡(|s|) bs) ⇒ (as' ≡(|s|) bs') ⇒ bsublist(s;as;as') = bsublist(s;bs;bs'))

Lemma: bsublist_functionality_wrt_bsublist
∀s:DSet. ∀as,as',bs,bs':|s| List.
  ((↑bsuplist(s;as;bs)) ⇒ (↑bsublist(s;as';bs')) ⇒ (↑(bsublist(s;as;as') ⇒b bsublist(s;bs;bs'))))

Lemma: bsublist_append_diff
∀s:DSet. ∀as,bs:|s| List.  ((↑bsublist(s;as;bs)) ⇒ (∃cs:|s| List. ((cs @ as) ≡(|s|) bs)))

Lemma: ball_respects_bsublist
∀s:DSet. ∀us,vs:|s| List.
  ((↑bsublist(s;us;vs)) ⇒ (∀Q:|s| ⟶ 𝔹. ((↑(For{<𝔹,∧b>} x ∈ vs. Q[x])) ⇒ (↑(For{<𝔹,∧b>} x ∈ us. Q[x])))))

Lemma: ball_functionality_wrt_bimplies
∀T:Type. ∀as:T List. ∀P,Q:T ⟶ 𝔹.  ((∀x:T. (↑(P[x] ⇒b Q[x]))) ⇒ (↑(∀bx(:T) ∈ as. P[x] ⇒b (∀bx(:T) ∈ as. Q[x]))))

Lemma: distinct_iff_counts_le_one
∀s:DSet. ∀ps:|s| List.  (↑distinct{s}(ps) ⇐⇒ ∀x:|s|. ((x #∈ ps) ≤ 1))

Lemma: firstn_factor
∀T:Type. ∀as:T List. ∀n:{0...||as||}.  (firstn(n;as) = (Π 0 ≤ i < n. [as[i]]) ∈ (T List))

Lemma: nth_tl_factor
∀T:Type. ∀n:ℕ. ∀as:T List.  ((n ≤ ||as||) ⇒ (nth_tl(n;as) = (Π n ≤ i < ||as||. [as[i]]) ∈ (T List)))

Lemma: segment_factor
∀T:Type. ∀as:T List. ∀i:{0...||as||}. ∀j:{i...||as||}.  ((as[i..j-]) = (Π i ≤ k < j. [as[k]]) ∈ (T List))

Lemma: append_segment
∀T:Type. ∀as:T List. ∀i:{0...||as||}. ∀j:{i...||as||}. ∀k:{j...||as||}.
  (((as[i..j-]) @ (as[j..k-])) = (as[i..k-]) ∈ (T List))

Definition: fin_type
{as} ==  {a:|s|| ↑(a ∈b as)} 

Lemma: fin_type_wf
∀s:DSet. ∀as:|s| List.  ({as} ∈ Type)

Lemma: fin_type_properties
∀s:DSet. ∀as:|s| List. ∀a:{as}.  (↑(a ∈b as))

Lemma: fin_type_inc
∀s:DSet. ∀as,bs:|s| List.  ((↑bsublist(s;as;bs)) ⇒ ({as} ⊆r {bs}))

Lemma: whole_segment_example
∀T:Type. ∀as:T List.  ((as[0..||as||-]) = as ∈ (T List))



Home Index