---

Step * of Lemma es-prior-match-programmable

∀[Info,A,B:Type]. ∀[R:A ─→ B ─→ 𝔹]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (es-prior-match(R; X; Y) = λp.if R (fst(p)) (snd(p)) then {p} else {} fi [X;Y] ∈ EClass(A × B))
BY
{ (Auto
   THEN (BLemma `es-interface-extensionality` THENA Auto)
   THEN Try (Complete ((ProveSV THEN Auto)))
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN (RepUR ``es-prior-match es-interface-pair-prior es-filter-image`` 0⋅
         THEN RepUR ``in-eclass eclass-val eclass-compose1`` 0
         THEN Folds ``in-eclass eclass-val`` 0
         THEN RepeatFor 2 (AutoSplit))⋅) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[R:A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].
    (es-prior-match(R;  X;  Y)  =  \mlambda{}p.if  R  (fst(p))  (snd(p))  then  \{p\}  else  \{\}  fi  [X;Y])


By

---

Latex:
(Auto
  THEN  (BLemma  `es-interface-extensionality`  THENA  Auto)
  THEN  Try  (Complete  ((ProveSV  THEN  Auto)))
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (RepUR  ``es-prior-match  es-interface-pair-prior  es-filter-image``  0\mcdot{}
              THEN  RepUR  ``in-eclass  eclass-val  eclass-compose1``  0
              THEN  Folds  ``in-eclass  eclass-val``  0
              THEN  RepeatFor  2  (AutoSplit))\mcdot{})

---

Home Index