---

Step * 1 of Lemma free-from-atom-fpf-ap


∀a:Atom1. ∀A:Type. ∀eq:EqDecider(A). ∀B:A ─→ 𝕌'. ∀f:x:A fp-> B[x].
  (a#f:x:A fp-> B[x] ⇒ (∀x:A. (a#x:A ⇒ (↑x ∈ dom(f)) ⇒ a#f(x):B[x])))
BY
{ RepeatFor 5 ((D 0 THENA Auto))
THEN RepeatFor 4 ((At ⌈𝕌'⌉ (D 0)⋅ THENA Auto))
THEN (RWO "member-fpf-domain" (-1) THENA Auto) }

1
1. a : Atom1@i
2. A : Type@i'
3. eq : EqDecider(A)@i
4. B : A ─→ 𝕌'@i 2
5. f : x:A fp-> B[x]@i'
6. a#f:x:A fp-> B[x]@i'
7. x : A@i'
8. a#x:A@i'
9. (x ∈ fpf-domain(f))
⊢ a#f(x):B[x]

---

Latex:



\mforall{}a:Atom1.  \mforall{}A:Type.  \mforall{}eq:EqDecider(A).  \mforall{}B:A  {}\mrightarrow{}  \mBbbU{}'.  \mforall{}f:x:A  fp->  B[x].
    (a\#f:x:A  fp->  B[x]  {}\mRightarrow{}  (\mforall{}x:A.  (a\#x:A  {}\mRightarrow{}  (\muparrow{}x  \mmember{}  dom(f))  {}\mRightarrow{}  a\#f(x):B[x])))


By

RepeatFor  5  ((D  0  THENA  Auto))
THEN  RepeatFor  4  ((At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto))
THEN  (RWO  "member-fpf-domain"  (-1)  THENA  Auto)

---

Home Index