---

Step * 3 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())
⊢ uiff(↑if i1 =b isall
then (var =z v1)
     ∧b (mFOL_ind(body;
                  mFOatomic(name,vars)⇒ λy.let R',vars' = dest-atomic(y) in
                                            name =a R' ∧b (list-deq(IntDeq) vars vars');
                  mFOconnect(knd,left,right)⇒ rec1,rec2.λy.let a',b' = dest-knd(y) in
                                                            (rec1 a') ∧b (rec2 b');
                  mFOquant(isall,var,body)⇒ rec3.λy.let w,b' = dest-if isall then all else exists(y); in
                                                      (var =z w) ∧b (rec3 b'))  
         b1)
else inr ⋅ 
fi ;mFOquant(isall;var;body) = mFOquant(i1;v1;b1) ∈ mFOL())
BY
{ ((Fold `mFO-equal` 0 THEN Fold `eq_mFO` 0) THEN AutoSplit) }

1
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())

2
1. isall : 𝔹
2. var : ℤ
3. body : mFOL()
4. ∀y:mFOL(). uiff(↑eq_mFO(body;y);body = y ∈ mFOL())
5. i1 : 𝔹
6. ¬i1 = isall
7. v1 : ℤ
8. b1 : mFOL()
9. uiff(↑eq_mFO(mFOquant(isall;var;body);b1);mFOquant(isall;var;body) = b1 ∈ mFOL())
⊢ uiff(↑(inr ⋅ );mFOquant(isall;var;body) = mFOquant(i1;v1;b1) ∈ mFOL())

---

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)
\mvdash{}  uiff(\muparrow{}if  i1  =b  isall
then  (var  =\msubz{}  v1)
          \mwedge{}\msubb{}  (mFOL\_ind(body;
                                    mFOatomic(name,vars){}\mRightarrow{}  \mlambda{}y.let  R',vars'  =  dest-atomic(y)  in
                                                                                        name  =a  R'  \mwedge{}\msubb{}  (list-deq(IntDeq)  vars  vars');
                                    mFOconnect(knd,left,right){}\mRightarrow{}  rec1,rec2.\mlambda{}y.let  a',b'  =  dest-knd(y)  in
                                                                                                                        (rec1  a')  \mwedge{}\msubb{}  (rec2  b');
                                    mFOquant(isall,var,body){}\mRightarrow{}  rec3.\mlambda{}y....)   
                  b1)
else  inr  \mcdot{} 
fi  ;mFOquant(isall;var;body)  =  mFOquant(i1;v1;b1))


By

---

Latex:
((Fold  `mFO-equal`  0  THEN  Fold  `eq\_mFO`  0)  THEN  AutoSplit)

---

Home Index