---

Step * of Lemma FOLRule-ext

FOLRule() ≡ lbl:Atom × if lbl =a "andI" then Unit
                       if lbl =a "impI" then Unit
                       if lbl =a "allI" then ℤ
                       if lbl =a "existsI" then ℤ
                       if lbl =a "orI" then 𝔹
                       if lbl =a "hyp" then Unit
                       if lbl =a "andE" then ℕ
                       if lbl =a "orE" then ℕ
                       if lbl =a "impE" then ℕ
                       if lbl =a "allE" then hypnum:ℕ × ℤ
                       if lbl =a "existsE" then hypnum:ℕ × ℤ
                       if lbl =a "falseE" then ℕ
                       else Void
                       fi 
BY
{ ProveDatatypeExt }

---

Latex:

---

Latex:
FOLRule()  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "andI"  then  Unit
                                              if  lbl  =a  "impI"  then  Unit
                                              if  lbl  =a  "allI"  then  \mBbbZ{}
                                              if  lbl  =a  "existsI"  then  \mBbbZ{}
                                              if  lbl  =a  "orI"  then  \mBbbB{}
                                              if  lbl  =a  "hyp"  then  Unit
                                              if  lbl  =a  "andE"  then  \mBbbN{}
                                              if  lbl  =a  "orE"  then  \mBbbN{}
                                              if  lbl  =a  "impE"  then  \mBbbN{}
                                              if  lbl  =a  "allE"  then  hypnum:\mBbbN{}  \mtimes{}  \mBbbZ{}
                                              if  lbl  =a  "existsE"  then  hypnum:\mBbbN{}  \mtimes{}  \mBbbZ{}
                                              if  lbl  =a  "falseE"  then  \mBbbN{}
                                              else  Void
                                              fi 


By

---

Latex:
ProveDatatypeExt

---

Home Index