---

Step * of Lemma assert-PZF_safe

No Annotations
∀C:Type. ∀phi:Form(C). ∀vs:Atom List.  (↑PZF_safe(phi;vs) ⇐⇒ PZF-safe(phi;vs))
BY
{ ((Intros THEN RepUR ``PZF_safe PZF-safe`` 0)
   THEN (RWO  "FormSafe1-iff-FormSafe1\'\'" 0 THENA Auto)
   THEN (Assert ⌜↑(FormSafe2(phi) vs) ⇐⇒ FormSafe1''(phi) vs⌝⋅ THENM (RWO "-1" 0 THEN Auto))
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (BLemma `Form-induction` THENW Auto)
   THEN RepUR ``FormSafe1\'\' FormSafe2`` 0
   THEN Try (Fold `FormSafe2` 0)
   THEN Try (Fold `FormSafe1\'\'` 0)
   THEN Try (QuickAuto)) }

1
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
          (↑(null(vs)
           ∨blet x = hd(vs) in
                 null(vs-[x])
                 ∧b ((FormVar?(left) ∧b FormVar-name(left) =a x ∧b (¬bx ∈b FormFvs(right)))
                    ∨b(FormVar?(right) ∧b FormVar-name(right) =a x ∧b (¬bx ∈b FormFvs(left)))))
          ⇐⇒ (↑null(vs))
              ∨ (∃x:Atom
                  (set-equal(Atom;vs;[x])
                  ∧ (((↑FormVar?(left)) ∧ (FormVar-name(left) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(right))))
                    ∨ ((↑FormVar?(right)) ∧ (FormVar-name(right) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(left))))))))))

2
1. C : Type
⊢ ∀element,set:Form(C).
    ((∀vs:Atom List. (↑(FormSafe2(element) vs) ⇐⇒ FormSafe1''(element) vs))
    ⇒ (∀vs:Atom List. (↑(FormSafe2(set) vs) ⇐⇒ FormSafe1''(set) vs))
    ⇒ (∀vs:Atom List
          (↑(null(vs)
           ∨blet x = hd(vs) in
                 null(vs-[x])
                 ∧b FormVar?(element)
                 ∧b FormVar-name(element) =a x
                 ∧b ((FormVar?(set) ∧b FormVar-name(set) =a x) ∨b(¬bx ∈b FormFvs(set))))
          ⇐⇒ (↑null(vs))
              ∨ (∃x:Atom
                  (set-equal(Atom;vs;[x])
                  ∧ (↑FormVar?(element))
                  ∧ (FormVar-name(element) = x ∈ Atom)
                  ∧ (((↑FormVar?(set)) ∧ (FormVar-name(set) = x ∈ Atom)) ∨ (¬(x ∈ FormFvs(set)))))))))

3
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))))

4
1. C : Type
⊢ ∀body:Form(C)
    ((∀vs:Atom List. (↑(FormSafe2(body) vs) ⇐⇒ FormSafe1''(body) vs))
    ⇒ (∀vs:Atom List. (↑(null(vs) ∧b (FormSafe2(body) [])) ⇐⇒ (↑null(vs)) ∧ (FormSafe1''(body) []))))

5
1. C : Type
⊢ ∀var:Atom. ∀body:Form(C).
    ((∀vs:Atom List. (↑(FormSafe2(body) vs) ⇐⇒ FormSafe1''(body) vs))
    ⇒ (∀vs:Atom List
          (↑((¬bvar ∈b vs) ∧b (FormSafe2(body) [var / vs])) ⇐⇒ (¬(var ∈ vs)) ∧ (FormSafe1''(body) [var / vs]))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}C:Type.  \mforall{}phi:Form(C).  \mforall{}vs:Atom  List.    (\muparrow{}PZF\_safe(phi;vs)  \mLeftarrow{}{}\mRightarrow{}  PZF-safe(phi;vs))


By

---

Latex:
((Intros  THEN  RepUR  ``PZF\_safe  PZF-safe``  0)
  THEN  (RWO    "FormSafe1-iff-FormSafe1\mbackslash{}'\mbackslash{}'"  0  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\muparrow{}(FormSafe2(phi)  vs)  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(phi)  vs\mkleeneclose{}\mcdot{}  THENM  (RWO  "-1"  0  THEN  Auto))
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (BLemma  `Form-induction`  THENW  Auto)
  THEN  RepUR  ``FormSafe1\mbackslash{}'\mbackslash{}'  FormSafe2``  0
  THEN  Try  (Fold  `FormSafe2`  0)
  THEN  Try  (Fold  `FormSafe1\mbackslash{}'\mbackslash{}'`  0)
  THEN  Try  (QuickAuto))

---

Home Index