Nuprl Definition : mFOLRule

mFOLRule() ==
  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:ℕ × ℤ
             else Void
             fi 



Definitions occuring in Statement :  nat: ifthenelse: if then else fi  eq_atom: =a y bool: 𝔹 unit: Unit product: x:A × B[x] int: token: "$token" atom: Atom void: Void
FDL editor aliases :  mFOLRule
mFOLRule()  ==
    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{}
                          else  Void
                          fi 



Date html generated: 2015_07_17-AM-07_54_54
Last ObjectModification: 2014_05_04-PM-00_55_50

Home Index