---

Step * of Lemma FormSafe1_functionality

∀C:Type. ∀phi:Form(C). ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ {(FormSafe1(phi) vs) ⇒ (FormSafe1(phi) ws)})
BY
{ (Intro
   THEN (BLemma `Form-induction` THENW Auto)
   THEN RepUR ``guard PZF-safe FormSafe1`` 0
   THEN Try (Fold `FormSafe1` 0)
   THEN Try (QuickAuto)) }

1
1. C : Type
⊢ ∀left,right:Form(C).
    ((∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(left) vs) ⇒ (FormSafe1(left) ws)))
    ⇒ (∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(right) vs) ⇒ (FormSafe1(right) ws)))
    ⇒ (∀vs,ws:Atom List.
          (l_subset(Atom;ws;vs)
          ⇒ ((↑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))))))))
          ⇒ ((↑null(ws))
             ∨ (∃x:Atom
                 (set-equal(Atom;ws;[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,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(element) vs) ⇒ (FormSafe1(element) ws)))
    ⇒ (∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(set) vs) ⇒ (FormSafe1(set) ws)))
    ⇒ (∀vs,ws:Atom List.
          (l_subset(Atom;ws;vs)
          ⇒ ((↑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)))))))
          ⇒ ((↑null(ws))
             ∨ (∃x:Atom
                 (set-equal(Atom;ws;[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,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(left) vs) ⇒ (FormSafe1(left) ws)))
    ⇒ (∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(right) vs) ⇒ (FormSafe1(right) ws)))
    ⇒ (∀vs,ws:Atom List.
          (l_subset(Atom;ws;vs)
          ⇒ (∃as,bs:Atom List
               (set-equal(Atom;vs;as @ bs)
               ∧ (FormSafe1(left) as)
               ∧ (FormSafe1(right) bs)
               ∧ (l_disjoint(Atom;as;FormFvs(right)) ∨ l_disjoint(Atom;bs;FormFvs(left)))))
          ⇒ (∃as,bs:Atom List
               (set-equal(Atom;ws;as @ bs)
               ∧ (FormSafe1(left) as)
               ∧ (FormSafe1(right) bs)
               ∧ (l_disjoint(Atom;as;FormFvs(right)) ∨ l_disjoint(Atom;bs;FormFvs(left))))))))

4
1. C : Type
⊢ ∀body:Form(C)
    ((∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(body) vs) ⇒ (FormSafe1(body) ws)))
    ⇒ (∀vs,ws:Atom List.
          (l_subset(Atom;ws;vs) ⇒ ((↑null(vs)) ∧ (FormSafe1(body) [])) ⇒ ((↑null(ws)) ∧ (FormSafe1(body) [])))))

5
1. C : Type
⊢ ∀var:Atom. ∀body:Form(C).
    ((∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ (FormSafe1(body) vs) ⇒ (FormSafe1(body) ws)))
    ⇒ (∀vs,ws:Atom List.
          (l_subset(Atom;ws;vs)
          ⇒ ((¬(var ∈ vs)) ∧ (FormSafe1(body) [var / vs]))
          ⇒ ((¬(var ∈ ws)) ∧ (FormSafe1(body) [var / ws])))))

---

Latex:

---

Latex:
\mforall{}C:Type.  \mforall{}phi:Form(C).  \mforall{}vs,ws:Atom  List.
    (l\_subset(Atom;ws;vs)  {}\mRightarrow{}  \{(FormSafe1(phi)  vs)  {}\mRightarrow{}  (FormSafe1(phi)  ws)\})


By

---

Latex:
(Intro
  THEN  (BLemma  `Form-induction`  THENW  Auto)
  THEN  RepUR  ``guard  PZF-safe  FormSafe1``  0
  THEN  Try  (Fold  `FormSafe1`  0)
  THEN  Try  (QuickAuto))

---

Home Index