---

Definition: permr
as ≡(T) bs ==  (||as|| = ||bs|| ∈ ℤ) c∧ (∃p:Sym(||as||). ∀i:ℕ||as||. (as[p.f i] = bs[i] ∈ T))

Lemma: permr_wf
∀T:Type. ∀as,bs:T List.  (as ≡(T) bs ∈ ℙ)

Lemma: comb_for_permr_wf
λT,as,bs,z. (as ≡(T) bs) ∈ T:Type ⟶ as:(T List) ⟶ bs:(T List) ⟶ (↓True) ⟶ ℙ

Lemma: permr_suptyping
∀T:Type. ∀Q:T ⟶ ℙ. ∀as,bs:{z:T| Q[z]}  List.  ((as ≡(T) bs) ⇒ (as ≡({z:T| Q[z]} ) bs))

Lemma: not_permr_cons_nil
∀T:Type. ∀a:T. ∀as:T List.  (¬([a / as] ≡(T) []))

Lemma: permr_nil_is_nil
∀T:Type. ∀as:T List.  ((as ≡(T) []) ⇒ (as = [] ∈ (T List)))

Lemma: permr_weakening
∀T:Type. ∀as,bs:T List.  ((as = bs ∈ (T List)) ⇒ (as ≡(T) bs))

Lemma: permr_reflex
∀T:Type. ∀as:T List.  (as ≡(T) as)

Lemma: permr_inversion
∀T:Type. ∀as,bs:T List.  ((bs ≡(T) as) ⇒ (as ≡(T) bs))

Lemma: permr_transitivity
∀T:Type. ∀as,bs,cs:T List.  ((as ≡(T) bs) ⇒ (bs ≡(T) cs) ⇒ (as ≡(T) cs))

Lemma: permr_equiv_rel
∀T:Type. EquivRel(T List;as,bs.as ≡(T) bs)

Lemma: cons_functionality_wrt_permr
∀T:Type. ∀a,b:T. ∀as,bs:T List.  ((a = b ∈ T) ⇒ (as ≡(T) bs) ⇒ ([a / as] ≡(T) [b / bs]))

Lemma: permr_functionality_wrt_permr
∀T,T':Type. ∀as:T List. ∀as':T' List. ∀bs:T List. ∀bs':T' List.
  ((T = T' ∈ Type) ⇒ (as ≡(T) as') ⇒ (bs ≡(T) bs') ⇒ (as ≡(T) bs ⇐⇒ as' ≡(T') bs'))

Lemma: perm_f_b_cancel
∀T:Type. ∀p:Perm(T). ∀x:T.  ((p.f (p.b x)) = x ∈ T)

Lemma: perm_b_f_cancel
∀T:Type. ∀p:Perm(T). ∀x:T.  ((p.b (p.f x)) = x ∈ T)

Lemma: perm_b_to_f
∀T:Type. ∀p:Perm(T). ∀x,y:T.  ((p.b x) = y ∈ T ⇐⇒ x = (p.f y) ∈ T)

Lemma: perm_f_inj
∀T:Type. ∀p:Perm(T). ∀x,y:T.  (((p.f x) = (p.f y) ∈ T) ⇒ (x = y ∈ T))

Lemma: perm_b_inj
∀T:Type. ∀p:Perm(T). ∀x,y:T.  (((p.b x) = (p.b y) ∈ T) ⇒ (x = y ∈ T))

Definition: tl_perm
tl_perm(p) ==  p O txpose_perm(0;p.b 0)

Lemma: tl_perm_wf
∀n:ℕ+. ∀p:Perm(ℕn).  (tl_perm(p) ∈ Perm(ℕ+n))

Definition: perm_morph
perm_morph(S;T;s2t;t2s;p) ==  mk_perm(s2t o (p.f o t2s);s2t o (p.b o t2s))

Lemma: perm_morph_wf
∀S,T:Type. ∀s2t:S ⟶ T. ∀t2s:T ⟶ S.  (InvFuns(S;T;s2t;t2s) ⇒ (∀p:Perm(S). (perm_morph(S;T;s2t;t2s;p) ∈ Perm(T))))

Lemma: permr_hd_cancel
∀T:Type. ∀a:T. ∀bs,bs':T List.  (([a / bs] ≡(T) [a / bs']) ⇒ (bs ≡(T) bs'))

Lemma: hd_two_swap_permr
∀T:Type. ∀as:T List. ∀a,a':T.  ([a; [a' / as]] ≡(T) [a'; [a / as]])

Lemma: cons_cons_permr
∀T:Type. ∀a,a':T. ∀as,as':T List.  ((as ≡(T) as') ⇒ ([a; [a' / as]] ≡(T) [a'; [a / as']]))

Lemma: append_functionality_wrt_permr
∀T:Type. ∀as,as',bs,bs':T List.  ((as ≡(T) as') ⇒ (bs ≡(T) bs') ⇒ ((as @ bs) ≡(T) (as' @ bs')))

Lemma: append_comm_1
∀T:Type. ∀a:T. ∀as:T List.  ((as @ [a]) ≡(T) ([a] @ as))

Lemma: append_comm
∀T:Type. ∀as,bs:T List.  ((as @ bs) ≡(T) (bs @ as))

Definition: permr_upto
as ≡ bs upto x,y.R[x; y]  ==  (||as|| = ||bs|| ∈ ℤ) c∧ (∃p:Sym(||as||). ∀i:ℕ||as||. R[as[p.f i]; bs[i]])

Lemma: permr_upto_wf
∀T:Type. ∀R:T ⟶ T ⟶ ℙ. ∀as,bs:T List.  (as ≡ bs upto x,y.R[x;y]  ∈ ℙ)

Lemma: permr_upto_inversion
∀T:Type. ∀R:T ⟶ T ⟶ ℙ.
  (EquivRel(T;x,y.R[x;y]) ⇒ (∀as,bs:T List.  (as ≡ bs upto x,y.R[x;y]  ⇒ bs ≡ as upto x,y.R[x;y] )))

Lemma: permr_upto_transitivity
∀T:Type. ∀R:T ⟶ T ⟶ ℙ.
  (EquivRel(T;x,y.R[x;y])
  ⇒ (∀as,bs,cs:T List.  (as ≡ bs upto x,y.R[x;y]  ⇒ bs ≡ cs upto x,y.R[x;y]  ⇒ as ≡ cs upto x,y.R[x;y] )))

Lemma: permr_upto_weakening
∀T:Type. ∀R:T ⟶ T ⟶ ℙ.  (EquivRel(T;x,y.R[x;y]) ⇒ (∀as,bs:T List.  ((as ≡(T) bs) ⇒ as ≡ bs upto x,y.R[x;y] )))

Lemma: permr_upto_equiv_rel
∀T:Type. ∀R:T ⟶ T ⟶ ℙ.  (EquivRel(T;x,y.R[x;y]) ⇒ EquivRel(T List;xs,ys.xs ≡ ys upto x,y.R[x;y] ))

Lemma: permr_upto_functionality_wrt_permr_upto
∀T:Type. ∀R:T ⟶ T ⟶ ℙ.
  (EquivRel(T;x,y.R[x;y])
  ⇒ (∀as,as',bs,bs':T List.
        (as ≡ bs upto x,y.R[x;y] 
        ⇒ as' ≡ bs' upto x,y.R[x;y] 
        ⇒ (as ≡ as' upto x,y.R[x;y]  ⇐⇒ bs ≡ bs' upto x,y.R[x;y] ))))

Definition: lequiv
as = bs upto {x,y.R[x; y]} ==  (||as|| = ||bs|| ∈ ℤ) c∧ (∀i:ℕ||as||. R[as[i]; bs[i]])

Lemma: lequiv_wf
∀T:Type. ∀R:T ⟶ T ⟶ ℙ. ∀as,bs:T List.  (as = bs upto {x,y.R[x;y]} ∈ ℙ)

Lemma: cons_functionality_wrt_lequiv
∀T:Type. ∀R:T ⟶ T ⟶ ℙ.
  (EquivRel(T;x,y.R[x;y])
  ⇒ (∀a,b:T. ∀as,bs:T List.  (R[a;b] ⇒ as = bs upto {x,y.R[x;y]} ⇒ [a / as] = [b / bs] upto {x,y.R[x;y]})))

Lemma: permr_upto_split
∀T:Type. ∀R:T ⟶ T ⟶ ℙ.
  (EquivRel(T;x,y.R[x;y])
  ⇒ (∀as,bs:T List.  (as ≡ bs upto x,y.R[x;y]  ⇐⇒ ∃cs:T List. ((as ≡(T) cs) ∧ cs = bs upto {x,y.R[x;y]}))))

Lemma: cons_functionality_wrt_permr_upto
∀T:Type. ∀R:T ⟶ T ⟶ ℙ.
  (EquivRel(T;x,y.R[x;y])
  ⇒ (∀a,b:T. ∀as,bs:T List.  (R[a;b] ⇒ as ≡ bs upto x,y.R[x;y]  ⇒ [a / as] ≡ [b / bs] upto x,y.R[x;y] )))



Home Index