---

Step * 3 of Lemma PZF_safe_functionality


1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs,ws:Atom List.  (set-equal(Atom;vs;ws) ⇒ PZF_safe(left;vs) = PZF_safe(left;ws))
5. ∀vs,ws:Atom List.  (set-equal(Atom;vs;ws) ⇒ PZF_safe(right;vs) = PZF_safe(right;ws))
6. vs : Atom List
7. ws : Atom List
8. set-equal(Atom;vs;ws)
⊢ eval as = FormFvs(left) in
  eval bs = FormFvs(right) in
    eval theta = vs-bs in
    PZF_safe(left;theta) ∧b PZF_safe(right;vs-theta)
    ∨beval phi = vs-as in
      PZF_safe(left;vs-phi) ∧b PZF_safe(right;phi) 
= eval as = FormFvs(left) in
  eval bs = FormFvs(right) in
    eval theta = ws-bs in
    PZF_safe(left;theta) ∧b PZF_safe(right;ws-theta)
    ∨beval phi = ws-as in
      PZF_safe(left;ws-phi) ∧b PZF_safe(right;phi)
BY
{ (((GenConcl ⌜FormFvs(left) = as ∈ (Atom List)⌝⋅ THENA Auto) THEN (CallByValueReduce 0 THENA Auto))
   THEN (GenConcl ⌜FormFvs(right) = bs ∈ (Atom List)⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)) }

1
1. C : Type
2. left : Form(C)
3. right : Form(C)
4. ∀vs,ws:Atom List.  (set-equal(Atom;vs;ws) ⇒ PZF_safe(left;vs) = PZF_safe(left;ws))
5. ∀vs,ws:Atom List.  (set-equal(Atom;vs;ws) ⇒ PZF_safe(right;vs) = PZF_safe(right;ws))
6. vs : Atom List
7. ws : Atom List
8. set-equal(Atom;vs;ws)
9. as : Atom List
10. FormFvs(left) = as ∈ (Atom List)
11. bs : Atom List
12. FormFvs(right) = bs ∈ (Atom List)
⊢ eval theta = vs-bs in
  PZF_safe(left;theta) ∧b PZF_safe(right;vs-theta)
  ∨beval phi = vs-as in
    PZF_safe(left;vs-phi) ∧b PZF_safe(right;phi) 
= eval theta = ws-bs in
  PZF_safe(left;theta) ∧b PZF_safe(right;ws-theta)
  ∨beval phi = ws-as in
    PZF_safe(left;ws-phi) ∧b PZF_safe(right;phi)

---

Latex:

---

Latex:

1.  C  :  Type
2.  left  :  Form(C)
3.  right  :  Form(C)
4.  \mforall{}vs,ws:Atom  List.    (set-equal(Atom;vs;ws)  {}\mRightarrow{}  PZF\_safe(left;vs)  =  PZF\_safe(left;ws))
5.  \mforall{}vs,ws:Atom  List.    (set-equal(Atom;vs;ws)  {}\mRightarrow{}  PZF\_safe(right;vs)  =  PZF\_safe(right;ws))
6.  vs  :  Atom  List
7.  ws  :  Atom  List
8.  set-equal(Atom;vs;ws)
\mvdash{}  eval  as  =  FormFvs(left)  in
    eval  bs  =  FormFvs(right)  in
        eval  theta  =  vs-bs  in
        PZF\_safe(left;theta)  \mwedge{}\msubb{}  PZF\_safe(right;vs-theta)
        \mvee{}\msubb{}eval  phi  =  vs-as  in
            PZF\_safe(left;vs-phi)  \mwedge{}\msubb{}  PZF\_safe(right;phi) 
=  eval  as  =  FormFvs(left)  in
    eval  bs  =  FormFvs(right)  in
        eval  theta  =  ws-bs  in
        PZF\_safe(left;theta)  \mwedge{}\msubb{}  PZF\_safe(right;ws-theta)
        \mvee{}\msubb{}eval  phi  =  ws-as  in
            PZF\_safe(left;ws-phi)  \mwedge{}\msubb{}  PZF\_safe(right;phi)


By

---

Latex:
(((GenConcl  \mkleeneopen{}FormFvs(left)  =  as\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (CallByValueReduce  0  THENA  Auto))
  THEN  (GenConcl  \mkleeneopen{}FormFvs(right)  =  bs\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto))

---

Home Index