---

Step * 2 of Lemma assert-eq_mFO


1. knd : Atom
2. left : mFOL()
3. right : mFOL()
4. ∀y:mFOL(). uiff(↑eq_mFO(left;y);left = y ∈ mFOL())
5. ∀y:mFOL(). uiff(↑eq_mFO(right;y);right = y ∈ mFOL())
6. k1 : Atom
7. l1 : mFOL()
8. r1 : mFOL()
9. uiff(↑eq_mFO(mFOconnect(knd;left;right);l1);mFOconnect(knd;left;right) = l1 ∈ mFOL())
10. uiff(↑eq_mFO(mFOconnect(knd;left;right);r1);mFOconnect(knd;left;right) = r1 ∈ mFOL())
⊢ uiff(↑if k1 =a knd
then (mFOL_ind(left;
               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'))  
      l1)
     ∧b (mFOL_ind(right;
                  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'))  
         r1)
else inr ⋅ 
fi ;mFOconnect(knd;left;right) = mFOconnect(k1;l1;r1) ∈ mFOL())
BY
{ (Fold `mFO-equal` 0 THEN Fold `eq_mFO` 0 THEN AutoSplit) }

1
1. knd : Atom
2. left : mFOL()
3. right : mFOL()
4. ∀y:mFOL(). uiff(↑eq_mFO(left;y);left = y ∈ mFOL())
5. ∀y:mFOL(). uiff(↑eq_mFO(right;y);right = y ∈ mFOL())
6. k1 : Atom
7. l1 : mFOL()
8. r1 : mFOL()
9. uiff(↑eq_mFO(mFOconnect(knd;left;right);l1);mFOconnect(knd;left;right) = l1 ∈ mFOL())
10. uiff(↑eq_mFO(mFOconnect(knd;left;right);r1);mFOconnect(knd;left;right) = r1 ∈ mFOL())
11. k1 = knd ∈ Atom
⊢ uiff(↑(eq_mFO(left;l1) ∧b eq_mFO(right;r1));mFOconnect(knd;left;right) = mFOconnect(k1;l1;r1) ∈ mFOL())

2
1. knd : Atom
2. left : mFOL()
3. right : mFOL()
4. ∀y:mFOL(). uiff(↑eq_mFO(left;y);left = y ∈ mFOL())
5. ∀y:mFOL(). uiff(↑eq_mFO(right;y);right = y ∈ mFOL())
6. k1 : Atom
7. k1 ≠ knd ∈ Atom 
8. l1 : mFOL()
9. r1 : mFOL()
10. uiff(↑eq_mFO(mFOconnect(knd;left;right);l1);mFOconnect(knd;left;right) = l1 ∈ mFOL())
11. uiff(↑eq_mFO(mFOconnect(knd;left;right);r1);mFOconnect(knd;left;right) = r1 ∈ mFOL())
⊢ uiff(↑(inr ⋅ );mFOconnect(knd;left;right) = mFOconnect(k1;l1;r1) ∈ mFOL())

---

Latex:

---

Latex:

1.  knd  :  Atom
2.  left  :  mFOL()
3.  right  :  mFOL()
4.  \mforall{}y:mFOL().  uiff(\muparrow{}eq\_mFO(left;y);left  =  y)
5.  \mforall{}y:mFOL().  uiff(\muparrow{}eq\_mFO(right;y);right  =  y)
6.  k1  :  Atom
7.  l1  :  mFOL()
8.  r1  :  mFOL()
9.  uiff(\muparrow{}eq\_mFO(mFOconnect(knd;left;right);l1);mFOconnect(knd;left;right)  =  l1)
10.  uiff(\muparrow{}eq\_mFO(mFOconnect(knd;left;right);r1);mFOconnect(knd;left;right)  =  r1)
\mvdash{}  uiff(\muparrow{}if  k1  =a  knd
then  (mFOL\_ind(left;
                              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.let  w,b'  =  dest-if  ...  then  all  else  exists(y);  in
                                                                                                      (var  =\msubz{}  w)  \mwedge{}\msubb{}  (rec3  b'))   
            l1)
          \mwedge{}\msubb{}  (mFOL\_ind(right;
                                    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....)   
                  r1)
else  inr  \mcdot{} 
fi  ;mFOconnect(knd;left;right)  =  mFOconnect(k1;l1;r1))


By

---

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

---

Home Index