---

Step * 1 1 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|| ∈ ℤ
10. pa : Sym(||as||)
11. ∀i:ℕ||as||. R[as[pa.f i];bs[i]]
12. ||bs|| = ||cs|| ∈ ℤ
13. pb : Sym(||bs||)
14. ∀i:ℕ||bs||. R[bs[pb.f i];cs[i]]
15. ||as|| = ||cs|| ∈ ℤ
⊢ ∃p:Sym(||as||). ∀i:ℕ||as||. R[as[p.f i];cs[i]]
BY
{ With pa
        O pb (D 0) THEN Auto' }

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. pa : Sym(||as||)
11. ∀i:ℕ||as||. R[as[pa.f i];bs[i]]
12. ||bs|| = ||cs|| ∈ ℤ
13. pb : Sym(||bs||)
14. ∀i:ℕ||bs||. R[bs[pb.f i];cs[i]]
15. ||as|| = ||cs|| ∈ ℤ
16. i : ℕ||as||
⊢ R[as[pa O pb.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||
10.  pa  :  Sym(||as||)
11.  \mforall{}i:\mBbbN{}||as||.  R[as[pa.f  i];bs[i]]
12.  ||bs||  =  ||cs||
13.  pb  :  Sym(||bs||)
14.  \mforall{}i:\mBbbN{}||bs||.  R[bs[pb.f  i];cs[i]]
15.  ||as||  =  ||cs||
\mvdash{}  \mexists{}p:Sym(||as||).  \mforall{}i:\mBbbN{}||as||.  R[as[p.f  i];cs[i]]


By

---

Latex:
With  pa
            O  pb  (D  0)  THEN  Auto'

---

Home Index