---

Step * of Lemma decidable__exists-prior-iterated-classrel

∀[Info,A,S:Type].
  ∀init:Id ─→ bag(S). ∀f:A ─→ S ─→ S. ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.
    (single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e);S)
    ⇒ Dec(∃v:S. prior-iterated-classrel(es;A;S;v;X;f;init;e)))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `prior-iterated-classrel` 0
   THEN (BoolCase ⌈first(e)⌉⋅ THENA Auto)
   THEN (InstLemma `decidable__exists-single-valued-bag` [⌈S⌉;⌈init loc(e)⌉]⋅ THENA Auto)
   THEN D (-1)) }

1
1. [Info] : Type
2. [A] : Type
3. [S] : Type
4. init : Id ─→ bag(S)@i
5. f : A ─→ S ─→ S@i
6. X : EClass(A)@i'
7. es : EO+(Info)@i'
8. e : E@i
9. single-valued-classrel(es;X;A)@i
10. single-valued-bag(init loc(e);S)@i
11. ↑first(e)
12. ∃v:S. v ↓∈ init loc(e)
⊢ Dec(∃v:S. ((True ∧ v ↓∈ init loc(e)) ∨ ((¬True) ∧ iterated-classrel(es;S;A;f;init;X;pred(e);v))))

2
1. [Info] : Type
2. [A] : Type
3. [S] : Type
4. init : Id ─→ bag(S)@i
5. f : A ─→ S ─→ S@i
6. X : EClass(A)@i'
7. es : EO+(Info)@i'
8. e : E@i
9. single-valued-classrel(es;X;A)@i
10. single-valued-bag(init loc(e);S)@i
11. ↑first(e)
12. ¬(∃v:S. v ↓∈ init loc(e))
⊢ Dec(∃v:S. ((True ∧ v ↓∈ init loc(e)) ∨ ((¬True) ∧ iterated-classrel(es;S;A;f;init;X;pred(e);v))))

3
1. [Info] : Type
2. [A] : Type
3. [S] : Type
4. init : Id ─→ bag(S)@i
5. f : A ─→ S ─→ S@i
6. X : EClass(A)@i'
7. es : EO+(Info)@i'
8. e : E@i
9. ¬↑first(e)
10. single-valued-classrel(es;X;A)@i
11. single-valued-bag(init loc(e);S)@i
12. ∃v:S. v ↓∈ init loc(e)
⊢ Dec(∃v:S. ((False ∧ v ↓∈ init loc(e)) ∨ ((¬False) ∧ iterated-classrel(es;S;A;f;init;X;pred(e);v))))

4
1. [Info] : Type
2. [A] : Type
3. [S] : Type
4. init : Id ─→ bag(S)@i
5. f : A ─→ S ─→ S@i
6. X : EClass(A)@i'
7. es : EO+(Info)@i'
8. e : E@i
9. ¬↑first(e)
10. single-valued-classrel(es;X;A)@i
11. single-valued-bag(init loc(e);S)@i
12. ¬(∃v:S. v ↓∈ init loc(e))
⊢ Dec(∃v:S. ((False ∧ v ↓∈ init loc(e)) ∨ ((¬False) ∧ iterated-classrel(es;S;A;f;init;X;pred(e);v))))

---

Latex:


\mforall{}[Info,A,S:Type].
    \mforall{}init:Id  {}\mrightarrow{}  bag(S).  \mforall{}f:A  {}\mrightarrow{}  S  {}\mrightarrow{}  S.  \mforall{}X:EClass(A).  \mforall{}es:EO+(Info).  \mforall{}e:E.
        (single-valued-classrel(es;X;A)
        {}\mRightarrow{}  single-valued-bag(init  loc(e);S)
        {}\mRightarrow{}  Dec(\mexists{}v:S.  prior-iterated-classrel(es;A;S;v;X;f;init;e)))


By

((UnivCD  THENA  Auto)
  THEN  Unfold  `prior-iterated-classrel`  0
  THEN  (BoolCase  \mkleeneopen{}first(e)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `decidable\_\_exists-single-valued-bag`  [\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}init  loc(e)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  (-1))

---

Home Index