Nuprl Definition : sublist-rec

sublist-rec(T;l1;l2) ==
  fix((λsublist-rec,l1,l2. case l1 of 
                             [] => True 
                             a::as =>
                              case l2 of 
                                [] => False 
                                b::bs =>
                                 ((a = b ∈ T) ∧ (sublist-rec as bs)) ∨ (sublist-rec l1 bs) 
                             esac 
                          esac)) 
  l1 
  l2


Definitions occuring in Statement :  list_ind: list_ind,  or: P ∨ Q,  and: P ∧ Q,  false: False,  true: True,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  equal: s = t ∈ T
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  true: True,  list_ind: list_ind,  false: False,  or: P ∨ Q,  and: P ∧ Q,  equal: s = t ∈ T,  apply: f a
FDL editor aliases :  sublist-rec
Latex:
sublist-rec(T;l1;l2)  ==
    fix((\mlambda{}sublist-rec,l1,l2.  case  l1  of 
                                                          []  =>  True 
                                                          a::as  =>
                                                            case  l2  of 
                                                                []  =>  False 
                                                                b::bs  =>
                                                                  ((a  =  b)  \mwedge{}  (sublist-rec  as  bs))  \mvee{}  (sublist-rec  l1  bs) 
                                                          esac 
                                                    esac)) 
    l1 
    l2


Date html generated: 2016_05_15-PM-03_33_44
Last ObjectModification: 2015_09_23-AM-07_44_11

Theory : general


Home Index