---

Step * of Lemma mFOL_ind_wf

No Annotations
∀[A:Type]. ∀[R:A ⟶ mFOL() ⟶ ℙ]. ∀[v:mFOL()]. ∀[atomic:name:Atom ⟶ vars:(ℤ List) ⟶ {x:A| R[x;name(vars)]} ].
∀[connect:knd:Atom
          ⟶ left:mFOL()
          ⟶ right:mFOL()
          ⟶ {x:A| R[x;left]} 
          ⟶ {x:A| R[x;right]} 
          ⟶ {x:A| R[x;mFOconnect(knd;left;right)]} ]. ∀[quant:isall:𝔹
                                                              ⟶ var:ℤ
                                                              ⟶ body:mFOL()
                                                              ⟶ {x:A| R[x;body]} 
                                                              ⟶ {x:A| R[x;mFOquant(isall;var;body)]} ].
  (mFOL_ind(v;
            mFOatomic(name,vars)⇒ atomic[name;vars];
            mFOconnect(knd,left,right)⇒ rec1,rec2.connect[knd;left;right;rec1;rec2];
            mFOquant(isall,var,body)⇒ rec3.quant[isall;var;body;rec3])  ∈ {x:A| R[x;v]} )
BY
{ (ProveDatatypeIndWfByLemma mFOL-definition) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  mFOL()  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:mFOL()].  \mforall{}[atomic:name:Atom
                                                                                                                {}\mrightarrow{}  vars:(\mBbbZ{}  List)
                                                                                                                {}\mrightarrow{}  \{x:A|  R[x;name(vars)]\}  ].
\mforall{}[connect:knd:Atom
                    {}\mrightarrow{}  left:mFOL()
                    {}\mrightarrow{}  right:mFOL()
                    {}\mrightarrow{}  \{x:A|  R[x;left]\} 
                    {}\mrightarrow{}  \{x:A|  R[x;right]\} 
                    {}\mrightarrow{}  \{x:A|  R[x;mFOconnect(knd;left;right)]\}  ].  \mforall{}[quant:isall:\mBbbB{}
                                                                                                                            {}\mrightarrow{}  var:\mBbbZ{}
                                                                                                                            {}\mrightarrow{}  body:mFOL()
                                                                                                                            {}\mrightarrow{}  \{x:A|  R[x;body]\} 
                                                                                                                            {}\mrightarrow{}  \{x:A| 
                                                                                                                                    R[x;mFOquant(isall;var;body)]\}  ].
    (mFOL\_ind(v;
                        mFOatomic(name,vars){}\mRightarrow{}  atomic[name;vars];
                        mFOconnect(knd,left,right){}\mRightarrow{}  rec1,rec2.connect[knd;left;right;rec1;rec2];
                        mFOquant(isall,var,body){}\mRightarrow{}  rec3.quant[isall;var;body;rec3])    \mmember{}  \{x:A|  R[x;v]\}  )


By

---

Latex:
(ProveDatatypeIndWfByLemma  mFOL-definition)

---

Home Index