Nuprl 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 
Proof
Definitions occuring in Statement : 
FOLRule: FOLRule()
, 
nat: ℕ
, 
ifthenelse: if b then t else f fi 
, 
eq_atom: x =a y
, 
bool: 𝔹
, 
ext-eq: A ≡ B
, 
unit: Unit
, 
product: x:A × B[x]
, 
int: ℤ
, 
token: "$token"
, 
atom: Atom
, 
void: Void
Definitions unfolded in proof : 
FOLRule: FOLRule()
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
uimplies: b supposing a
Lemmas referenced : 
ext-eq_weakening, 
FOLRule_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
cut, 
lemma_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
hypothesis, 
because_Cache, 
independent_isectElimination
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 
Date html generated:
2016_05_15-PM-10_22_08
Last ObjectModification:
2015_12_27-PM-06_29_25
Theory : minimal-first-order-logic
Home
Index