---

Step * 1 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|| ∈ ℤ
16. i : ℕ||as||
⊢ R[as[pa O pb.f i];cs[i]]
BY
{ TryOnAllClauses (Unfold `so_apply`) 
THEN AbReduce 0 }

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.f (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||
16.  i  :  \mBbbN{}||as||
\mvdash{}  R[as[pa  O  pb.f  i];cs[i]]


By

---

Latex:
TryOnAllClauses  (Unfold  `so\_apply`) 
THEN  AbReduce  0

---

Home Index