---

Step * of Lemma fpf-join-sub

∀[A:Type]. ∀[B:A ─→ Type]. ∀[eq:EqDecider(A)]. ∀[f1,g1,f2,g2:a:A fp-> B[a]].
  (f1 ⊕ f2 ⊆ g1 ⊕ g2) supposing (f2 ⊆ g2 and f1 ⊆ g1 and f2 || g1)
BY
{ (Auto THEN (All (Unfold `fpf-sub`)) THEN Auto) }

1
1. A : Type
2. B : A ─→ Type
3. eq : EqDecider(A)
4. f1 : a:A fp-> B[a]
5. g1 : a:A fp-> B[a]
6. f2 : a:A fp-> B[a]
7. g2 : a:A fp-> B[a]
8. f2 || g1
9. ∀x:A. ((↑x ∈ dom(f1)) ⇒ ((↑x ∈ dom(g1)) c∧ (f1(x) = g1(x) ∈ B[x])))
10. ∀x:A. ((↑x ∈ dom(f2)) ⇒ ((↑x ∈ dom(g2)) c∧ (f2(x) = g2(x) ∈ B[x])))
11. x : A@i
12. ↑x ∈ dom(f1 ⊕ f2)@i
⊢ (↑x ∈ dom(g1)) ∨ (↑x ∈ dom(g2))

2
1. A : Type
2. B : A ─→ Type
3. eq : EqDecider(A)
4. f1 : a:A fp-> B[a]
5. g1 : a:A fp-> B[a]
6. f2 : a:A fp-> B[a]
7. g2 : a:A fp-> B[a]
8. f2 || g1
9. ∀x:A. ((↑x ∈ dom(f1)) ⇒ ((↑x ∈ dom(g1)) c∧ (f1(x) = g1(x) ∈ B[x])))
10. ∀x:A. ((↑x ∈ dom(f2)) ⇒ ((↑x ∈ dom(g2)) c∧ (f2(x) = g2(x) ∈ B[x])))
11. x : A@i
12. ↑x ∈ dom(f1 ⊕ f2)@i
13. ↑x ∈ dom(g1 ⊕ g2)
⊢ f1 ⊕ f2(x) = g1 ⊕ g2(x) ∈ B[x]

---

Latex:


\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f1,g1,f2,g2:a:A  fp->  B[a]].
    (f1  \moplus{}  f2  \msubseteq{}  g1  \moplus{}  g2)  supposing  (f2  \msubseteq{}  g2  and  f1  \msubseteq{}  g1  and  f2  ||  g1)


By

(Auto  THEN  (All  (Unfold  `fpf-sub`))  THEN  Auto)

---

Home Index