---

Step * of Lemma assert-eq_mFO

No Annotations
∀[x,y:mFOL()].  uiff(↑eq_mFO(x;y);x = y ∈ mFOL())
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (BLemma `mFOL-induction` THENA Auto)
   THEN (UnivCD THENA Auto)
   THEN MoveToConcl (-1)
   THEN (BLemma `mFOL-induction` THENA Auto)
   THEN (UnivCD THENA Auto)
   THEN RepUR ``eq_mFO mFO-equal`` 0⋅
   THEN RW (AddrC [1;1] UnfoldTopAbC) 0
   THEN Reduce 0
   THEN Try (Complete ((RepUR ``assert`` 0 THEN Auto)))) }

1
1. name : Atom
2. vars : ℤ List
3. n1 : Atom
4. v1 : ℤ List
⊢ uiff(↑(name =a n1 ∧b (list-deq(IntDeq) vars v1));name(vars) = n1(v1) ∈ 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. 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())

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x,y:mFOL()].    uiff(\muparrow{}eq\_mFO(x;y);x  =  y)


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (BLemma  `mFOL-induction`  THENA  Auto)
  THEN  (UnivCD  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (BLemma  `mFOL-induction`  THENA  Auto)
  THEN  (UnivCD  THENA  Auto)
  THEN  RepUR  ``eq\_mFO  mFO-equal``  0\mcdot{}
  THEN  RW  (AddrC  [1;1]  UnfoldTopAbC)  0
  THEN  Reduce  0
  THEN  Try  (Complete  ((RepUR  ``assert``  0  THEN  Auto))))

---

Home Index