---

Step * 1 of Lemma assert-eq_mFO


1. name : Atom@i
2. vars : ℤ List@i
3. n1 : Atom@i
4. v1 : ℤ List@i
⊢ uiff(↑(name =a n1 ∧b (list-deq(IntDeq) vars v1));name(vars) = n1(v1) ∈ mFOL())
BY
{ (Auto THEN Try ((DoSubsume THEN Auto))) }

1
1. name : Atom@i
2. vars : ℤ List@i
3. n1 : Atom@i
4. v1 : ℤ List@i
5. ↑(name =a n1 ∧b (list-deq(IntDeq) vars v1))
⊢ name(vars) = n1(v1) ∈ mFOL()

2
1. name : Atom@i
2. vars : ℤ List@i
3. n1 : Atom@i
4. v1 : ℤ List@i
5. name(vars) = n1(v1) ∈ mFOL()
6. name = n1 ∈ Atom
⊢ ↑(list-deq(IntDeq) vars v1)

---

Latex:



1.  name  :  Atom@i
2.  vars  :  \mBbbZ{}  List@i
3.  n1  :  Atom@i
4.  v1  :  \mBbbZ{}  List@i
\mvdash{}  uiff(\muparrow{}(name  =a  n1  \mwedge{}\msubb{}  (list-deq(IntDeq)  vars  v1));name(vars)  =  n1(v1))


By

(Auto  THEN  Try  ((DoSubsume  THEN  Auto)))

---

Home Index