---

Definition: perm_sig
perm_sig(T) ==  f:T ⟶ T × (T ⟶ T)

Lemma: perm_sig_wf
∀T:Type. (perm_sig(T) ∈ Type)

Definition: perm_f
p.f ==  fst(p)

Lemma: perm_f_wf
∀T:Type. ∀p:perm_sig(T).  (p.f ∈ T ⟶ T)

Definition: perm_b
p.b ==  snd(p)

Lemma: perm_b_wf
∀T:Type. ∀p:perm_sig(T).  (p.b ∈ T ⟶ T)

Lemma: comb_for_perm_sig_wf
λT,z. perm_sig(T) ∈ T:Type ⟶ (↓True) ⟶ Type

Definition: perm
Perm(T) ==  {p:perm_sig(T)| InvFuns(T;T;p.f;p.b)} 

Lemma: perm_wf
∀T:Type. (Perm(T) ∈ Type)

Lemma: comb_for_perm_wf
λT,z. Perm(T) ∈ T:Type ⟶ (↓True) ⟶ Type

Lemma: perm_properties
∀T:Type. ∀p:Perm(T).  InvFuns(T;T;p.f;p.b)

Definition: mk_perm
mk_perm(f;b) ==  <f, b>

Lemma: mk_perm_wf
∀T:Type. ∀f,b:T ⟶ T.  (mk_perm(f;b) ∈ perm_sig(T))

Lemma: comb_for_mk_perm_wf
λT,f,b,z. mk_perm(f;b) ∈ T:Type ⟶ f:(T ⟶ T) ⟶ b:(T ⟶ T) ⟶ (↓True) ⟶ perm_sig(T)

Lemma: mk_perm_wf_a
∀T:Type. ∀f,b:T ⟶ T.  (InvFuns(T;T;f;b) ⇒ (mk_perm(f;b) ∈ Perm(T)))

Lemma: comb_for_mk_perm_wf_a
λT,f,b,z. mk_perm(f;b) ∈ T:Type ⟶ f:(T ⟶ T) ⟶ b:(T ⟶ T) ⟶ (↓InvFuns(T;T;f;b)) ⟶ Perm(T)

Lemma: mk_perm_eta_rw
∀T:Type. ∀p:Perm(T).  (mk_perm(p.f;p.b) = p ∈ Perm(T))

Definition: id_perm
id_perm() ==  mk_perm(Id;Id)

Lemma: id_perm_wf
∀T:Type. (id_perm() ∈ Perm(T))

Definition: inv_perm
inv_perm(p) ==  mk_perm(p.b;p.f)

Lemma: inv_perm_wf
∀T:Type. ∀p:Perm(T).  (inv_perm(p) ∈ Perm(T))

Definition: comp_perm
p O q ==  mk_perm(p.f o q.f;q.b o p.b)

Lemma: comp_perm_wf
∀T:Type. ∀p,q:Perm(T).  (p O q ∈ Perm(T))

Lemma: comb_for_comp_perm_wf
λT,p,q,z. p O q ∈ T:Type ⟶ p:Perm(T) ⟶ q:Perm(T) ⟶ (↓True) ⟶ Perm(T)

Lemma: perm_assoc
∀[T:Type]. ∀[p,q,r:Perm(T)].  (p O q O r = p O q O r ∈ Perm(T))

Lemma: perm_ident
∀[T:Type]. ∀[p:Perm(T)].  ((p O id_perm() = p ∈ Perm(T)) ∧ (id_perm() O p = p ∈ Perm(T)))

Lemma: perm_inverse
∀[T:Type]. ∀[p:Perm(T)].  ((p O inv_perm(p) = id_perm() ∈ Perm(T)) ∧ (inv_perm(p) O p = id_perm() ∈ Perm(T)))

Definition: perm_igrp
perm_igrp(T) ==  mk_igrp(Perm(T);λp,q. p O q;id_perm();λp.inv_perm(p))

Lemma: perm_igrp_wf
∀[T:Type]. (perm_igrp(T) ∈ IGroup)

Lemma: comb_for_perm_igrp_wf
λT,z. perm_igrp(T) ∈ T:Type ⟶ (↓True) ⟶ IGroup

Lemma: perm_grp_inv_assoc
∀[T:Type]. ∀[a,b:Perm(T)].  ((a O inv_perm(a) O b = b ∈ Perm(T)) ∧ (inv_perm(a) O a O b = b ∈ Perm(T)))

Lemma: perm_grp_inv_id
∀T:Type. (inv_perm(id_perm()) = id_perm() ∈ Perm(T))

Lemma: perm_grp_inv_inv
∀[T:Type]. ∀[a:Perm(T)].  (inv_perm(inv_perm(a)) = a ∈ Perm(T))

Lemma: perm_grp_inv_thru_op
∀[T:Type]. ∀[a,b:Perm(T)].  (inv_perm(a O b) = inv_perm(b) O inv_perm(a) ∈ Perm(T))

Lemma: perm_grp_inverse
∀[T:Type]. ∀[a:Perm(T)].  ((a O inv_perm(a) = id_perm() ∈ Perm(T)) ∧ (inv_perm(a) O a = id_perm() ∈ Perm(T)))

Lemma: perm_mon_ident
∀[T:Type]. ∀[a:Perm(T)].  ((a O id_perm() = a ∈ Perm(T)) ∧ (id_perm() O a = a ∈ Perm(T)))

Lemma: perm_mon_assoc
∀[T:Type]. ∀[a,b,c:Perm(T)].  (a O b O c = a O b O c ∈ Perm(T))

Definition: sym_grp
Sym(n) ==  Perm(ℕn)

Definition: swap
swap(i;j) ==  λn.if (n =z i) then j if (n =z j) then i else n fi 

Lemma: swap_wf
∀n:ℕ. ∀i,j:ℕn.  (swap(i;j) ∈ ℕn ⟶ ℕn)

Definition: tswap
swap{n}(i;j) ==  swap(i;j)

Lemma: tswap_wf
∀n:ℕ. ∀i,j:ℕn.  (swap{n}(i;j) ∈ ℕn ⟶ ℕn)

Lemma: swap_order_2
∀n:ℕ. ∀i,j:ℕn.  ((swap(i;j) o swap(i;j)) = Id ∈ (ℕn ⟶ ℕn))

Lemma: swap_sym
∀n:ℕ. ∀i,j:ℕn.  (swap(i;j) = swap(j;i) ∈ (ℕn ⟶ ℕn))

Lemma: swap_id
∀n:ℕ. ∀i,j:ℕn.  ((i = j ∈ ℤ) ⇒ (swap(i;j) = Id ∈ (ℕn ⟶ ℕn)))

Lemma: swap_eval_1
∀i,j,k:ℤ.  ((k = i ∈ ℤ) ⇒ ((swap(i;j) k) = j ∈ ℤ))

Lemma: swap_eval_2
∀i,j,k:ℤ.  ((k = j ∈ ℤ) ⇒ ((swap(i;j) k) = i ∈ ℤ))

Lemma: swap_eval_3
∀i,j,k:ℤ.  ((¬(k = i ∈ ℤ)) ⇒ (¬(k = j ∈ ℤ)) ⇒ ((swap(i;j) k) = k ∈ ℤ))

Lemma: tswap_eval_1
∀n:ℕ. ∀i,j,k:ℕn.  ((k = i ∈ ℕn) ⇒ ((swap{n}(i;j) k) = j ∈ ℕn))

Lemma: tswap_eval_2
∀n:ℕ. ∀i,j,k:ℕn.  ((k = j ∈ ℕn) ⇒ ((swap{n}(i;j) k) = i ∈ ℕn))

Lemma: tswap_eval_3
∀n:ℕ. ∀i,j,k:ℕn.  ((¬(k = i ∈ ℕn)) ⇒ (¬(k = j ∈ ℕn)) ⇒ ((swap{n}(i;j) k) = k ∈ ℕn))

Lemma: triple_swap
∀n:ℕ. ∀i,j,k:ℕn.  ((¬(i = j ∈ ℤ)) ⇒ (¬(j = k ∈ ℤ)) ⇒ (swap(i;j) = (swap(i;k) o (swap(j;k) o swap(i;k))) ∈ (ℕn ⟶ ℕn)))

Definition: txpose_perm
txpose_perm(i;j) ==  mk_perm(swap(i;j);swap(i;j))

Lemma: txpose_perm_wf
∀n:ℕ. ∀i,j:ℕn.  (txpose_perm(i;j) ∈ Sym(n))

Lemma: comb_for_txpose_perm_wf
λn,i,j,z. txpose_perm(i;j) ∈ n:ℕ ⟶ i:ℕn ⟶ j:ℕn ⟶ (↓True) ⟶ Sym(n)

Lemma: txpose_perm_inv
∀n:ℕ. ∀i,j:ℕn.  (inv_perm(txpose_perm(i;j)) = txpose_perm(i;j) ∈ Sym(n))

Lemma: txpose_perm_order_2
∀n:ℕ. ∀i,j:ℕn.  (txpose_perm(i;j) O txpose_perm(i;j) = id_perm() ∈ Sym(n))

Lemma: txpose_perm_sym
∀n:ℕ. ∀i,j:ℕn.  (txpose_perm(i;j) = txpose_perm(j;i) ∈ Sym(n))

Lemma: txpose_perm_id
∀n:ℕ. ∀i,j:ℕn.  ((i = j ∈ ℤ) ⇒ (txpose_perm(i;j) = id_perm() ∈ Sym(n)))

Lemma: triple_txpose_perm
∀n:ℕ. ∀i,j,k:ℕn.
  ((¬(i = j ∈ ℤ))
  ⇒ (¬(j = k ∈ ℤ))
  ⇒ (txpose_perm(i;j) = txpose_perm(i;k) O txpose_perm(j;k) O txpose_perm(i;k) ∈ Sym(n)))

Definition: rev_permf
rev_permf(n) ==  λi.(n - 1 - i)

Lemma: rev_permf_wf
∀n:ℕ. (rev_permf(n) ∈ ℕn ⟶ ℕn)

Lemma: rev_permf_order_2
∀n:ℕ. ((rev_permf(n) o rev_permf(n)) = Id ∈ (ℕn ⟶ ℕn))

Definition: rev_perm
↔p{n} ==  mk_perm(rev_permf(n);rev_permf(n))

Lemma: rev_perm_wf
∀n:ℕ. (↔p{n} ∈ Sym(n))

Definition: app_permf
app_permf(m;n;p;q) ==  λi.if i <z m then p i else (q (i - m)) + m fi 

Lemma: app_permf_wf
∀m,n:ℕ. ∀p:ℕm ⟶ ℕm. ∀q:ℕn ⟶ ℕn.  (app_permf(m;n;p;q) ∈ ℕm + n ⟶ ℕm + n)

Lemma: comb_for_app_permf_wf
λm,n,p,q,z. app_permf(m;n;p;q) ∈ m:ℕ ⟶ n:ℕ ⟶ p:(ℕm ⟶ ℕm) ⟶ q:(ℕn ⟶ ℕn) ⟶ (↓True) ⟶ ℕm + n ⟶ ℕm + n

Lemma: app_permf_id
∀m,n:ℕ.  (app_permf(m;n;Id{ℕm};Id{ℕn}) = Id{ℕm + n} ∈ (ℕm + n ⟶ ℕm + n))

Lemma: app_permf_comp
∀m,n:ℕ. ∀p,p':ℕm ⟶ ℕm. ∀q,q':ℕn ⟶ ℕn.
  ((app_permf(m;n;p;q) o app_permf(m;n;p';q')) = app_permf(m;n;p o p';q o q') ∈ (ℕm + n ⟶ ℕm + n))

Definition: app_perm
app_perm(m;n;p;q) ==  mk_perm(app_permf(m;n;p.f;q.f);app_permf(m;n;p.b;q.b))

Lemma: app_perm_wf
∀m,n:ℕ. ∀p:Sym(m). ∀q:Sym(n).  (app_perm(m;n;p;q) ∈ Sym(m + n))

Definition: conj_perm
conj{p}(q) ==  p O q O inv_perm(p)

Lemma: conj_perm_wf
∀n:ℕ. ∀p,q:Sym(n).  (conj{p}(q) ∈ Sym(n))

Definition: extend_permf
extend_permf(pf;n) ==  λi.if (i =z n) then i else pf i fi 

Lemma: extend_permf_wf
∀n:ℕ. ∀p:ℕn ⟶ ℕn.  (extend_permf(p;n) ∈ ℕn + 1 ⟶ ℕn + 1)

Lemma: comb_for_extend_permf_wf
λn,p,z. extend_permf(p;n) ∈ n:ℕ ⟶ p:(ℕn ⟶ ℕn) ⟶ (↓True) ⟶ ℕn + 1 ⟶ ℕn + 1

Lemma: extend_permf_over_id
∀n:ℕ. (extend_permf(Id;n) = Id ∈ (ℕn + 1 ⟶ ℕn + 1))

Lemma: extend_permf_over_comp
∀n:ℕ. ∀f,g:ℕn ⟶ ℕn.  (extend_permf(g o f;n) = (extend_permf(g;n) o extend_permf(f;n)) ∈ (ℕn + 1 ⟶ ℕn + 1))

Lemma: extend_permf_over_swap
∀n:ℕ. ∀i,j:ℕn.  (extend_permf(swap(i;j);n) = swap(i;j) ∈ (ℕn + 1 ⟶ ℕn + 1))

Definition: extend_perm
↑{n}(p) ==  mk_perm(extend_permf(p.f;n);extend_permf(p.b;n))

Lemma: extend_perm_wf
∀n:ℕ. ∀p:Sym(n).  (↑{n}(p) ∈ Sym(n + 1))

Lemma: comb_for_extend_perm_wf
λn,p,z. ↑{n}(p) ∈ n:ℕ ⟶ p:Sym(n) ⟶ (↓True) ⟶ Sym(n + 1)

Lemma: extend_perm_over_id
∀n:ℕ. (↑{n}(id_perm()) = id_perm() ∈ Sym(n + 1))

Lemma: extend_perm_over_comp
∀n:ℕ. ∀p,q:Sym(n).  (↑{n}(p O q) = ↑{n}(p) O ↑{n}(q) ∈ Sym(n + 1))

Lemma: extend_perm_over_txpose
∀n:ℕ. ∀i,j:ℕn.  (↑{n}(txpose_perm(i;j)) = txpose_perm(i;j) ∈ Sym(n + 1))

Definition: restrict_perm
restrict_perm(p;n) ==  p

Lemma: restrict_perm_wf
∀n:ℕ. ∀p:Sym(n + 1).  (((p.f n) = n ∈ ℕn + 1) ⇒ (restrict_perm(p;n) ∈ Sym(n)))

Lemma: extend_restrict_perm_cancel
∀n:{1...}. ∀p:Sym(n).  (((p.f (n - 1)) = (n - 1) ∈ ℕn) ⇒ (↑{n - 1}(restrict_perm(p;n - 1)) = p ∈ Sym(n)))

Lemma: restrict_perm_using_txpose
∀n:{1...}. ∀p:Sym(n).  ∃q:Sym(n - 1). ∃i,j:ℕn. (p = txpose_perm(i;j) O ↑{n - 1}(q) ∈ Sym(n))

Lemma: trivial_nat1_fun
∀f:ℕ1 ⟶ ℕ1. (f = Id ∈ (ℕ1 ⟶ ℕ1))

Lemma: zero_sym_grp
∀p:Sym(0). (p = id_perm() ∈ Sym(0))

Lemma: trivial_sym_grp
∀p:Sym(1). (p = id_perm() ∈ Sym(1))

Lemma: mon_itop_txpose_invar
∀g:IAbMonoid. ∀n:ℕ. ∀E:ℕn ⟶ |g|. ∀x:ℕ+n.  ((Π 0 ≤ j < n. E[txpose_perm(x;0).f j]) = (Π 0 ≤ j < n. E[j]) ∈ |g|)



Home Index