---

Step * 3 of Lemma assert-eq_mFO


1. isall : 𝔹@i
2. var : ℤ@i
3. body : mFOL()@i
4. ∀y:mFOL(). uiff(↑eq_mFO(body;y);body = y ∈ mFOL())@i
5. i1 : 𝔹@i
6. v1 : ℤ@i
7. b1 : mFOL()@i
8. uiff(↑eq_mFO(mFOquant(isall;var;body);b1);mFOquant(isall;var;body) = b1 ∈ mFOL())@i
⊢ uiff(↑if i1 =b isall then (var =z v1) ∧b eq_mFO(body;b1) else inr ⋅  fi ;mFOquant(isall;var;body)
= mFOquant(i1;v1;b1)
∈ mFOL())
BY
{ ((AutoSplit THEN Try (Fold `bfalse` 0)) THEN (RW assert_pushdownC 0 THENA Auto) THEN RWW "4 5" 0 THEN Auto) }

---

Latex:



1.  isall  :  \mBbbB{}@i
2.  var  :  \mBbbZ{}@i
3.  body  :  mFOL()@i
4.  \mforall{}y:mFOL().  uiff(\muparrow{}eq\_mFO(body;y);body  =  y)@i
5.  i1  :  \mBbbB{}@i
6.  v1  :  \mBbbZ{}@i
7.  b1  :  mFOL()@i
8.  uiff(\muparrow{}eq\_mFO(mFOquant(isall;var;body);b1);mFOquant(isall;var;body)  =  b1)@i
\mvdash{}  uiff(\muparrow{}if  i1  =b  isall  then  (var  =\msubz{}  v1)  \mwedge{}\msubb{}  eq\_mFO(body;b1)  else  inr  \mcdot{}    fi  ;mFOquant(isall;var;body)
=  mFOquant(i1;v1;b1))


By

((AutoSplit  THEN  Try  (Fold  `bfalse`  0))
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  RWW  "4  5"  0
  THEN  Auto)

---

Home Index