---

Step * of Lemma FOLRule_ind_wf

No Annotations
∀[A:Type]. ∀[R:A ⟶ FOLRule() ⟶ ℙ]. ∀[v:FOLRule()]. ∀[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;fRuleorI(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]} ].
∀[falseE:hypnum:ℕ ⟶ {x:A| R[x;falseE on hypnum]} ].
  (case(v)
   andI => andI
   impI => impI
   allI with var => allI[var]
   existsI with var => existsI[var]
   orI (left?left) => orI[left]
   hyp => hyp
   andE @hypnum => andE[hypnum]
   orE @hypnum => orE[hypnum]
   impE @hypnum => impE[hypnum]
   allE @hypnum with var => allE[hypnum;var]
   existsE @hypnum with var => existsE[hypnum;var]
   falseE @hypnum => falseE[hypnum] ∈ {x:A| R[x;v]} )
BY
{ (ProveDatatypeIndWfByLemma FOLRule-definition) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  FOLRule()  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:FOLRule()].  \mforall{}[andI:\{x:A|  R[x;andI]\}  ].  \mforall{}[impI:\{x:A| 
                                                                                                                                                                              R[x;impI]\}  ].
\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;fRuleorI(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]\}  ].
\mforall{}[falseE:hypnum:\mBbbN{}  {}\mrightarrow{}  \{x:A|  R[x;falseE  on  hypnum]\}  ].
    (case(v)
      andI  =>  andI
      impI  =>  impI
      allI  with  var  =>  allI[var]
      existsI  with  var  =>  existsI[var]
      orI  (left?left)  =>  orI[left]
      hyp  =>  hyp
      andE  @hypnum  =>  andE[hypnum]
      orE  @hypnum  =>  orE[hypnum]
      impE  @hypnum  =>  impE[hypnum]
      allE  @hypnum  with  var  =>  allE[hypnum;var]
      existsE  @hypnum  with  var  =>  existsE[hypnum;var]
      falseE  @hypnum  =>  falseE[hypnum]  \mmember{}  \{x:A|  R[x;v]\}  )


By

---

Latex:
(ProveDatatypeIndWfByLemma  FOLRule-definition)

---

Home Index