---

Step * 1 1 of Lemma assert-eq_mFO


1. name : Atom
2. vars : ℤ List
3. n1 : Atom
4. v1 : ℤ List
5. ↑(name =a n1 ∧b (list-deq(IntDeq) vars v1))
⊢ name(vars) = n1(v1) ∈ mFOL()
BY
{ ((RW assert_pushdownC (-1) THEN Auto) THEN RWO "deq_property<" (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((RW  assert\_pushdownC  (-1)  THEN  Auto)  THEN  RWO  "deq\_property<"  (-1)\mcdot{}  THEN  Auto)

---

Home Index