---

Step * 2 of Lemma FormSafe1'-iff-FormSafe1''


1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs:Atom List. (FormSafe1'(left) vs ⇐⇒ FormSafe1''(left) vs)
5. ∀vs:Atom List. (FormSafe1'(right) vs ⇐⇒ FormSafe1''(right) vs)
6. vs : Atom List
7. ∃phi:Atom List. (l_subset(Atom;phi;vs-FormFvs(left)) ∧ (FormSafe1'(left) vs-phi) ∧ (FormSafe1'(right) phi))
⊢ let phi = vs-FormFvs(left) in
      (FormSafe1''(left) vs-phi) ∧ (FormSafe1''(right) phi)
BY
{ (ExRepD THEN (Assert ⌜set-equal(Atom;vs-FormFvs(left);phi)⌝⋅ THENM (RepUR ``let`` 0 THEN Auto))) }

1
.....assertion..... 
1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs:Atom List. (FormSafe1'(left) vs ⇐⇒ FormSafe1''(left) vs)
5. ∀vs:Atom List. (FormSafe1'(right) vs ⇐⇒ FormSafe1''(right) vs)
6. vs : Atom List
7. phi : Atom List
8. l_subset(Atom;phi;vs-FormFvs(left))
9. FormSafe1'(left) vs-phi
10. FormSafe1'(right) phi
⊢ set-equal(Atom;vs-FormFvs(left);phi)

2
1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs:Atom List. (FormSafe1'(left) vs ⇐⇒ FormSafe1''(left) vs)
5. ∀vs:Atom List. (FormSafe1'(right) vs ⇐⇒ FormSafe1''(right) vs)
6. vs : Atom List
7. phi : Atom List
8. l_subset(Atom;phi;vs-FormFvs(left))
9. FormSafe1'(left) vs-phi
10. FormSafe1'(right) phi
11. set-equal(Atom;vs-FormFvs(left);phi)
⊢ FormSafe1''(left) vs-vs-FormFvs(left)

3
1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs:Atom List. (FormSafe1'(left) vs ⇐⇒ FormSafe1''(left) vs)
5. ∀vs:Atom List. (FormSafe1'(right) vs ⇐⇒ FormSafe1''(right) vs)
6. vs : Atom List
7. phi : Atom List
8. l_subset(Atom;phi;vs-FormFvs(left))
9. FormSafe1'(left) vs-phi
10. FormSafe1'(right) phi
11. set-equal(Atom;vs-FormFvs(left);phi)
12. FormSafe1''(left) vs-vs-FormFvs(left)
⊢ FormSafe1''(right) vs-FormFvs(left)

---

Latex:

---

Latex:

1.  C  :  Type
2.  left  :  Form(C)
3.  right  :  Form(C)
4.  \mforall{}vs:Atom  List.  (FormSafe1'(left)  vs  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(left)  vs)
5.  \mforall{}vs:Atom  List.  (FormSafe1'(right)  vs  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(right)  vs)
6.  vs  :  Atom  List
7.  \mexists{}phi:Atom  List
        (l\_subset(Atom;phi;vs-FormFvs(left))  \mwedge{}  (FormSafe1'(left)  vs-phi)  \mwedge{}  (FormSafe1'(right)  phi))
\mvdash{}  let  phi  =  vs-FormFvs(left)  in
            (FormSafe1''(left)  vs-phi)  \mwedge{}  (FormSafe1''(right)  phi)


By

---

Latex:
(ExRepD  THEN  (Assert  \mkleeneopen{}set-equal(Atom;vs-FormFvs(left);phi)\mkleeneclose{}\mcdot{}  THENM  (RepUR  ``let``  0  THEN  Auto)))

---

Home Index