---

Step * 1 1 of Lemma mFOL-abstract-functionality

.....subterm..... T:t
2:n
1. Dom : Type
2. S : FOStruct(Dom)
3. name : Atom@i'
4. vars : ℤ List@i'
5. a1 : FOAssignment(Dom)@i'
6. a2 : FOAssignment(Dom)@i'
7. ∀z:ℤ. ((z ∈ mFOL-freevars(name(vars))) ⇒ ((a1 z) = (a2 z) ∈ Dom))@i'
⊢ map(a1;vars) = map(a2;vars) ∈ (Dom List)
BY
{ (RepUR ``mFOL-freevars`` (-1)
   THEN (Assert ∀z:ℤ. ((z ∈ vars) ⇒ ((a1 z) = (a2 z) ∈ Dom)) BY
               (RepeatFor 2 (ParallelLast) THEN Auto))
   THEN Thin (-2)
   THEN ListInd 4
   THEN Reduce 0
   THEN Auto
   THEN EqCD
   THEN Auto
   THEN RepeatFor 2 ((BackThruSomeHyp THEN Auto))) }

---

Latex:


.....subterm.....  T:t
2:n
1.  Dom  :  Type
2.  S  :  FOStruct(Dom)
3.  name  :  Atom@i'
4.  vars  :  \mBbbZ{}  List@i'
5.  a1  :  FOAssignment(Dom)@i'
6.  a2  :  FOAssignment(Dom)@i'
7.  \mforall{}z:\mBbbZ{}.  ((z  \mmember{}  mFOL-freevars(name(vars)))  {}\mRightarrow{}  ((a1  z)  =  (a2  z)))@i'
\mvdash{}  map(a1;vars)  =  map(a2;vars)


By

(RepUR  ``mFOL-freevars``  (-1)
  THEN  (Assert  \mforall{}z:\mBbbZ{}.  ((z  \mmember{}  vars)  {}\mRightarrow{}  ((a1  z)  =  (a2  z)))  BY
                          (RepeatFor  2  (ParallelLast)  THEN  Auto))
  THEN  Thin  (-2)
  THEN  ListInd  4
  THEN  Reduce  0
  THEN  Auto
  THEN  EqCD
  THEN  Auto
  THEN  RepeatFor  2  ((BackThruSomeHyp  THEN  Auto)))

---

Home Index