Nuprl Definition : eq_var

eq_var(a;b) ==
  if a is an atom then if b is an atom then a =a b otherwise ff otherwise let x,n = a 
                                                                          in if b is an atom then ff
                                                                             otherwise let y,m = b 
                                                                                       in x =a y ∧b (n =z m)


Definitions occuring in Statement :  band: p ∧b q,  eq_atom: x =a y,  eq_int: (i =z j),  bfalse: ff,  isatom: if z is an atom then a otherwise b,  spread: spread def
Definitions occuring in definition :  isatom: if z is an atom then a otherwise b,  bfalse: ff,  spread: spread def,  band: p ∧b q,  eq_atom: x =a y,  eq_int: (i =z j)
FDL editor aliases :  eq_var
Latex:
eq\_var(a;b)  ==
    if  a  is  an  atom  then  if  b  is  an  atom  then  a  =a  b  otherwise  ff
    otherwise  let  x,n  =  a 
                        in  if  b  is  an  atom  then  ff  otherwise  let  y,m  =  b 
                                                                                                  in  x  =a  y  \mwedge{}\msubb{}  (n  =\msubz{}  m)


Date html generated: 2020_05_19-PM-09_52_58
Last ObjectModification: 2020_03_09-PM-04_07_56

Theory : terms


Home Index