---

Step * of Lemma Accum-class-trans

∀[Info,B,A:Type].
  ∀R:B ⟶ B ⟶ ℙ. ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    (Trans(B;x,y.R[x;y])
    ⇒ (∀s1,s2:B.  SqStable(R[s1;s2]))
    ⇒ (∀a:A. ∀e:E.
          ((e1 <loc e) ⇒ e ≤loc e2  ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ Prior(Accum-class(f;init;X))?init(e) ⇒ R[s;f a s]))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ Accum-class(f;init;X)(e1)
    ⇒ v2 ∈ Accum-class(f;init;X)(e2)
    ⇒ (e1 <loc e2)
    ⇒ R[v1;v2])
BY
{ (RepeatFor 9 ((D 0 THENA Auto))
   THEN VrCausalInd'
   THEN Auto
   THEN RepeatFor 2 (MaUseClassRel'' (-2))
   THEN Try (Fold `Accum-class` (-2))
   THEN TrySquashExRepD (-2)
   THEN MaUseClassRel'' (-3)
   THEN TrySquashExRepD (-3)
   THEN D (-3)
   THEN ExRepD
   THEN Try (Complete ((Assert ⌜False⌝⋅ THEN Auto)))
   THEN RepUR ``es-p-local-pred`` (-4)
   THEN RepD
   THEN UseLoclTri ⌜es⌝⌜e1⌝⌜e'⌝⋅) }

1
1. Info : Type
2. B : Type
3. A : Type
4. R : B ⟶ B ⟶ ℙ@i'
5. f : A ⟶ B ⟶ B@i
6. init : Id ⟶ bag(B)@i
7. X : EClass(A)@i'
8. es : EO+(Info)@i'
9. e1 : E@i
10. e2 : E@i
11. ∀e':E
      ((e' < e2)
      ⇒ (∀v1,v2:B.
            (Trans(B;x,y.R[x;y])
            ⇒ (∀s1,s2:B.  SqStable(R[s1;s2]))
            ⇒ (∀a:A. ∀e:E.
                  ((e1 <loc e)
                  ⇒ e ≤loc e' 
                  ⇒ a ∈ X(e)
                  ⇒ (∀s:B. (s ∈ Prior(Accum-class(f;init;X))?init(e) ⇒ R[s;f a s]))))
            ⇒ single-valued-classrel(es;X;A)
            ⇒ single-valued-bag(init loc(e1);B)
            ⇒ v1 ∈ Accum-class(f;init;X)(e1)
            ⇒ v2 ∈ Accum-class(f;init;X)(e')
            ⇒ (e1 <loc e')
            ⇒ R[v1;v2])))
12. v1 : B@i
13. v2 : B@i
14. Trans(B;x,y.R[x;y])@i
15. ∀s1,s2:B.  SqStable(R[s1;s2])@i
16. ∀a:A. ∀e:E.
      ((e1 <loc e) ⇒ e ≤loc e2  ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ Prior(Accum-class(f;init;X))?init(e) ⇒ R[s;f a s])))@i
17. single-valued-classrel(es;X;A)@i
18. single-valued-bag(init loc(e1);B)@i
19. v1 ∈ Accum-class(f;init;X)(e1)@i
20. a : A
21. b : B
22. v2 = (f a b) ∈ B
23. e' : E
24. (e' <loc e2)
25. ↓∃w:B. w ∈ Accum-class(f;init;X)(e')
26. ∀e'':E. ((e'' <loc e2) ⇒ (e' <loc e'') ⇒ (¬↓∃w:B. w ∈ Accum-class(f;init;X)(e'')))
27. b ∈ Accum-class(f;init;X)(e')
28. a ∈ X(e2)
29. (e1 <loc e2)@i
30. (e1 <loc e')
⊢ R[v1;v2]

2
1. Info : Type
2. B : Type
3. A : Type
4. R : B ⟶ B ⟶ ℙ@i'
5. f : A ⟶ B ⟶ B@i
6. init : Id ⟶ bag(B)@i
7. X : EClass(A)@i'
8. es : EO+(Info)@i'
9. e1 : E@i
10. e2 : E@i
11. ∀e':E
      ((e' < e2)
      ⇒ (∀v1,v2:B.
            (Trans(B;x,y.R[x;y])
            ⇒ (∀s1,s2:B.  SqStable(R[s1;s2]))
            ⇒ (∀a:A. ∀e:E.
                  ((e1 <loc e)
                  ⇒ e ≤loc e' 
                  ⇒ a ∈ X(e)
                  ⇒ (∀s:B. (s ∈ Prior(Accum-class(f;init;X))?init(e) ⇒ R[s;f a s]))))
            ⇒ single-valued-classrel(es;X;A)
            ⇒ single-valued-bag(init loc(e1);B)
            ⇒ v1 ∈ Accum-class(f;init;X)(e1)
            ⇒ v2 ∈ Accum-class(f;init;X)(e')
            ⇒ (e1 <loc e')
            ⇒ R[v1;v2])))
12. v1 : B@i
13. v2 : B@i
14. Trans(B;x,y.R[x;y])@i
15. ∀s1,s2:B.  SqStable(R[s1;s2])@i
16. ∀a:A. ∀e:E.
      ((e1 <loc e) ⇒ e ≤loc e2  ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ Prior(Accum-class(f;init;X))?init(e) ⇒ R[s;f a s])))@i
17. single-valued-classrel(es;X;A)@i
18. single-valued-bag(init loc(e1);B)@i
19. v1 ∈ Accum-class(f;init;X)(e1)@i
20. a : A
21. b : B
22. v2 = (f a b) ∈ B
23. e' : E
24. (e' <loc e2)
25. ↓∃w:B. w ∈ Accum-class(f;init;X)(e')
26. ∀e'':E. ((e'' <loc e2) ⇒ (e' <loc e'') ⇒ (¬↓∃w:B. w ∈ Accum-class(f;init;X)(e'')))
27. b ∈ Accum-class(f;init;X)(e')
28. a ∈ X(e2)
29. (e1 <loc e2)@i
30. e1 = e' ∈ E
⊢ R[v1;v2]

3
1. Info : Type
2. B : Type
3. A : Type
4. R : B ⟶ B ⟶ ℙ@i'
5. f : A ⟶ B ⟶ B@i
6. init : Id ⟶ bag(B)@i
7. X : EClass(A)@i'
8. es : EO+(Info)@i'
9. e1 : E@i
10. e2 : E@i
11. ∀e':E
      ((e' < e2)
      ⇒ (∀v1,v2:B.
            (Trans(B;x,y.R[x;y])
            ⇒ (∀s1,s2:B.  SqStable(R[s1;s2]))
            ⇒ (∀a:A. ∀e:E.
                  ((e1 <loc e)
                  ⇒ e ≤loc e' 
                  ⇒ a ∈ X(e)
                  ⇒ (∀s:B. (s ∈ Prior(Accum-class(f;init;X))?init(e) ⇒ R[s;f a s]))))
            ⇒ single-valued-classrel(es;X;A)
            ⇒ single-valued-bag(init loc(e1);B)
            ⇒ v1 ∈ Accum-class(f;init;X)(e1)
            ⇒ v2 ∈ Accum-class(f;init;X)(e')
            ⇒ (e1 <loc e')
            ⇒ R[v1;v2])))
12. v1 : B@i
13. v2 : B@i
14. Trans(B;x,y.R[x;y])@i
15. ∀s1,s2:B.  SqStable(R[s1;s2])@i
16. ∀a:A. ∀e:E.
      ((e1 <loc e) ⇒ e ≤loc e2  ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ Prior(Accum-class(f;init;X))?init(e) ⇒ R[s;f a s])))@i
17. single-valued-classrel(es;X;A)@i
18. single-valued-bag(init loc(e1);B)@i
19. v1 ∈ Accum-class(f;init;X)(e1)@i
20. a : A
21. b : B
22. v2 = (f a b) ∈ B
23. e' : E
24. (e' <loc e2)
25. ↓∃w:B. w ∈ Accum-class(f;init;X)(e')
26. ∀e'':E. ((e'' <loc e2) ⇒ (e' <loc e'') ⇒ (¬↓∃w:B. w ∈ Accum-class(f;init;X)(e'')))
27. b ∈ Accum-class(f;init;X)(e')
28. a ∈ X(e2)
29. (e1 <loc e2)@i
30. (e' <loc e1)
⊢ R[v1;v2]

---

Latex:

---

Latex:
\mforall{}[Info,B,A:Type].
    \mforall{}R:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}.  \mforall{}f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  B.  \mforall{}init:Id  {}\mrightarrow{}  bag(B).  \mforall{}X:EClass(A).  \mforall{}es:EO+(Info).  \mforall{}e1,e2:E.
    \mforall{}v1,v2:B.
        (Trans(B;x,y.R[x;y])
        {}\mRightarrow{}  (\mforall{}s1,s2:B.    SqStable(R[s1;s2]))
        {}\mRightarrow{}  (\mforall{}a:A.  \mforall{}e:E.
                    ((e1  <loc  e)
                    {}\mRightarrow{}  e  \mleq{}loc  e2 
                    {}\mRightarrow{}  a  \mmember{}  X(e)
                    {}\mRightarrow{}  (\mforall{}s:B.  (s  \mmember{}  Prior(Accum-class(f;init;X))?init(e)  {}\mRightarrow{}  R[s;f  a  s]))))
        {}\mRightarrow{}  single-valued-classrel(es;X;A)
        {}\mRightarrow{}  single-valued-bag(init  loc(e1);B)
        {}\mRightarrow{}  v1  \mmember{}  Accum-class(f;init;X)(e1)
        {}\mRightarrow{}  v2  \mmember{}  Accum-class(f;init;X)(e2)
        {}\mRightarrow{}  (e1  <loc  e2)
        {}\mRightarrow{}  R[v1;v2])


By

---

Latex:
(RepeatFor  9  ((D  0  THENA  Auto))
  THEN  VrCausalInd'
  THEN  Auto
  THEN  RepeatFor  2  (MaUseClassRel''  (-2))
  THEN  Try  (Fold  `Accum-class`  (-2))
  THEN  TrySquashExRepD  (-2)
  THEN  MaUseClassRel''  (-3)
  THEN  TrySquashExRepD  (-3)
  THEN  D  (-3)
  THEN  ExRepD
  THEN  Try  (Complete  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)))
  THEN  RepUR  ``es-p-local-pred``  (-4)
  THEN  RepD
  THEN  UseLoclTri  \mkleeneopen{}es\mkleeneclose{}\mkleeneopen{}e1\mkleeneclose{}\mkleeneopen{}e'\mkleeneclose{}\mcdot{})

---

Home Index