---

Step * of Lemma fpf-join-idempotent

∀[A:Type]. ∀[B:A ─→ Type]. ∀[f:a:A fp-> B[a]]. ∀[eq:EqDecider(A)].  (f ⊕ f = f ∈ a:A fp-> B[a])
BY
{ (Auto
   THEN Repeat (Unfolds ``fpf-join fpf fpf-dom fpf-cap fpf-ap`` 0)
   THEN (D (-2))
   THEN All Reduce
   THEN Subst filter(λa.(¬ba ∈b d));d) ~ [] 0⋅) }

1
.....equality..... 
1. A : Type
2. B : A ─→ Type
3. d : A List
4. f1 : a:{a:A| (a ∈ d)}  ─→ B[a]
5. eq : EqDecider(A)
⊢ filter(λa.(¬ba ∈b d));d) ~ []

2
1. A : Type
2. B : A ─→ Type
3. d : A List
4. f1 : a:{a:A| (a ∈ d)}  ─→ B[a]
5. eq : EqDecider(A)
⊢ <d @ [], λa.if a ∈b d) then f1 a else f1 a fi > = <d, f1> ∈ (d:A List × (a:{a:A| (a ∈ d)}  ─→ B[a]))

---

Latex:


\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[f:a:A  fp->  B[a]].  \mforall{}[eq:EqDecider(A)].    (f  \moplus{}  f  =  f)


By

(Auto
  THEN  Repeat  (Unfolds  ``fpf-join  fpf  fpf-dom  fpf-cap  fpf-ap``  0)
  THEN  (D  (-2))
  THEN  All  Reduce
  THEN  Subst  filter(\mlambda{}a.(\mneg{}\msubb{}a  \mmember{}\msubb{}  d));d)  \msim{}  []  0\mcdot{})

---

Home Index