Nuprl Definition : fseg

fseg(T;L1;L2) ==  ∃L:T List. (L2 = (L @ L1) ∈ (T List))


Definitions occuring in Statement :  append: as @ bs,  list: T List,  exists: ∃x:A. B[x],  equal: s = t ∈ T
Definitions occuring in definition :  exists: ∃x:A. B[x],  equal: s = t ∈ T,  list: T List,  append: as @ bs
FDL editor aliases :  fseg
Latex:
fseg(T;L1;L2)  ==    \mexists{}L:T  List.  (L2  =  (L  @  L1))


Date html generated: 2016_05_14-PM-01_34_57
Last ObjectModification: 2015_09_22-PM-05_54_23

Theory : list_1


Home Index