Nuprl Definition : list_eq

list_eq(eq;as;bs) ==
  if null(as) then null(bs) else (¬bnull(bs)) ∧b let a,aa = as in let b,bb = bs in (eq a b) ∧b list_eq(eq;aa;bb) fi 


Definitions occuring in Statement :  null: null(as),  band: p ∧b q,  bnot: ¬bb,  ifthenelse: if b then t else f fi ,  apply: f a,  spread: spread def
Definitions occuring in definition :  ifthenelse: if b then t else f fi ,  bnot: ¬bb,  null: null(as),  spread: spread def,  band: p ∧b q,  apply: f a
FDL editor aliases :  list_eq
Latex:
list\_eq(eq;as;bs)  ==
    if  null(as)
    then  null(bs)
    else  (\mneg{}\msubb{}null(bs))  \mwedge{}\msubb{}  let  a,aa  =  as  in  let  b,bb  =  bs  in  (eq  a  b)  \mwedge{}\msubb{}  list\_eq(eq;aa;bb)
    fi 


Date html generated: 2018_05_21-PM-00_19_55
Last ObjectModification: 2018_02_08-PM-01_33_21

Theory : list_0


Home Index