---

Step * of Lemma fpf-compatible-join-cap

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ─→ Type]. ∀[f,g:a:A fp-> B[a]]. ∀[x:A]. ∀[z:B[x]].
  f ⊕ g(x)?z = g(x)?f(x)?z ∈ B[x] supposing f || g
BY
{ (((Auto
     THEN (Unfold `fpf-compatible` (-1))
     THEN Unfold `fpf-cap` 0
     THEN SplitOnConclITE
     THEN Auto
     THEN (RWO "fpf-join-dom" (-1)))
    THENA Auto
    )
   THEN Repeat ((SplitOnConclITE THEN Auto))
   ) }

1
.....truecase..... 
1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. f : a:A fp-> B[a]
5. g : a:A fp-> B[a]
6. x : A
7. z : B[x]
8. ∀x:A. (((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))) ⇒ (f(x) = g(x) ∈ B[x]))
9. (↑x ∈ dom(f)) ∨ (↑x ∈ dom(g))
10. ↑x ∈ dom(g)
⊢ f ⊕ g(x) = g(x) ∈ B[x]

2
.....falsecase..... 
1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. f : a:A fp-> B[a]
5. g : a:A fp-> B[a]
6. x : A
7. z : B[x]
8. ∀x:A. (((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))) ⇒ (f(x) = g(x) ∈ B[x]))
9. (↑x ∈ dom(f)) ∨ (↑x ∈ dom(g))
10. ¬↑x ∈ dom(g)
11. ¬↑x ∈ dom(f)
⊢ f ⊕ g(x) = z ∈ B[x]

3
.....truecase..... 
1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. f : a:A fp-> B[a]
5. g : a:A fp-> B[a]
6. x : A
7. z : B[x]
8. ∀x:A. (((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))) ⇒ (f(x) = g(x) ∈ B[x]))
9. ¬((↑x ∈ dom(f)) ∨ (↑x ∈ dom(g)))
10. ↑x ∈ dom(g)
⊢ z = g(x) ∈ B[x]

4
.....truecase..... 
1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. f : a:A fp-> B[a]
5. g : a:A fp-> B[a]
6. x : A
7. z : B[x]
8. ∀x:A. (((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))) ⇒ (f(x) = g(x) ∈ B[x]))
9. ¬((↑x ∈ dom(f)) ∨ (↑x ∈ dom(g)))
10. ¬↑x ∈ dom(g)
11. ↑x ∈ dom(f)
⊢ z = f(x) ∈ B[x]

---

Latex:


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


By

(((Auto
      THEN  (Unfold  `fpf-compatible`  (-1))
      THEN  Unfold  `fpf-cap`  0
      THEN  SplitOnConclITE
      THEN  Auto
      THEN  (RWO  "fpf-join-dom"  (-1)))
    THENA  Auto
    )
  THEN  Repeat  ((SplitOnConclITE  THEN  Auto))
  )

---

Home Index