Nuprl Definition : exists_sublist

exists_sublist(L;P)
==r if null(L) then P [] else let a,as = L in exists_sublist(as;P) ∨bexists_sublist(as;λl.(P [a / l])) fi 
exists_sublist(L;P) ==
  fix((λexists_sublist,L,P. if null(L)
                           then P []
                           else let a,as = L 
                                in (exists_sublist as P) ∨b(exists_sublist as (λl.(P [a / l])))
                           fi )) 
  L 
  P


Definitions occuring in Statement :  null: null(as),  cons: [a / b],  nil: [],  bor: p ∨bq,  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def
Definitions occuring in definition :  fix: fix(F),  ifthenelse: if b then t else f fi ,  null: null(as),  nil: [],  spread: spread def,  bor: p ∨bq,  lambda: λx.A[x],  apply: f a,  cons: [a / b]
FDL editor aliases :  exists_sublist
Latex:
exists\_sublist(L;P)
==r  if  null(L)
        then  P  []
        else  let  a,as  =  L 
                  in  exists\_sublist(as;P)  \mvee{}\msubb{}exists\_sublist(as;\mlambda{}l.(P  [a  /  l]))
        fi 

Latex:
exists\_sublist(L;P)  ==
    fix((\mlambda{}exists$_{sublist}$,L,P.  if  null(L)
                                                    then  P  []
                                                    else  let  a,as  =  L 
                                                              in  (exists$_{sublist}$  as  P)  \mvee{}\msubb{}(exists$_\mbackslash{}\000Cff7bsublist}$  as  (\mlambda{}l.(P  [a  /  l])))
                                                    fi  )) 
    L 
    P


Date html generated: 2018_05_21-PM-00_33_35
Last ObjectModification: 2017_10_12-AM-10_00_57

Theory : list_1


Home Index