---

Step * of Lemma formula_ind_wf

No Annotations
∀[A:Type]. ∀[R:A ⟶ formula() ⟶ ℙ]. ∀[v:formula()]. ∀[var:name:Atom ⟶ {x:A| R[x;pvar(name)]} ].
∀[not:sub:formula() ⟶ {x:A| R[x;sub]}  ⟶ {x:A| R[x;pnot(sub)]} ]. ∀[and:left:formula()
                                                                        ⟶ right:formula()
                                                                        ⟶ {x:A| R[x;left]} 
                                                                        ⟶ {x:A| R[x;right]} 
                                                                        ⟶ {x:A| R[x;pand(left;right)]} ].
∀[or:left:formula() ⟶ right:formula() ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;por(left;right)]} ].
∀[imp:left:formula() ⟶ right:formula() ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;pimp(left;right)]} ].
  (formula_ind(v;
               pvar(name)⇒ var[name];
               pnot(sub)⇒ rec1.not[sub;rec1];
               pand(left,right)⇒ rec2,rec3.and[left;right;rec2;rec3];
               por(left,right)⇒ rec4,rec5.or[left;right;rec4;rec5];
               pimp(left,right)⇒ rec6,rec7.imp[left;right;rec6;rec7])  ∈ {x:A| R[x;v]} )
BY
{ (ProveDatatypeIndWfByLemma formula-definition) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  formula()  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:formula()].  \mforall{}[var:name:Atom  {}\mrightarrow{}  \{x:A|  R[x;pvar(name)]\}  ].
\mforall{}[not:sub:formula()  {}\mrightarrow{}  \{x:A|  R[x;sub]\}    {}\mrightarrow{}  \{x:A|  R[x;pnot(sub)]\}  ].  \mforall{}[and:left:formula()
                                                                                                                                                {}\mrightarrow{}  right:formula()
                                                                                                                                                {}\mrightarrow{}  \{x:A|  R[x;left]\} 
                                                                                                                                                {}\mrightarrow{}  \{x:A|  R[x;right]\} 
                                                                                                                                                {}\mrightarrow{}  \{x:A| 
                                                                                                                                                        R[x;pand(left;right)]\}  ]\000C.
\mforall{}[or:left:formula()
          {}\mrightarrow{}  right:formula()
          {}\mrightarrow{}  \{x:A|  R[x;left]\} 
          {}\mrightarrow{}  \{x:A|  R[x;right]\} 
          {}\mrightarrow{}  \{x:A|  R[x;por(left;right)]\}  ].  \mforall{}[imp:left:formula()
                                                                                        {}\mrightarrow{}  right:formula()
                                                                                        {}\mrightarrow{}  \{x:A|  R[x;left]\} 
                                                                                        {}\mrightarrow{}  \{x:A|  R[x;right]\} 
                                                                                        {}\mrightarrow{}  \{x:A|  R[x;pimp(left;right)]\}  ].
    (formula\_ind(v;
                              pvar(name){}\mRightarrow{}  var[name];
                              pnot(sub){}\mRightarrow{}  rec1.not[sub;rec1];
                              pand(left,right){}\mRightarrow{}  rec2,rec3.and[left;right;rec2;rec3];
                              por(left,right){}\mRightarrow{}  rec4,rec5.or[left;right;rec4;rec5];
                              pimp(left,right){}\mRightarrow{}  rec6,rec7.imp[left;right;rec6;rec7])    \mmember{}  \{x:A|  R[x;v]\}  )


By

---

Latex:
(ProveDatatypeIndWfByLemma  formula-definition)

---

Home Index