---

Step * 2 1 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())
11. k1 = knd ∈ Atom
⊢ uiff(↑(eq_mFO(left;l1) ∧b eq_mFO(right;r1));mFOconnect(knd;left;right) = mFOconnect(k1;l1;r1) ∈ mFOL())
BY
{ ((RW assert_pushdownC 0 THENA Auto) THEN RWW "4 5" 0 THEN Auto) }

---

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)
11.  k1  =  knd
\mvdash{}  uiff(\muparrow{}(eq\_mFO(left;l1)  \mwedge{}\msubb{}  eq\_mFO(right;r1));mFOconnect(knd;left;right)  =  mFOconnect(k1;l1;r1))


By

---

Latex:
((RW  assert\_pushdownC  0  THENA  Auto)  THEN  RWW  "4  5"  0  THEN  Auto)

---

Home Index