---

Step * 3 1 of Lemma assert-PZF_safe


1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs:Atom List. (↑(FormSafe2(left) vs) ⇐⇒ FormSafe1''(left) vs)
5. ∀vs:Atom List. (↑(FormSafe2(right) vs) ⇐⇒ FormSafe1''(right) vs)
6. vs : Atom List
7. as : Atom List
8. FormFvs(left) = as ∈ (Atom List)
9. bs : Atom List
10. FormFvs(right) = bs ∈ (Atom List)
11. theta : Atom List
12. vs-bs = theta ∈ (Atom List)
13. phi : Atom List
14. vs-as = phi ∈ (Atom List)
⊢ ((↑(FormSafe2(left) theta)) ∧ (↑(FormSafe2(right) vs-theta)))
  ∨ ((↑(FormSafe2(left) vs-phi)) ∧ (↑(FormSafe2(right) phi)))
⇐⇒ let theta = theta in
        (FormSafe1''(left) theta) ∧ (FormSafe1''(right) vs-theta)
    ∨ let phi = phi in
          (FormSafe1''(left) vs-phi) ∧ (FormSafe1''(right) phi)
BY
{ (RepUR ``let`` 0 THEN Auto) }

1
1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs:Atom List. (↑(FormSafe2(left) vs) ⇐⇒ FormSafe1''(left) vs)
5. ∀vs:Atom List. (↑(FormSafe2(right) vs) ⇐⇒ FormSafe1''(right) vs)
6. vs : Atom List
7. as : Atom List
8. FormFvs(left) = as ∈ (Atom List)
9. bs : Atom List
10. FormFvs(right) = bs ∈ (Atom List)
11. theta : Atom List
12. vs-bs = theta ∈ (Atom List)
13. phi : Atom List
14. vs-as = phi ∈ (Atom List)
15. ((↑(FormSafe2(left) theta)) ∧ (↑(FormSafe2(right) vs-theta)))
∨ ((↑(FormSafe2(left) vs-phi)) ∧ (↑(FormSafe2(right) phi)))
⊢ ((FormSafe1''(left) theta) ∧ (FormSafe1''(right) vs-theta)) ∨ ((FormSafe1''(left) vs-phi) ∧ (FormSafe1''(right) phi))

2
1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs:Atom List. (↑(FormSafe2(left) vs) ⇐⇒ FormSafe1''(left) vs)
5. ∀vs:Atom List. (↑(FormSafe2(right) vs) ⇐⇒ FormSafe1''(right) vs)
6. vs : Atom List
7. as : Atom List
8. FormFvs(left) = as ∈ (Atom List)
9. bs : Atom List
10. FormFvs(right) = bs ∈ (Atom List)
11. theta : Atom List
12. vs-bs = theta ∈ (Atom List)
13. phi : Atom List
14. vs-as = phi ∈ (Atom List)
15. ((FormSafe1''(left) theta) ∧ (FormSafe1''(right) vs-theta))
∨ ((FormSafe1''(left) vs-phi) ∧ (FormSafe1''(right) phi))
⊢ ((↑(FormSafe2(left) theta)) ∧ (↑(FormSafe2(right) vs-theta)))
∨ ((↑(FormSafe2(left) vs-phi)) ∧ (↑(FormSafe2(right) phi)))

---

Latex:

---

Latex:

1.  C  :  Type
2.  left  :  Form(C)
3.  right  :  Form(C)
4.  \mforall{}vs:Atom  List.  (\muparrow{}(FormSafe2(left)  vs)  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(left)  vs)
5.  \mforall{}vs:Atom  List.  (\muparrow{}(FormSafe2(right)  vs)  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(right)  vs)
6.  vs  :  Atom  List
7.  as  :  Atom  List
8.  FormFvs(left)  =  as
9.  bs  :  Atom  List
10.  FormFvs(right)  =  bs
11.  theta  :  Atom  List
12.  vs-bs  =  theta
13.  phi  :  Atom  List
14.  vs-as  =  phi
\mvdash{}  ((\muparrow{}(FormSafe2(left)  theta))  \mwedge{}  (\muparrow{}(FormSafe2(right)  vs-theta)))
    \mvee{}  ((\muparrow{}(FormSafe2(left)  vs-phi))  \mwedge{}  (\muparrow{}(FormSafe2(right)  phi)))
\mLeftarrow{}{}\mRightarrow{}  let  theta  =  theta  in
                (FormSafe1''(left)  theta)  \mwedge{}  (FormSafe1''(right)  vs-theta)
        \mvee{}  let  phi  =  phi  in
                    (FormSafe1''(left)  vs-phi)  \mwedge{}  (FormSafe1''(right)  phi)


By

---

Latex:
(RepUR  ``let``  0  THEN  Auto)

---

Home Index