---

Step * 3 of Lemma assert-PZF_safe


1. C : Type
⊢ ∀left,right:Form(C).
    ((∀vs:Atom List. (↑(FormSafe2(left) vs) ⇐⇒ FormSafe1''(left) vs))
    ⇒ (∀vs:Atom List. (↑(FormSafe2(right) vs) ⇐⇒ FormSafe1''(right) vs))
    ⇒ (∀vs:Atom List
          (↑eval as = FormFvs(left) in
            eval bs = FormFvs(right) in
              eval theta = vs-bs in
              (FormSafe2(left) theta) ∧b (FormSafe2(right) vs-theta)
              ∨beval phi = vs-as in
                (FormSafe2(left) vs-phi) ∧b (FormSafe2(right) phi)
          ⇐⇒ let theta = vs-FormFvs(right) in
                  (FormSafe1''(left) theta) ∧ (FormSafe1''(right) vs-theta)
              ∨ let phi = vs-FormFvs(left) in
                    (FormSafe1''(left) vs-phi) ∧ (FormSafe1''(right) phi))))
BY
{ (Intros
   THEN (GenConcl ⌜FormFvs(left) = as ∈ (Atom List)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜FormFvs(right) = bs ∈ (Atom List)⌝⋅ THENA Auto)
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN (GenConcl ⌜vs-bs = theta ∈ (Atom List)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜vs-as = phi ∈ (Atom List)⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (RW assert_pushdownC 0 THENA 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)
⊢ ((↑(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)

---

Latex:

---

Latex:

1.  C  :  Type
\mvdash{}  \mforall{}left,right:Form(C).
        ((\mforall{}vs:Atom  List.  (\muparrow{}(FormSafe2(left)  vs)  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(left)  vs))
        {}\mRightarrow{}  (\mforall{}vs:Atom  List.  (\muparrow{}(FormSafe2(right)  vs)  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(right)  vs))
        {}\mRightarrow{}  (\mforall{}vs:Atom  List
                    (\muparrow{}eval  as  =  FormFvs(left)  in
                        eval  bs  =  FormFvs(right)  in
                            eval  theta  =  vs-bs  in
                            (FormSafe2(left)  theta)  \mwedge{}\msubb{}  (FormSafe2(right)  vs-theta)
                            \mvee{}\msubb{}eval  phi  =  vs-as  in
                                (FormSafe2(left)  vs-phi)  \mwedge{}\msubb{}  (FormSafe2(right)  phi)
                    \mLeftarrow{}{}\mRightarrow{}  let  theta  =  vs-FormFvs(right)  in
                                    (FormSafe1''(left)  theta)  \mwedge{}  (FormSafe1''(right)  vs-theta)
                            \mvee{}  let  phi  =  vs-FormFvs(left)  in
                                        (FormSafe1''(left)  vs-phi)  \mwedge{}  (FormSafe1''(right)  phi))))


By

---

Latex:
(Intros
  THEN  (GenConcl  \mkleeneopen{}FormFvs(left)  =  as\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}FormFvs(right)  =  bs\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  (GenConcl  \mkleeneopen{}vs-bs  =  theta\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}vs-as  =  phi\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (RW  assert\_pushdownC  0  THENA  Auto))

---

Home Index