---

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
{ xxx(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⋅)xxx }

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:

---

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

---

Latex:
xxx(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{})xxx

---

Home Index