---

Definition: Formco
Formco(C) ==
  corec(X.lbl:Atom × if lbl =a "Var" then Atom
                     if lbl =a "Const" then C
                     if lbl =a "Set" then var:Atom × X
                     if lbl =a "Equal" then left:X × X
                     if lbl =a "Member" then element:X × X
                     if lbl =a "And" then left:X × X
                     if lbl =a "Or" then left:X × X
                     if lbl =a "Not" then X
                     if lbl =a "All" then var:Atom × X
                     if lbl =a "Exists" then var:Atom × X
                     else Void
                     fi )

Lemma: Formco_wf
∀[C:Type]. (Formco(C) ∈ Type)

Lemma: Formco-ext
∀[C:Type]
  Formco(C) ≡ lbl:Atom × if lbl =a "Var" then Atom
                         if lbl =a "Const" then C
                         if lbl =a "Set" then var:Atom × Formco(C)
                         if lbl =a "Equal" then left:Formco(C) × Formco(C)
                         if lbl =a "Member" then element:Formco(C) × Formco(C)
                         if lbl =a "And" then left:Formco(C) × Formco(C)
                         if lbl =a "Or" then left:Formco(C) × Formco(C)
                         if lbl =a "Not" then Formco(C)
                         if lbl =a "All" then var:Atom × Formco(C)
                         if lbl =a "Exists" then var:Atom × Formco(C)
                         else Void
                         fi 

Definition: Formco_size
Formco_size(p) ==
  fix((λsize,p. let lbl,x = p 
                in if lbl =a "Var" then 0
                   if lbl =a "Const" then 0
                   if lbl =a "Set" then 1 + (size (snd(x)))
                   if lbl =a "Equal" then 1 + (size (fst(x))) + (size (snd(x)))
                   if lbl =a "Member" then 1 + (size (fst(x))) + (size (snd(x)))
                   if lbl =a "And" then 1 + (size (fst(x))) + (size (snd(x)))
                   if lbl =a "Or" then 1 + (size (fst(x))) + (size (snd(x)))
                   if lbl =a "Not" then 1 + (size x)
                   if lbl =a "All" then 1 + (size (snd(x)))
                   if lbl =a "Exists" then 1 + (size (snd(x)))
                   else 0
                   fi )) 
  p

Lemma: Formco_size_wf
∀[C:Type]. ∀[p:Formco(C)].  (Formco_size(p) ∈ partial(ℕ))

Definition: Form
Form(C) ==  {p:Formco(C)| (Formco_size(p))↓} 

Lemma: Form_wf
∀[C:Type]. (Form(C) ∈ Type)

Definition: Form_size
Form_size(p) ==
  fix((λsize,p. let lbl,x = p 
                in if lbl =a "Var" then 0
                   if lbl =a "Const" then 0
                   if lbl =a "Set" then 1 + (size (snd(x)))
                   if lbl =a "Equal" then 1 + (size (fst(x))) + (size (snd(x)))
                   if lbl =a "Member" then 1 + (size (fst(x))) + (size (snd(x)))
                   if lbl =a "And" then 1 + (size (fst(x))) + (size (snd(x)))
                   if lbl =a "Or" then 1 + (size (fst(x))) + (size (snd(x)))
                   if lbl =a "Not" then 1 + (size x)
                   if lbl =a "All" then 1 + (size (snd(x)))
                   if lbl =a "Exists" then 1 + (size (snd(x)))
                   else 0
                   fi )) 
  p

Lemma: Form_size_wf
∀[C:Type]. ∀[p:Form(C)].  (Form_size(p) ∈ ℕ)

Lemma: Form-ext
∀[C:Type]
  Form(C) ≡ lbl:Atom × if lbl =a "Var" then Atom
                       if lbl =a "Const" then C
                       if lbl =a "Set" then var:Atom × Form(C)
                       if lbl =a "Equal" then left:Form(C) × Form(C)
                       if lbl =a "Member" then element:Form(C) × Form(C)
                       if lbl =a "And" then left:Form(C) × Form(C)
                       if lbl =a "Or" then left:Form(C) × Form(C)
                       if lbl =a "Not" then Form(C)
                       if lbl =a "All" then var:Atom × Form(C)
                       if lbl =a "Exists" then var:Atom × Form(C)
                       else Void
                       fi 

Definition: FormVar
Vname ==  <"Var", name>

Lemma: FormVar_wf
∀[C:Type]. ∀[name:Atom].  (Vname ∈ Form(C))

Definition: FormConst
Const(value) ==  <"Const", value>

Lemma: FormConst_wf
∀[C:Type]. ∀[value:C].  (Const(value) ∈ Form(C))

Definition: FormSet
{var | phi} ==  <"Set", var, phi>

Lemma: FormSet_wf
∀[C:Type]. ∀[var:Atom]. ∀[phi:Form(C)].  ({var | phi} ∈ Form(C))

Definition: FormEqual
left = right ==  <"Equal", left, right>

Lemma: FormEqual_wf
∀[C:Type]. ∀[left,right:Form(C)].  (left = right ∈ Form(C))

Definition: FormMember
element ∈ set ==  <"Member", element, set>

Lemma: FormMember_wf
∀[C:Type]. ∀[element,set:Form(C)].  (element ∈ set ∈ Form(C))

Definition: FormAnd
left ∧ right) ==  <"And", left, right>

Lemma: FormAnd_wf
∀[C:Type]. ∀[left,right:Form(C)].  (left ∧ right) ∈ Form(C))

Definition: FormOr
left ∨ right ==  <"Or", left, right>

Lemma: FormOr_wf
∀[C:Type]. ∀[left,right:Form(C)].  (left ∨ right ∈ Form(C))

Definition: FormNot
¬(body) ==  <"Not", body>

Lemma: FormNot_wf
∀[C:Type]. ∀[body:Form(C)].  (¬(body) ∈ Form(C))

Definition: FormAll
∀var. body ==  <"All", var, body>

Lemma: FormAll_wf
∀[C:Type]. ∀[var:Atom]. ∀[body:Form(C)].  (∀var. body ∈ Form(C))

Definition: FormExists
∃var. body ==  <"Exists", var, body>

Lemma: FormExists_wf
∀[C:Type]. ∀[var:Atom]. ∀[body:Form(C)].  (∃var. body ∈ Form(C))

Definition: FormVar?
FormVar?(v) ==  fst(v) =a "Var"

Lemma: FormVar?_wf
∀[C:Type]. ∀[v:Form(C)].  (FormVar?(v) ∈ 𝔹)

Definition: FormVar-name
FormVar-name(v) ==  snd(v)

Lemma: FormVar-name_wf
∀[C:Type]. ∀[v:Form(C)].  FormVar-name(v) ∈ Atom supposing ↑FormVar?(v)

Definition: FormConst?
FormConst?(v) ==  fst(v) =a "Const"

Lemma: FormConst?_wf
∀[C:Type]. ∀[v:Form(C)].  (FormConst?(v) ∈ 𝔹)

Definition: FormConst-value
FormConst-value(v) ==  snd(v)

Lemma: FormConst-value_wf
∀[C:Type]. ∀[v:Form(C)].  FormConst-value(v) ∈ C supposing ↑FormConst?(v)

Definition: FormSet?
FormSet?(v) ==  fst(v) =a "Set"

Lemma: FormSet?_wf
∀[C:Type]. ∀[v:Form(C)].  (FormSet?(v) ∈ 𝔹)

Definition: FormSet-var
FormSet-var(v) ==  fst(snd(v))

Lemma: FormSet-var_wf
∀[C:Type]. ∀[v:Form(C)].  FormSet-var(v) ∈ Atom supposing ↑FormSet?(v)

Definition: FormSet-phi
FormSet-phi(v) ==  snd(snd(v))

Lemma: FormSet-phi_wf
∀[C:Type]. ∀[v:Form(C)].  FormSet-phi(v) ∈ Form(C) supposing ↑FormSet?(v)

Definition: FormEqual?
FormEqual?(v) ==  fst(v) =a "Equal"

Lemma: FormEqual?_wf
∀[C:Type]. ∀[v:Form(C)].  (FormEqual?(v) ∈ 𝔹)

Definition: FormEqual-left
FormEqual-left(v) ==  fst(snd(v))

Lemma: FormEqual-left_wf
∀[C:Type]. ∀[v:Form(C)].  FormEqual-left(v) ∈ Form(C) supposing ↑FormEqual?(v)

Definition: FormEqual-right
FormEqual-right(v) ==  snd(snd(v))

Lemma: FormEqual-right_wf
∀[C:Type]. ∀[v:Form(C)].  FormEqual-right(v) ∈ Form(C) supposing ↑FormEqual?(v)

Definition: FormMember?
FormMember?(v) ==  fst(v) =a "Member"

Lemma: FormMember?_wf
∀[C:Type]. ∀[v:Form(C)].  (FormMember?(v) ∈ 𝔹)

Definition: FormMember-element
FormMember-element(v) ==  fst(snd(v))

Lemma: FormMember-element_wf
∀[C:Type]. ∀[v:Form(C)].  FormMember-element(v) ∈ Form(C) supposing ↑FormMember?(v)

Definition: FormMember-set
FormMember-set(v) ==  snd(snd(v))

Lemma: FormMember-set_wf
∀[C:Type]. ∀[v:Form(C)].  FormMember-set(v) ∈ Form(C) supposing ↑FormMember?(v)

Definition: FormAnd?
FormAnd?(v) ==  fst(v) =a "And"

Lemma: FormAnd?_wf
∀[C:Type]. ∀[v:Form(C)].  (FormAnd?(v) ∈ 𝔹)

Definition: FormAnd-left
FormAnd-left(v) ==  fst(snd(v))

Lemma: FormAnd-left_wf
∀[C:Type]. ∀[v:Form(C)].  FormAnd-left(v) ∈ Form(C) supposing ↑FormAnd?(v)

Definition: FormAnd-right
FormAnd-right(v) ==  snd(snd(v))

Lemma: FormAnd-right_wf
∀[C:Type]. ∀[v:Form(C)].  FormAnd-right(v) ∈ Form(C) supposing ↑FormAnd?(v)

Definition: FormOr?
FormOr?(v) ==  fst(v) =a "Or"

Lemma: FormOr?_wf
∀[C:Type]. ∀[v:Form(C)].  (FormOr?(v) ∈ 𝔹)

Definition: FormOr-left
FormOr-left(v) ==  fst(snd(v))

Lemma: FormOr-left_wf
∀[C:Type]. ∀[v:Form(C)].  FormOr-left(v) ∈ Form(C) supposing ↑FormOr?(v)

Definition: FormOr-right
FormOr-right(v) ==  snd(snd(v))

Lemma: FormOr-right_wf
∀[C:Type]. ∀[v:Form(C)].  FormOr-right(v) ∈ Form(C) supposing ↑FormOr?(v)

Definition: FormNot?
FormNot?(v) ==  fst(v) =a "Not"

Lemma: FormNot?_wf
∀[C:Type]. ∀[v:Form(C)].  (FormNot?(v) ∈ 𝔹)

Definition: FormNot-body
FormNot-body(v) ==  snd(v)

Lemma: FormNot-body_wf
∀[C:Type]. ∀[v:Form(C)].  FormNot-body(v) ∈ Form(C) supposing ↑FormNot?(v)

Definition: FormAll?
FormAll?(v) ==  fst(v) =a "All"

Lemma: FormAll?_wf
∀[C:Type]. ∀[v:Form(C)].  (FormAll?(v) ∈ 𝔹)

Definition: FormAll-var
FormAll-var(v) ==  fst(snd(v))

Lemma: FormAll-var_wf
∀[C:Type]. ∀[v:Form(C)].  FormAll-var(v) ∈ Atom supposing ↑FormAll?(v)

Definition: FormAll-body
FormAll-body(v) ==  snd(snd(v))

Lemma: FormAll-body_wf
∀[C:Type]. ∀[v:Form(C)].  FormAll-body(v) ∈ Form(C) supposing ↑FormAll?(v)

Definition: FormExists?
FormExists?(v) ==  fst(v) =a "Exists"

Lemma: FormExists?_wf
∀[C:Type]. ∀[v:Form(C)].  (FormExists?(v) ∈ 𝔹)

Definition: FormExists-var
FormExists-var(v) ==  fst(snd(v))

Lemma: FormExists-var_wf
∀[C:Type]. ∀[v:Form(C)].  FormExists-var(v) ∈ Atom supposing ↑FormExists?(v)

Definition: FormExists-body
FormExists-body(v) ==  snd(snd(v))

Lemma: FormExists-body_wf
∀[C:Type]. ∀[v:Form(C)].  FormExists-body(v) ∈ Form(C) supposing ↑FormExists?(v)

Lemma: Form-induction
∀[C:Type]. ∀[P:Form(C) ⟶ ℙ].
  ((∀name:Atom. P[Vname])
  ⇒ (∀value:C. P[Const(value)])
  ⇒ (∀var:Atom. ∀phi:Form(C).  (P[phi] ⇒ P[{var | phi}]))
  ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left = right]))
  ⇒ (∀element,set:Form(C).  (P[element] ⇒ P[set] ⇒ P[element ∈ set]))
  ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left ∧ right)]))
  ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left ∨ right]))
  ⇒ (∀body:Form(C). (P[body] ⇒ P[¬(body)]))
  ⇒ (∀var:Atom. ∀body:Form(C).  (P[body] ⇒ P[∀var. body]))
  ⇒ (∀var:Atom. ∀body:Form(C).  (P[body] ⇒ P[∃var. body]))
  ⇒ {∀v:Form(C). P[v]})

Lemma: Form-definition
∀[C,A:Type]. ∀[R:A ⟶ Form(C) ⟶ ℙ].
  ((∀name:Atom. {x:A| R[x;Vname]} )
  ⇒ (∀value:C. {x:A| R[x;Const(value)]} )
  ⇒ (∀var:Atom. ∀phi:Form(C).  ({x:A| R[x;phi]}  ⇒ {x:A| R[x;{var | phi}]} ))
  ⇒ (∀left,right:Form(C).  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;left = right]} ))
  ⇒ (∀element,set:Form(C).  ({x:A| R[x;element]}  ⇒ {x:A| R[x;set]}  ⇒ {x:A| R[x;element ∈ set]} ))
  ⇒ (∀left,right:Form(C).  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;left ∧ right)]} ))
  ⇒ (∀left,right:Form(C).  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;left ∨ right]} ))
  ⇒ (∀body:Form(C). ({x:A| R[x;body]}  ⇒ {x:A| R[x;¬(body)]} ))
  ⇒ (∀var:Atom. ∀body:Form(C).  ({x:A| R[x;body]}  ⇒ {x:A| R[x;∀var. body]} ))
  ⇒ (∀var:Atom. ∀body:Form(C).  ({x:A| R[x;body]}  ⇒ {x:A| R[x;∃var. body]} ))
  ⇒ {∀v:Form(C). {x:A| R[x;v]} })

Definition: Form_ind
Form_ind(v;
         FormVar(name)⇒ Var[name];
         FormConst(value)⇒ Const[value];
         FormSet(var,phi)⇒ rec1.Set[var;
                                     phi;
                                     rec1];
         FormEqual(left,right)⇒ rec2,rec3.Equal[left;
                                                 right;
                                                 rec2;
                                                 rec3];
         FormMember(element,set)⇒ rec4,rec5.Member[element;
                                                    set;
                                                    rec4;
                                                    rec5];
         FormAnd(left,right)⇒ rec6,rec7.And[left;
                                             right;
                                             rec6;
                                             rec7];
         FormOr(left,right)⇒ rec8,rec9.Or[left;
                                           right;
                                           rec8;
                                           rec9];
         FormNot(body)⇒ rec10.Not[body; rec10];
         FormAll(var,body)⇒ rec11.All[var;
                                       body;
                                       rec11];
         FormExists(var,body)⇒ rec12.Exists[var;
                                             body;
                                             rec12])  ==
  fix((λForm_ind,v. let lbl,v1 = v 
                    in if lbl="Var" then Var[v1]
                       if lbl="Const" then Const[v1]
                       if lbl="Set"
                         then let var,v2 = v1 
                              in Set[var;
                                     v2;
                                     Form_ind v2]
                       if lbl="Equal"
                         then let left,v2 = v1 
                              in Equal[left;
                                       v2;
                                       Form_ind left;
                                       Form_ind v2]
                       if lbl="Member"
                         then let element,v2 = v1 
                              in Member[element;
                                        v2;
                                        Form_ind element;
                                        Form_ind v2]
                       if lbl="And"
                         then let left,v2 = v1 
                              in And[left;
                                     v2;
                                     Form_ind left;
                                     Form_ind v2]
                       if lbl="Or"
                         then let left,v2 = v1 
                              in Or[left;
                                    v2;
                                    Form_ind left;
                                    Form_ind v2]
                       if lbl="Not" then Not[v1; Form_ind v1]
                       if lbl="All"
                         then let var,v2 = v1 
                              in All[var;
                                     v2;
                                     Form_ind v2]
                       if lbl="Exists"
                         then let var,v2 = v1 
                              in Exists[var;
                                        v2;
                                        Form_ind v2]
                       else Ax
                       fi )) 
  v

Lemma: Form_ind_wf
∀[C,A:Type]. ∀[R:A ⟶ Form(C) ⟶ ℙ]. ∀[v:Form(C)]. ∀[Var:name:Atom ⟶ {x:A| R[x;Vname]} ].
∀[Const:value:C ⟶ {x:A| R[x;Const(value)]} ]. ∀[Set:var:Atom
                                                    ⟶ phi:Form(C)
                                                    ⟶ {x:A| R[x;phi]} 
                                                    ⟶ {x:A| R[x;{var | phi}]} ]. ∀[Equal:left:Form(C)
                                                                                         ⟶ right:Form(C)
                                                                                         ⟶ {x:A| R[x;left]} 
                                                                                         ⟶ {x:A| R[x;right]} 
                                                                                         ⟶ {x:A| R[x;left = right]} ].
∀[Member:element:Form(C) ⟶ set:Form(C) ⟶ {x:A| R[x;element]}  ⟶ {x:A| R[x;set]}  ⟶ {x:A| R[x;element ∈ set]} ].
∀[And:left:Form(C) ⟶ right:Form(C) ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;left ∧ right)]} ].
∀[Or:left:Form(C) ⟶ right:Form(C) ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;left ∨ right]} ].
∀[Not:body:Form(C) ⟶ {x:A| R[x;body]}  ⟶ {x:A| R[x;¬(body)]} ]. ∀[All:var:Atom
                                                                      ⟶ body:Form(C)
                                                                      ⟶ {x:A| R[x;body]} 
                                                                      ⟶ {x:A| R[x;∀var. body]} ].
∀[Exists:var:Atom ⟶ body:Form(C) ⟶ {x:A| R[x;body]}  ⟶ {x:A| R[x;∃var. body]} ].
  (Form_ind(v;
            FormVar(name)⇒ Var[name];
            FormConst(value)⇒ Const[value];
            FormSet(var,phi)⇒ rec1.Set[var;phi;rec1];
            FormEqual(left,right)⇒ rec2,rec3.Equal[left;right;rec2;rec3];
            FormMember(element,set)⇒ rec4,rec5.Member[element;set;rec4;rec5];
            FormAnd(left,right)⇒ rec6,rec7.And[left;right;rec6;rec7];
            FormOr(left,right)⇒ rec8,rec9.Or[left;right;rec8;rec9];
            FormNot(body)⇒ rec10.Not[body;rec10];
            FormAll(var,body)⇒ rec11.All[var;body;rec11];
            FormExists(var,body)⇒ rec12.Exists[var;body;rec12])  ∈ {x:A| R[x;v]} )

Lemma: Form_ind_wf_simple
∀[C,A:Type]. ∀[v:Form(C)]. ∀[Var:name:Atom ⟶ A]. ∀[Const:value:C ⟶ A]. ∀[Set:var:Atom ⟶ phi:Form(C) ⟶ A ⟶ A].
∀[Equal,Member,And,Or:left:Form(C) ⟶ right:Form(C) ⟶ A ⟶ A ⟶ A]. ∀[Not:body:Form(C) ⟶ A ⟶ A].
∀[All,Exists:var:Atom ⟶ body:Form(C) ⟶ A ⟶ A].
  (Form_ind(v;
            FormVar(name)⇒ Var[name];
            FormConst(value)⇒ Const[value];
            FormSet(var,phi)⇒ rec1.Set[var;phi;rec1];
            FormEqual(left,right)⇒ rec2,rec3.Equal[left;right;rec2;rec3];
            FormMember(element,set)⇒ rec4,rec5.Member[element;set;rec4;rec5];
            FormAnd(left,right)⇒ rec6,rec7.And[left;right;rec6;rec7];
            FormOr(left,right)⇒ rec8,rec9.Or[left;right;rec8;rec9];
            FormNot(body)⇒ rec10.Not[body;rec10];
            FormAll(var,body)⇒ rec11.All[var;body;rec11];
            FormExists(var,body)⇒ rec12.Exists[var;body;rec12])  ∈ A)

Lemma: subtype_rel_Formco
∀[A,B:Type].  Formco(A) ⊆r Formco(B) supposing A ⊆r B

Lemma: subtype_rel_Form
∀[A,B:Type].  Form(A) ⊆r Form(B) supposing A ⊆r B

Definition: wfFormAux
wfFormAux(f) ==
  Form_ind(f;
           FormVar(v)⇒ λisterm.isterm;
           FormConst(c)⇒ λisterm.isterm;
           FormSet(x,phi)⇒ r.λisterm.(isterm ∧b (r ff));
           FormEqual(l,r)⇒ r1,r2.λisterm.((¬bisterm) ∧b (r1 tt) ∧b (r2 tt));
           FormMember(e,s)⇒ r1,r2.λisterm.((¬bisterm) ∧b (r1 tt) ∧b (r2 tt));
           FormAnd(l,r)⇒ r1,r2.λisterm.((¬bisterm) ∧b (r1 ff) ∧b (r2 ff));
           FormOr(l,r)⇒ r1,r2.λisterm.((¬bisterm) ∧b (r1 ff) ∧b (r2 ff));
           FormNot(b)⇒ r1.λisterm.((¬bisterm) ∧b (r1 ff));
           FormAll(x,b)⇒ r1.λisterm.((¬bisterm) ∧b (r1 ff));
           FormExists(x,b)⇒ r1.λisterm.((¬bisterm) ∧b (r1 ff))) 

Lemma: wfFormAux_wf
∀[c:Type]. ∀[f:Form(c)].  (wfFormAux(f) ∈ 𝔹 ⟶ 𝔹)

Definition: termForm
termForm(f) ==
  Form_ind(f;
           FormVar(v)⇒ tt;
           FormConst(c)⇒ tt;
           FormSet(x,phi)⇒ r.tt;
           FormEqual(l,r)⇒ a,b.ff;
           FormMember(e,s)⇒ a,b.ff;
           FormAnd(l,r)⇒ a,b.ff;
           FormOr(l,r)⇒ a,b.ff;
           FormNot(x)⇒ a.ff;
           FormAll(x,b)⇒ a.ff;
           FormExists(x,b)⇒ a.ff) 

Lemma: termForm_wf
∀[c:Type]. ∀[f:Form(c)].  (termForm(f) ∈ 𝔹)

Definition: wfForm
wfForm(f) ==  wfFormAux(f) termForm(f)

Lemma: wfForm_wf
∀[C:Type]. ∀[f:Form(C)].  (wfForm(f) ∈ 𝔹)

Lemma: wfFormAux-unique
∀[C:Type]. ∀[f:Form(C)]. ∀[b:𝔹].  ((↑(wfFormAux(f) b)) ⇒ termForm(f) = b)

Definition: FormFvs
FormFvs(f) ==
  Form_ind(f;
           FormVar(v)⇒ [v];
           FormConst(c)⇒ [];
           FormSet(x,phi)⇒ fvsphi.filter(λv.(¬bv =a x);fvsphi);
           FormEqual(t1,t2)⇒ fvs1,fvs2.fvs1 ⋃ fvs2;
           FormMember(t1,t2)⇒ fvs1,fvs2.fvs1 ⋃ fvs2;
           FormAnd(a,b)⇒ fvsa,fvsb.fvsa ⋃ fvsb;
           FormOr(a,b)⇒ fvsa,fvsb.fvsa ⋃ fvsb;
           FormNot(a)⇒ fvsa.fvsa;
           FormAll(x,phi)⇒ fvsphi.filter(λv.(¬bv =a x);fvsphi);
           FormExists(x,phi)⇒ fvsphi.filter(λv.(¬bv =a x);fvsphi)) 

Lemma: FormFvs_wf
∀[c:Type]. ∀[f:Form(c)].  (FormFvs(f) ∈ Atom List)

Definition: FormSafe1
FormSafe1(f) ==
  Form_ind(f;
           FormVar(v)⇒ λvs.False;
           FormConst(c)⇒ λvs.False;
           FormSet(x,phi)⇒ r.λvs.False;
           FormEqual(a,b)⇒ ra,rb.λvs.((↑null(vs))
                                      ∨ (∃x:Atom
                                          (set-equal(Atom;vs;[x])
                                          ∧ (((↑FormVar?(a)) ∧ (FormVar-name(a) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(b))))
                                            ∨ ((↑FormVar?(b)) ∧ (FormVar-name(b) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(a))))))));
           FormMember(a,b)⇒ ra,rb.λvs.((↑null(vs))
                                       ∨ (∃x:Atom
                                           (set-equal(Atom;vs;[x])
                                           ∧ (↑FormVar?(a))
                                           ∧ (FormVar-name(a) = x ∈ Atom)
                                           ∧ (((↑FormVar?(b)) ∧ (FormVar-name(b) = x ∈ Atom)) ∨ (¬(x ∈ FormFvs(b)))))));
           FormAnd(a,b)⇒ ra,rb.λvs.∃as,bs:Atom List
                                     (set-equal(Atom;vs;as @ bs)
                                     ∧ (ra as)
                                     ∧ (rb bs)
                                     ∧ (l_disjoint(Atom;as;FormFvs(b)) ∨ l_disjoint(Atom;bs;FormFvs(a))));
           FormOr(a,b)⇒ ra,rb.λvs.((ra vs) ∧ (rb vs));
           FormNot(a)⇒ ra.λvs.((↑null(vs)) ∧ (ra []));
           FormAll(x,phi)⇒ r.λvs.False;
           FormExists(x,phi)⇒ r.λvs.((¬(x ∈ vs)) ∧ (r [x / vs]))) 

Lemma: FormSafe1_wf
∀[C:Type]. ∀[f:Form(C)].  (FormSafe1(f) ∈ (Atom List) ⟶ ℙ)

Lemma: FormSafe1_functionality
∀C:Type. ∀phi:Form(C). ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ {(FormSafe1(phi) vs) ⇒ (FormSafe1(phi) ws)})

Lemma: FormSafe1-Fvs-subset
∀C:Type. ∀phi:Form(C). ∀vs:Atom List.  ((FormSafe1(phi) vs) ⇒ l_subset(Atom;vs;FormFvs(phi)))

Definition: PZF-safe
PZF-safe(phi;vs) ==  FormSafe1(phi) vs

Lemma: PZF-safe_wf
∀[C:Type]. ∀[phi:Form(C)]. ∀[vs:Atom List].  (PZF-safe(phi;vs) ∈ ℙ)

Lemma: PZF-safe_functionality
∀C:Type. ∀phi:Form(C). ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ {PZF-safe(phi;vs) ⇒ PZF-safe(phi;ws)})

Lemma: PZF-safe-Fvs-subset
∀C:Type. ∀phi:Form(C). ∀vs:Atom List.  (PZF-safe(phi;vs) ⇒ l_subset(Atom;vs;FormFvs(phi)))

Definition: FormSafe1'
FormSafe1'(f) ==
  Form_ind(f;
           FormVar(v)⇒ λvs.False;
           FormConst(c)⇒ λvs.False;
           FormSet(x,phi)⇒ r.λvs.False;
           FormEqual(a,b)⇒ ra,rb.λvs.((↑null(vs))
                                      ∨ (∃x:Atom
                                          (set-equal(Atom;vs;[x])
                                          ∧ (((↑FormVar?(a)) ∧ (FormVar-name(a) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(b))))
                                            ∨ ((↑FormVar?(b)) ∧ (FormVar-name(b) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(a))))))));
           FormMember(a,b)⇒ ra,rb.λvs.((↑null(vs))
                                       ∨ (∃x:Atom
                                           (set-equal(Atom;vs;[x])
                                           ∧ (↑FormVar?(a))
                                           ∧ (FormVar-name(a) = x ∈ Atom)
                                           ∧ (((↑FormVar?(b)) ∧ (FormVar-name(b) = x ∈ Atom)) ∨ (¬(x ∈ FormFvs(b)))))));
           FormAnd(a,b)⇒ ra,rb.λvs.((∃theta:Atom List
                                       (l_subset(Atom;theta;vs-FormFvs(b)) ∧ (ra theta) ∧ (rb vs-theta)))
                                    ∨ (∃phi:Atom List. (l_subset(Atom;phi;vs-FormFvs(a)) ∧ (ra vs-phi) ∧ (rb phi))));
           FormOr(a,b)⇒ ra,rb.λvs.((ra vs) ∧ (rb vs));
           FormNot(a)⇒ ra.λvs.((↑null(vs)) ∧ (ra []));
           FormAll(x,phi)⇒ r.λvs.False;
           FormExists(x,phi)⇒ r.λvs.((¬(x ∈ vs)) ∧ (r [x / vs]))) 

Lemma: FormSafe1'_wf
∀[C:Type]. ∀[f:Form(C)].  (FormSafe1'(f) ∈ (Atom List) ⟶ ℙ)

Lemma: FormSafe-iff-FormSafe1'
∀C:Type. ∀f:Form(C). ∀vs:Atom List.  (FormSafe1(f) vs ⇐⇒ FormSafe1'(f) vs)

Definition: FormSafe1''
FormSafe1''(f) ==
  Form_ind(f;
           FormVar(v)⇒ λvs.False;
           FormConst(c)⇒ λvs.False;
           FormSet(x,phi)⇒ r.λvs.False;
           FormEqual(a,b)⇒ ra,rb.λvs.((↑null(vs))
                                      ∨ (∃x:Atom
                                          (set-equal(Atom;vs;[x])
                                          ∧ (((↑FormVar?(a)) ∧ (FormVar-name(a) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(b))))
                                            ∨ ((↑FormVar?(b)) ∧ (FormVar-name(b) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(a))))))));
           FormMember(a,b)⇒ ra,rb.λvs.((↑null(vs))
                                       ∨ (∃x:Atom
                                           (set-equal(Atom;vs;[x])
                                           ∧ (↑FormVar?(a))
                                           ∧ (FormVar-name(a) = x ∈ Atom)
                                           ∧ (((↑FormVar?(b)) ∧ (FormVar-name(b) = x ∈ Atom)) ∨ (¬(x ∈ FormFvs(b)))))));
           FormAnd(a,b)⇒ ra,rb.λvs.(let theta = vs-FormFvs(b) in
                                         (ra theta) ∧ (rb vs-theta)
                                    ∨ let phi = vs-FormFvs(a) in
                                          (ra vs-phi) ∧ (rb phi));
           FormOr(a,b)⇒ ra,rb.λvs.((ra vs) ∧ (rb vs));
           FormNot(a)⇒ ra.λvs.((↑null(vs)) ∧ (ra []));
           FormAll(x,phi)⇒ r.λvs.False;
           FormExists(x,phi)⇒ r.λvs.((¬(x ∈ vs)) ∧ (r [x / vs]))) 

Lemma: FormSafe1''_wf
∀[C:Type]. ∀[f:Form(C)].  (FormSafe1''(f) ∈ (Atom List) ⟶ ℙ)

Lemma: FormSafe1'-iff-FormSafe1''
∀C:Type. ∀f:Form(C). ∀vs:Atom List.  (FormSafe1'(f) vs ⇐⇒ FormSafe1''(f) vs)

Lemma: FormSafe1-iff-FormSafe1''
∀C:Type. ∀f:Form(C). ∀vs:Atom List.  (FormSafe1(f) vs ⇐⇒ FormSafe1''(f) vs)

Definition: FormSafe2
FormSafe2(f) ==
  Form_ind(f;
           FormVar(v)⇒ λvs.ff;
           FormConst(c)⇒ λvs.ff;
           FormSet(x,phi)⇒ r.λvs.ff;
           FormEqual(a,b)⇒ ra,rb.λvs.(null(vs)
                                      ∨blet x = hd(vs) in
                                            null(vs-[x])
                                            ∧b ((FormVar?(a) ∧b FormVar-name(a) =a x ∧b (¬bx ∈b FormFvs(b)))
                                               ∨b(FormVar?(b) ∧b FormVar-name(b) =a x ∧b (¬bx ∈b FormFvs(a)))));
           FormMember(a,b)⇒ ra,rb.λvs.(null(vs)
                                       ∨blet x = hd(vs) in
                                             null(vs-[x])
                                             ∧b FormVar?(a)
                                             ∧b FormVar-name(a) =a x
                                             ∧b ((FormVar?(b) ∧b FormVar-name(b) =a x) ∨b(¬bx ∈b FormFvs(b))));
           FormAnd(a,b)⇒ ra,rb.λvs.eval as = FormFvs(a) in
                                    eval bs = FormFvs(b) in
                                      eval theta = vs-bs in
                                      (ra theta) ∧b (rb vs-theta)
                                      ∨beval phi = vs-as in
                                        (ra vs-phi) ∧b (rb phi);
           FormOr(a,b)⇒ ra,rb.λvs.((ra vs) ∧b (rb vs));
           FormNot(a)⇒ ra.λvs.(null(vs) ∧b (ra []));
           FormAll(x,phi)⇒ r.λvs.ff;
           FormExists(x,phi)⇒ r.λvs.((¬bx ∈b vs) ∧b (r [x / vs]))) 

Lemma: FormSafe2_wf
∀[C:Type]. ∀[f:Form(C)].  (FormSafe2(f) ∈ (Atom List) ⟶ 𝔹)

Definition: PZF_safe
PZF_safe(phi;vs) ==  FormSafe2(phi) vs

Lemma: PZF_safe_wf
∀[C:Type]. ∀[phi:Form(C)]. ∀[vs:Atom List].  (PZF_safe(phi;vs) ∈ 𝔹)

Lemma: PZF_safe_functionality
∀[C:Type]. ∀[phi:Form(C)]. ∀[vs,ws:Atom List].  PZF_safe(phi;vs) = PZF_safe(phi;ws) supposing set-equal(Atom;vs;ws)

Lemma: assert-PZF_safe
∀C:Type. ∀phi:Form(C). ∀vs:Atom List.  (↑PZF_safe(phi;vs) ⇐⇒ PZF-safe(phi;vs))

Lemma: PZF_safe_functionality_subset
∀[C:Type]. ∀[phi:Form(C)]. ∀[vs,ws:Atom List].
  (↑PZF_safe(phi;vs)) ⇒ (↑PZF_safe(phi;ws)) supposing l_subset(Atom;ws;vs)

Definition: SafeForm
SafeForm(f) ==
  Form_ind(f;
           FormVar(v)⇒ tt;
           FormConst(c)⇒ tt;
           FormSet(x,phi)⇒ r.r ∧b PZF_safe(phi;[x]);
           FormEqual(l,r)⇒ r1,r2.r1 ∧b r2;
           FormMember(e,s)⇒ r1,r2.r1 ∧b r2;
           FormAnd(l,r)⇒ r1,r2.r1 ∧b r2;
           FormOr(l,r)⇒ r1,r2.r1 ∧b r2;
           FormNot(b)⇒ r1.r1;
           FormAll(x,b)⇒ r1.r1;
           FormExists(x,b)⇒ r1.r1) 

Lemma: SafeForm_wf
∀[C:Type]. ∀[f:Form(C)].  (SafeForm(f) ∈ 𝔹)

Definition: PZF-Form
PZF-Form(C) ==  {f:Form(C)| (↑wfForm(f)) ∧ (↑SafeForm(f))} 

Lemma: PZF-Form_wf
∀[C:Type]. (PZF-Form(C) ∈ Type)

Definition: PZF-Term
PZF-Term(C) ==  {f:PZF-Form(C)| ↑termForm(f)} 

Lemma: PZF-Term_wf
∀[C:Type]. (PZF-Term(C) ∈ Type)

Definition: PZF-Formula
PZF-Formula(C) ==  {f:PZF-Form(C)| ¬↑termForm(f)} 

Lemma: PZF-Formula_wf
∀[C:Type]. (PZF-Formula(C) ∈ Type)

Lemma: FormSet_wf2
∀[C:Type]. ∀[x:Atom]. ∀[phi:PZF-Formula(C)].  {x | phi} ∈ PZF-Term(C) supposing PZF-safe(phi;[x])

Lemma: FormEqual_wf2
∀[C:Type]. ∀[a,b:PZF-Term(C)].  (a = b ∈ PZF-Formula(C))

Lemma: FormMember_wf2
∀[C:Type]. ∀[a,b:PZF-Term(C)].  (a ∈ b ∈ PZF-Formula(C))

Lemma: FormAnd_wf2
∀[C:Type]. ∀[a,b:PZF-Formula(C)].  (a ∧ b) ∈ PZF-Formula(C))

Lemma: FormOr_wf2
∀[C:Type]. ∀[a,b:PZF-Formula(C)].  (a ∨ b ∈ PZF-Formula(C))

Lemma: FormNot_wf2
∀[C:Type]. ∀[a:PZF-Formula(C)].  (¬(a) ∈ PZF-Formula(C))

Lemma: FormAll_wf2
∀[C:Type]. ∀[a:PZF-Formula(C)]. ∀[x:Atom].  (∀x. a ∈ PZF-Formula(C))

Lemma: FormExists_wf2
∀[C:Type]. ∀[a:PZF-Formula(C)]. ∀[x:Atom].  (∃x. a ∈ PZF-Formula(C))

Lemma: PZF-induction
∀C:Type
  ∀[F:PZF-Formula(C) ⟶ ℙ]. ∀[T:PZF-Term(C) ⟶ ℙ].
    ((∀name:Atom. T[Vname])
    ⇒ (∀value:C. T[Const(value)])
    ⇒ (∀x:Atom. ∀phi:PZF-Formula(C).  (F[phi] ⇒ PZF-safe(phi;[x]) ⇒ T[{x | phi}]))
    ⇒ (∀a,b:PZF-Term(C).  (T[a] ⇒ T[b] ⇒ F[a = b]))
    ⇒ (∀a,b:PZF-Term(C).  (T[a] ⇒ T[b] ⇒ F[a ∈ b]))
    ⇒ (∀a,b:PZF-Formula(C).  (F[a] ⇒ F[b] ⇒ F[a ∧ b)]))
    ⇒ (∀a,b:PZF-Formula(C).  (F[a] ⇒ F[b] ⇒ F[a ∨ b]))
    ⇒ (∀a:PZF-Formula(C). (F[a] ⇒ F[¬(a)]))
    ⇒ (∀a:PZF-Formula(C). ∀x:Atom.  (F[a] ⇒ F[∀x. a]))
    ⇒ (∀a:PZF-Formula(C). ∀x:Atom.  (F[a] ⇒ F[∃x. a]))
    ⇒ ((∀phi:PZF-Formula(C). F[phi]) ∧ (∀t:PZF-Term(C). T[t])))

Definition: validForm
validForm(f) ==  wfForm(f) ∧b SafeForm(f)

Lemma: validForm_wf
∀[C:Type]. ∀[f:Form(C)].  (validForm(f) ∈ 𝔹)



Home Index