---

Step * 2 of Lemma assert-eq_mFO


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())
BY
{ ((AutoSplit THEN Try (Fold `bfalse` 0)) THEN (RW assert_pushdownC 0 THENA Auto) THEN RWW "4 5" 0 THEN Auto) }

---

Latex:



1.  knd  :  Atom@i
2.  left  :  mFOL()@i
3.  right  :  mFOL()@i
4.  \mforall{}y:mFOL().  uiff(\muparrow{}eq\_mFO(left;y);left  =  y)@i
5.  \mforall{}y:mFOL().  uiff(\muparrow{}eq\_mFO(right;y);right  =  y)@i
6.  k1  :  Atom@i
7.  l1  :  mFOL()@i
8.  r1  :  mFOL()@i
9.  uiff(\muparrow{}eq\_mFO(mFOconnect(knd;left;right);l1);mFOconnect(knd;left;right)  =  l1)@i
10.  uiff(\muparrow{}eq\_mFO(mFOconnect(knd;left;right);r1);mFOconnect(knd;left;right)  =  r1)@i
\mvdash{}  uiff(\muparrow{}if  k1  =a  knd
then  eq\_mFO(left;l1)  \mwedge{}\msubb{}  eq\_mFO(right;r1)
else  inr  \mcdot{} 
fi  ;mFOconnect(knd;left;right)  =  mFOconnect(k1;l1;r1))


By

((AutoSplit  THEN  Try  (Fold  `bfalse`  0))
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  RWW  "4  5"  0
  THEN  Auto)

---

Home Index