Nuprl Definition : eq_list

as =b bs ==
  Y 
  (λeq_list,as,bs. case as of 
                     [] => null(bs) 
                     a::as' =>
                      case bs of [] => ff | b::bs' => (a (=b) b) ∧b (eq_list as' bs') esac 
                  esac) 
  as 
  bs


Definitions occuring in Statement :  null: null(as),  list_ind: list_ind,  band: p ∧b q,  bfalse: ff,  infix_ap: x f y,  ycomb: Y,  apply: f a,  lambda: λx.A[x],  set_eq: =b
Definitions occuring in definition :  ycomb: Y,  lambda: λx.A[x],  null: null(as),  list_ind: list_ind,  bfalse: ff,  band: p ∧b q,  infix_ap: x f y,  set_eq: =b,  apply: f a
Latex:
as  =\msubb{}  bs  ==
    Y 
    (\mlambda{}eq$_{list}$,as,bs.  case  as  of 
                                        []  =>  null(bs) 
                                        a::as'  =>
                                          case  bs  of  []  =>  ff  |  b::bs'  =>  (a  (=\msubb{})  b)  \mwedge{}\msubb{}  (eq$_{list}$  \000Cas'  bs')  esac 
                                  esac) 
    as 
    bs


Date html generated: 2016_05_16-AM-07_34_49
Last ObjectModification: 2015_09_23-AM-09_51_28

Theory : list_2


Home Index