---

Step * 1 1 of Lemma trivial-mFOL-rename

.....subterm..... T:t
2:n
1. x : ℤ
2. y : ℤ
3. name : Atom
4. vars : ℤ List
5. ¬(y ∈ remove-repeats(IntDeq;vars))
⊢ vars = map(λv.if (v =z y) then x else v fi ;vars) ∈ (ℤ List)
BY
{ ((RWO "trivial_map" 0 THEN Auto) THEN Reduce 0 THEN AutoSplit) }

1
1. x : ℤ
2. y : ℤ
3. name : Atom
4. vars : ℤ List
5. ¬(y ∈ remove-repeats(IntDeq;vars))
6. x1 : ℤ
7. (x1 ∈ vars)
8. x1 = y ∈ ℤ
⊢ x = x1 ∈ ℤ

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  name  :  Atom
4.  vars  :  \mBbbZ{}  List
5.  \mneg{}(y  \mmember{}  remove-repeats(IntDeq;vars))
\mvdash{}  vars  =  map(\mlambda{}v.if  (v  =\msubz{}  y)  then  x  else  v  fi  ;vars)


By

---

Latex:
((RWO  "trivial\_map"  0  THEN  Auto)  THEN  Reduce  0  THEN  AutoSplit)

---

Home Index