---

Step * 1 of Lemma fpf-sub-join-right2


∀A:Type. ∀B,C:A ─→ Type. ∀eq:EqDecider(A). ∀f:a:A fp-> B[a]. ∀g:a:A fp-> C[a].
  ((∀x:A. (((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))) ⇒ ((B[x] ⊆r C[x]) c∧ (f(x) = g(x) ∈ C[x])))) ⇒ g ⊆ f ⊕ g)
BY
{ Repeat ((D 0 THENA Complete ((Auto THEN TrySubsume)))) }

1
1. A : Type@i'
2. B : A ─→ Type@i'
3. C : A ─→ Type@i'
4. eq : EqDecider(A)@i
5. f : a:A fp-> B[a]@i
6. g : a:A fp-> C[a]@i
7. ∀x:A. (((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))) ⇒ ((B[x] ⊆r C[x]) c∧ (f(x) = g(x) ∈ C[x])))@i
8. x : A@i
9. ↑x ∈ dom(g)@i
⊢ ↑x ∈ dom(f ⊕ g)

2
1. A : Type@i'
2. B : A ─→ Type@i'
3. C : A ─→ Type@i'
4. eq : EqDecider(A)@i
5. f : a:A fp-> B[a]@i
6. g : a:A fp-> C[a]@i
7. ∀x:A. (((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))) ⇒ ((B[x] ⊆r C[x]) c∧ (f(x) = g(x) ∈ C[x])))@i
8. x : A@i
9. ↑x ∈ dom(g)@i
10. ↑x ∈ dom(f ⊕ g)
⊢ g(x) = f ⊕ g(x) ∈ C[x]

---

Latex:



\mforall{}A:Type.  \mforall{}B,C:A  {}\mrightarrow{}  Type.  \mforall{}eq:EqDecider(A).  \mforall{}f:a:A  fp->  B[a].  \mforall{}g:a:A  fp->  C[a].
    ((\mforall{}x:A.  (((\muparrow{}x  \mmember{}  dom(f))  \mwedge{}  (\muparrow{}x  \mmember{}  dom(g)))  {}\mRightarrow{}  ((B[x]  \msubseteq{}r  C[x])  c\mwedge{}  (f(x)  =  g(x)))))  {}\mRightarrow{}  g  \msubseteq{}  f  \moplus{}  g)


By

Repeat  ((D  0  THENA  Complete  ((Auto  THEN  TrySubsume))))

---

Home Index