---

Step * of Lemma Form_ind_wf

No Annotations
∀[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]} )
BY
{ (ProveDatatypeIndWfByLemma Form-definition) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C,A:Type].  \mforall{}[R:A  {}\mrightarrow{}  Form(C)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:Form(C)].  \mforall{}[Var:name:Atom  {}\mrightarrow{}  \{x:A|  R[x;Vname]\}  ].
\mforall{}[Const:value:C  {}\mrightarrow{}  \{x:A|  R[x;Const(value)]\}  ].  \mforall{}[Set:var:Atom
                                                                                                        {}\mrightarrow{}  phi:Form(C)
                                                                                                        {}\mrightarrow{}  \{x:A|  R[x;phi]\} 
                                                                                                        {}\mrightarrow{}  \{x:A|  R[x;\{var  |  phi\}]\}  ].
\mforall{}[Equal:left:Form(C)
                {}\mrightarrow{}  right:Form(C)
                {}\mrightarrow{}  \{x:A|  R[x;left]\} 
                {}\mrightarrow{}  \{x:A|  R[x;right]\} 
                {}\mrightarrow{}  \{x:A|  R[x;left  =  right]\}  ].  \mforall{}[Member:element:Form(C)
                                                                                              {}\mrightarrow{}  set:Form(C)
                                                                                              {}\mrightarrow{}  \{x:A|  R[x;element]\} 
                                                                                              {}\mrightarrow{}  \{x:A|  R[x;set]\} 
                                                                                              {}\mrightarrow{}  \{x:A|  R[x;element  \mmember{}  set]\}  ].
\mforall{}[And:left:Form(C)
            {}\mrightarrow{}  right:Form(C)
            {}\mrightarrow{}  \{x:A|  R[x;left]\} 
            {}\mrightarrow{}  \{x:A|  R[x;right]\} 
            {}\mrightarrow{}  \{x:A|  R[x;left  \mwedge{}  right)]\}  ].  \mforall{}[Or:left:Form(C)
                                                                                    {}\mrightarrow{}  right:Form(C)
                                                                                    {}\mrightarrow{}  \{x:A|  R[x;left]\} 
                                                                                    {}\mrightarrow{}  \{x:A|  R[x;right]\} 
                                                                                    {}\mrightarrow{}  \{x:A|  R[x;left  \mvee{}  right]\}  ].  \mforall{}[Not:body:Form(C)
                                                                                                                                                            {}\mrightarrow{}  \{x:A|  R[x;body]\} 
                                                                                                                                                            {}\mrightarrow{}  \{x:A| 
                                                                                                                                                                    R[x;\mneg{}(body)]\}  ].
\mforall{}[All:var:Atom  {}\mrightarrow{}  body:Form(C)  {}\mrightarrow{}  \{x:A|  R[x;body]\}    {}\mrightarrow{}  \{x:A|  R[x;\mforall{}var.  body]\}  ].
\mforall{}[Exists:var:Atom  {}\mrightarrow{}  body:Form(C)  {}\mrightarrow{}  \{x:A|  R[x;body]\}    {}\mrightarrow{}  \{x:A|  R[x;\mexists{}var.  body]\}  ].
    (Form\_ind(v;
                        FormVar(name){}\mRightarrow{}  Var[name];
                        FormConst(value){}\mRightarrow{}  Const[value];
                        FormSet(var,phi){}\mRightarrow{}  rec1.Set[var;phi;rec1];
                        FormEqual(left,right){}\mRightarrow{}  rec2,rec3.Equal[left;right;rec2;rec3];
                        FormMember(element,set){}\mRightarrow{}  rec4,rec5.Member[element;set;rec4;rec5];
                        FormAnd(left,right){}\mRightarrow{}  rec6,rec7.And[left;right;rec6;rec7];
                        FormOr(left,right){}\mRightarrow{}  rec8,rec9.Or[left;right;rec8;rec9];
                        FormNot(body){}\mRightarrow{}  rec10.Not[body;rec10];
                        FormAll(var,body){}\mRightarrow{}  rec11.All[var;body;rec11];
                        FormExists(var,body){}\mRightarrow{}  rec12.Exists[var;body;rec12])    \mmember{}  \{x:A|  R[x;v]\}  )


By

---

Latex:
(ProveDatatypeIndWfByLemma  Form-definition)

---

Home Index