---

Step * of Lemma copathAgree_transitivity

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])].
  ∀x,y,z:copath(a.B[a];w).
    ((copath-length(x) ≤ copath-length(y))
    ⇒ (copath-length(y) ≤ copath-length(z))
    ⇒ copathAgree(a.B[a];w;x;y)
    ⇒ copathAgree(a.B[a];w;y;z)
    ⇒ copathAgree(a.B[a];w;x;z))
BY
{ (((RepUR ``copath copathAgree copath-length`` 0 THEN Auto) THEN DVar `x' THEN DVar `y' THEN DVar `z' THEN All Reduce)
   THEN (Decide ⌜n < n1⌝⋅ THENA Auto)
   THEN (All Reduce THENA Auto)
   THEN (Decide ⌜n1 < n2⌝⋅ THENA Auto)
   THEN (All Reduce THENA Auto)
   THEN (Decide ⌜n < n2⌝⋅ THENA Auto)
   THEN (All Reduce THENA Auto)
   THEN All (RWO "not-lt")
   THEN Auto) }

1
1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. [w] : coW(A;a.B[a])
4. n : ℕ@i
5. x1 : coPath(a.B[a];w;n)@i
6. n1 : ℕ@i
7. y1 : coPath(a.B[a];w;n1)@i
8. n2 : ℕ@i
9. z1 : coPath(a.B[a];w;n2)@i
10. n ≤ n1
11. n1 ≤ n2
12. coPathAgree(a.B[a];n;w;x1;y1)
13. coPathAgree(a.B[a];n1;w;y1;z1)
14. n < n1
15. n1 < n2
16. n < n2
⊢ coPathAgree(a.B[a];n;w;x1;z1)

2
1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. [w] : coW(A;a.B[a])
4. n : ℕ@i
5. x1 : coPath(a.B[a];w;n)@i
6. n1 : ℕ@i
7. y1 : coPath(a.B[a];w;n1)@i
8. n2 : ℕ@i
9. z1 : coPath(a.B[a];w;n2)@i
10. n ≤ n1
11. n1 ≤ n2
12. coPathAgree(a.B[a];n;w;x1;y1)
13. coPathAgree(a.B[a];n2;w;y1;z1)
14. n < n1
15. n2 ≤ n1
16. n < n2
⊢ coPathAgree(a.B[a];n;w;x1;z1)

3
1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. [w] : coW(A;a.B[a])
4. n : ℕ@i
5. x1 : coPath(a.B[a];w;n)@i
6. n1 : ℕ@i
7. y1 : coPath(a.B[a];w;n1)@i
8. n2 : ℕ@i
9. z1 : coPath(a.B[a];w;n2)@i
10. n ≤ n1
11. n1 ≤ n2
12. coPathAgree(a.B[a];n1;w;x1;y1)
13. coPathAgree(a.B[a];n1;w;y1;z1)
14. n1 ≤ n
15. n1 < n2
16. n < n2
⊢ coPathAgree(a.B[a];n;w;x1;z1)

4
1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. [w] : coW(A;a.B[a])
4. n : ℕ@i
5. x1 : coPath(a.B[a];w;n)@i
6. n1 : ℕ@i
7. y1 : coPath(a.B[a];w;n1)@i
8. n2 : ℕ@i
9. z1 : coPath(a.B[a];w;n2)@i
10. n ≤ n1
11. n1 ≤ n2
12. coPathAgree(a.B[a];n1;w;x1;y1)
13. coPathAgree(a.B[a];n2;w;y1;z1)
14. n1 ≤ n
15. n2 ≤ n1
16. n2 ≤ n
⊢ coPathAgree(a.B[a];n2;w;x1;z1)

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w:coW(A;a.B[a])].
    \mforall{}x,y,z:copath(a.B[a];w).
        ((copath-length(x)  \mleq{}  copath-length(y))
        {}\mRightarrow{}  (copath-length(y)  \mleq{}  copath-length(z))
        {}\mRightarrow{}  copathAgree(a.B[a];w;x;y)
        {}\mRightarrow{}  copathAgree(a.B[a];w;y;z)
        {}\mRightarrow{}  copathAgree(a.B[a];w;x;z))


By

---

Latex:
(((RepUR  ``copath  copathAgree  copath-length``  0  THEN  Auto)
    THEN  DVar  `x'
    THEN  DVar  `y'
    THEN  DVar  `z'
    THEN  All  Reduce)
  THEN  (Decide  \mkleeneopen{}n  <  n1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (All  Reduce  THENA  Auto)
  THEN  (Decide  \mkleeneopen{}n1  <  n2\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (All  Reduce  THENA  Auto)
  THEN  (Decide  \mkleeneopen{}n  <  n2\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (All  Reduce  THENA  Auto)
  THEN  All  (RWO  "not-lt")
  THEN  Auto)

---

Home Index