---

Step * of Lemma mFOLRule_ind_wf

∀[A:Type]. ∀[R:A ─→ mFOLRule() ─→ ℙ]. ∀[v:mFOLRule()]. ∀[andI:{x:A| R[x;andI]} ]. ∀[impI:{x:A| R[x;impI]} ].
∀[allI:var:ℤ ─→ {x:A| R[x;allI with var]} ]. ∀[existsI:var:ℤ ─→ {x:A| R[x;existsI with var]} ].
∀[orI:left:𝔹 ─→ {x:A| R[x;mRuleorI(left)]} ]. ∀[hyp:{x:A| R[x;hyp]} ]. ∀[andE:hypnum:ℕ ─→ {x:A| R[x;andE on hypnum]} ].
∀[orE:hypnum:ℕ ─→ {x:A| R[x;orE on hypnum]} ]. ∀[impE:hypnum:ℕ ─→ {x:A| R[x;impE on hypnum]} ].
∀[allE:hypnum:ℕ ─→ var:ℤ ─→ {x:A| R[x;allE on hypnum with var]} ]. ∀[existsE:hypnum:ℕ
                                                                            ─→ var:ℤ
                                                                            ─→ {x:A| R[x;existsE on hypnum with var]} ].
  (mFOLRule_ind(v;
   andI;
   impI;
   var.allI[var];
   var.existsI[var];
   left.orI[left];
   hyp;hypnum.andE[hypnum];
   hypnum.orE[hypnum];
   hypnum.impE[hypnum];
   hypnum,var.allE[hypnum;var];
   hypnum,var.existsE[hypnum;var]) ∈ {x:A| R[x;v]} )
BY
{ ProveDatatypeIndWf TERMOF{mFOLRule-definition:o, 1:l, i:l}⋅ }

---

Latex:


\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  mFOLRule()  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:mFOLRule()].  \mforall{}[andI:\{x:A|  R[x;andI]\}  ].  \mforall{}[impI:\{x:A| 
                                                                                                                                                                                  R
                                                                                                                                                                                  [x;impI]\}  ]\000C.
\mforall{}[allI:var:\mBbbZ{}  {}\mrightarrow{}  \{x:A|  R[x;allI  with  var]\}  ].  \mforall{}[existsI:var:\mBbbZ{}  {}\mrightarrow{}  \{x:A|  R[x;existsI  with  var]\}  ].
\mforall{}[orI:left:\mBbbB{}  {}\mrightarrow{}  \{x:A|  R[x;mRuleorI(left)]\}  ].  \mforall{}[hyp:\{x:A|  R[x;hyp]\}  ].
\mforall{}[andE:hypnum:\mBbbN{}  {}\mrightarrow{}  \{x:A|  R[x;andE  on  hypnum]\}  ].  \mforall{}[orE:hypnum:\mBbbN{}  {}\mrightarrow{}  \{x:A|  R[x;orE  on  hypnum]\}  ].
\mforall{}[impE:hypnum:\mBbbN{}  {}\mrightarrow{}  \{x:A|  R[x;impE  on  hypnum]\}  ].  \mforall{}[allE:hypnum:\mBbbN{}
                                                                                                              {}\mrightarrow{}  var:\mBbbZ{}
                                                                                                              {}\mrightarrow{}  \{x:A|  R[x;allE  on  hypnum  with  var]\}  ].
\mforall{}[existsE:hypnum:\mBbbN{}  {}\mrightarrow{}  var:\mBbbZ{}  {}\mrightarrow{}  \{x:A|  R[x;existsE  on  hypnum  with  var]\}  ].
    (mFOLRule\_ind(v;
      andI;
      impI;
      var.allI[var];
      var.existsI[var];
      left.orI[left];
      hyp;hypnum.andE[hypnum];
      hypnum.orE[hypnum];
      hypnum.impE[hypnum];
      hypnum,var.allE[hypnum;var];
      hypnum,var.existsE[hypnum;var])  \mmember{}  \{x:A|  R[x;v]\}  )


By

ProveDatatypeIndWf  TERMOF\{mFOLRule-definition:o,  1:l,  i:l\}\mcdot{}

---

Home Index