---

Step * of Lemma fpf-join-assoc

∀[A:Type]. ∀[B:A ─→ Type]. ∀[eq:EqDecider(A)]. ∀[f,g,h:a:A fp-> B[a]].  (f ⊕ g ⊕ h = f ⊕ g ⊕ h ∈ a:A fp-> B[a])
BY
{ (Repeat (Unfolds ``fpf fpf-join fpf-cap fpf-ap fpf-dom`` 0)
   THEN Auto
   THEN DVar `f'
   THEN DVar `g'
   THEN DVar `h'
   THEN All Reduce
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
1:n
1. A : Type
2. B : A ─→ Type
3. eq : EqDecider(A)
4. d : A List
5. f1 : a:{a:A| (a ∈ d)}  ─→ B[a]
6. d1 : A List
7. g1 : a:{a:A| (a ∈ d1)}  ─→ B[a]
8. d2 : A List
9. h1 : a:{a:A| (a ∈ d2)}  ─→ B[a]
⊢ (d @ filter(λa.(¬ba ∈b d));d1 @ filter(λa.(¬ba ∈b d1));d2)))
= ((d @ filter(λa.(¬ba ∈b d));d1)) @ filter(λa.(¬ba ∈b d @ filter(λa.(¬ba ∈b d));d1)));d2))
∈ (A List)

2
.....subterm..... T:t
2:n
1. A : Type
2. B : A ─→ Type
3. eq : EqDecider(A)
4. d : A List
5. f1 : a:{a:A| (a ∈ d)}  ─→ B[a]
6. d1 : A List
7. g1 : a:{a:A| (a ∈ d1)}  ─→ B[a]
8. d2 : A List
9. h1 : a:{a:A| (a ∈ d2)}  ─→ B[a]
⊢ (λa.if a ∈b d) then f1 a
      if a ∈b d1) then g1 a
      else h1 a
      fi )
= (λa.if a ∈b d @ filter(λa.(¬ba ∈b d));d1)) then if a ∈b d) then f1 a else g1 a fi  else h1 a fi )
∈ (a:{a:A| (a ∈ d @ filter(λa.(¬ba ∈b d));d1 @ filter(λa.(¬ba ∈b d1));d2)))}  ─→ B[a])

---

Latex:


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


By

(Repeat  (Unfolds  ``fpf  fpf-join  fpf-cap  fpf-ap  fpf-dom``  0)
  THEN  Auto
  THEN  DVar  `f'
  THEN  DVar  `g'
  THEN  DVar  `h'
  THEN  All  Reduce
  THEN  EqCD
  THEN  Auto)

---

Home Index