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