---

Step * of Lemma rec-combined-class-opt-1-single-val

∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[F:A ─→ B ─→ B]. ∀[X:EClass(A)]. ∀[init:Id ─→ bag(B)].
  (single-valued-classrel(es;lifting-2(F)|X,Prior(self)?init|;B)) supposing 
     (single-valued-classrel(es;X;A) and 
     (∀l:Id. single-valued-bag(init l;B)))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``single-valued-classrel`` 0
   THEN Auto
   THEN InstLemma `rec-combined-class-opt-1-single-val0` [⌈Info⌉;⌈A⌉;⌈B⌉;⌈es⌉;⌈F⌉;⌈X⌉;⌈init⌉;⌈e⌉;⌈v1⌉;⌈v2⌉]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[F:A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].
    (single-valued-classrel(es;lifting-2(F)|X,Prior(self)?init|;B))  supposing 
          (single-valued-classrel(es;X;A)  and 
          (\mforall{}l:Id.  single-valued-bag(init  l;B)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``single-valued-classrel``  0
  THEN  Auto
  THEN  InstLemma  `rec-combined-class-opt-1-single-val0`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}init\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{};
  \mkleeneopen{}v2\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index