---

Step * of Lemma assert-eq_mFO

∀[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 ((Fold `mFO-equal` 0 THEN Fold `eq_mFO` 0))
         THEN Try (WithRuleCount 10000 ((RepUR ``assert`` 0 THEN Complete (Auto)))⋅))⋅) }

1
1. name : Atom@i
2. vars : ℤ List@i
3. n1 : Atom@i
4. v1 : ℤ List@i
⊢ uiff(↑(name =a n1 ∧b (list-deq(IntDeq) vars v1));name(vars) = n1(v1) ∈ mFOL())

2
1. knd : Atom@i
2. left : mFOL()@i
3. right : mFOL()@i
4. ∀y:mFOL(). uiff(↑eq_mFO(left;y);left = y ∈ mFOL())@i
5. ∀y:mFOL(). uiff(↑eq_mFO(right;y);right = y ∈ mFOL())@i
6. k1 : Atom@i
7. l1 : mFOL()@i
8. r1 : mFOL()@i
9. uiff(↑eq_mFO(mFOconnect(knd;left;right);l1);mFOconnect(knd;left;right) = l1 ∈ mFOL())@i
10. uiff(↑eq_mFO(mFOconnect(knd;left;right);r1);mFOconnect(knd;left;right) = r1 ∈ mFOL())@i
⊢ uiff(↑if k1 =a knd then eq_mFO(left;l1) ∧b eq_mFO(right;r1) else inr ⋅  fi ;mFOconnect(knd;left;right)
= mFOconnect(k1;l1;r1)
∈ mFOL())

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

---

Latex:


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


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\mcdot{}
              THEN  RW  (AddrC  [1;1]  UnfoldTopAbC)  0
              THEN  Reduce  0
              THEN  Try  ((Fold  `mFO-equal`  0  THEN  Fold  `eq\_mFO`  0))
              THEN  Try  (WithRuleCount  10000  ((RepUR  ``assert``  0  THEN  Complete  (Auto)))\mcdot{}))\mcdot{})

---

Home Index