---

Step * 3 1 of Lemma assert-eq_mFO


1. isall : 𝔹
2. var : ℤ
3. body : mFOL()
4. ∀y:mFOL(). uiff(↑eq_mFO(body;y);body = y ∈ mFOL())
5. i1 : 𝔹
6. v1 : ℤ
7. b1 : mFOL()
8. uiff(↑eq_mFO(mFOquant(isall;var;body);b1);mFOquant(isall;var;body) = b1 ∈ mFOL())
9. i1 = isall
⊢ uiff(↑((var =z v1) ∧b eq_mFO(body;b1));mFOquant(isall;var;body) = mFOquant(i1;v1;b1) ∈ mFOL())
BY
{ ((RW assert_pushdownC 0 THENA Auto) THEN RWW "4 5" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  isall  :  \mBbbB{}
2.  var  :  \mBbbZ{}
3.  body  :  mFOL()
4.  \mforall{}y:mFOL().  uiff(\muparrow{}eq\_mFO(body;y);body  =  y)
5.  i1  :  \mBbbB{}
6.  v1  :  \mBbbZ{}
7.  b1  :  mFOL()
8.  uiff(\muparrow{}eq\_mFO(mFOquant(isall;var;body);b1);mFOquant(isall;var;body)  =  b1)
9.  i1  =  isall
\mvdash{}  uiff(\muparrow{}((var  =\msubz{}  v1)  \mwedge{}\msubb{}  eq\_mFO(body;b1));mFOquant(isall;var;body)  =  mFOquant(i1;v1;b1))


By

---

Latex:
((RW  assert\_pushdownC  0  THENA  Auto)  THEN  RWW  "4  5"  0  THEN  Auto)

---

Home Index