---

Step * 1 of Lemma permr_upto_transitivity


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀a:T. R[a;a]
4. ∀a,b:T.  (R[a;b] ⇒ R[b;a])
5. ∀a,b,c:T.  (R[a;b] ⇒ R[b;c] ⇒ R[a;c])
6. as : T List
7. bs : T List
8. cs : T List
9. (||as|| = ||bs|| ∈ ℤ) c∧ (∃p:Sym(||as||). ∀i:ℕ||as||. R[as[p.f i];bs[i]])
10. (||bs|| = ||cs|| ∈ ℤ) c∧ (∃p:Sym(||bs||). ∀i:ℕ||bs||. R[bs[p.f i];cs[i]])
⊢ (||as|| = ||cs|| ∈ ℤ) c∧ (∃p:Sym(||as||). ∀i:ℕ||as||. R[as[p.f i];cs[i]])
BY
{ (OnCls [10; 11; 9; 10; 0] D THEN Try TRIVIAL) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀a:T. R[a;a]
4. ∀a,b:T.  (R[a;b] ⇒ R[b;a])
5. ∀a,b,c:T.  (R[a;b] ⇒ R[b;c] ⇒ R[a;c])
6. as : T List
7. bs : T List
8. cs : T List
9. ||as|| = ||bs|| ∈ ℤ
10. p1 : Sym(||as||)
11. ∀i:ℕ||as||. R[as[p1.f i];bs[i]]
12. ||bs|| = ||cs|| ∈ ℤ
13. p : Sym(||bs||)
14. ∀i:ℕ||bs||. R[bs[p.f i];cs[i]]
15. ||as|| = ||cs|| ∈ ℤ
⊢ ∃p:Sym(||as||). ∀i:ℕ||as||. R[as[p.f i];cs[i]]

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}a:T.  R[a;a]
4.  \mforall{}a,b:T.    (R[a;b]  {}\mRightarrow{}  R[b;a])
5.  \mforall{}a,b,c:T.    (R[a;b]  {}\mRightarrow{}  R[b;c]  {}\mRightarrow{}  R[a;c])
6.  as  :  T  List
7.  bs  :  T  List
8.  cs  :  T  List
9.  (||as||  =  ||bs||)  c\mwedge{}  (\mexists{}p:Sym(||as||).  \mforall{}i:\mBbbN{}||as||.  R[as[p.f  i];bs[i]])
10.  (||bs||  =  ||cs||)  c\mwedge{}  (\mexists{}p:Sym(||bs||).  \mforall{}i:\mBbbN{}||bs||.  R[bs[p.f  i];cs[i]])
\mvdash{}  (||as||  =  ||cs||)  c\mwedge{}  (\mexists{}p:Sym(||as||).  \mforall{}i:\mBbbN{}||as||.  R[as[p.f  i];cs[i]])


By

---

Latex:
(OnCls  [10;  11;  9;  10;  0]  D  THEN  Try  TRIVIAL)

---

Home Index