Nuprl Definition : mFOLRule

Nuprl Definition : mFOLRule_ind

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]) ==
  let lbl,v1 = v
  in if lbl="andI" then andI
     if lbl="impI" then impI
     if lbl="allI" then allI[v1]
     if lbl="existsI" then existsI[v1]
     if lbl="orI" then orI[v1]
     if lbl="hyp" then hyp
     if lbl="andE" then andE[v1]
     if lbl="orE" then orE[v1]
     if lbl="impE" then impE[v1]
     if lbl="allE" then let hypnum,v2 = v1 in allE[hypnum; v2]
     if lbl="existsE" then let hypnum,v2 = v1 in existsE[hypnum; v2]
     else ⊥
     fi

Definitions occuring in Statement : bottom: ⊥, atom_eq: if a=b then c else d fi , spread: spread def, token: "$token"
FDL editor aliases : mFOLRule_ind mFOLRule_ind
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]) == let lbl,v1 = v in if lbl="andI" then andI if lbl="impI" then impI if lbl="allI" then allI[v1] if lbl="existsI" then existsI[v1] if lbl="orI" then orI[v1] if lbl="hyp" then hyp if lbl="andE" then andE[v1] if lbl="orE" then orE[v1] if lbl="impE" then impE[v1] if lbl="allE" then let hypnum,v2 = v1 in allE[hypnum; v2] if lbl="existsE" then let hypnum,v2 = v1 in existsE[hypnum; v2] else \mbot{} fi Date html generated: 2015_07_17-AM-07_56_17 Last ObjectModification: 2014_05_04-PM-01_01_49 Home Index