Nuprl Definition : iseg

l1 ≤ l2 ==  ∃l:T List. (l2 = (l1 @ l) ∈ (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 :  iseg
Latex:
l1  \mleq{}  l2  ==    \mexists{}l:T  List.  (l2  =  (l1  @  l))


Date html generated: 2016_05_14-PM-01_30_39
Last ObjectModification: 2015_09_22-PM-05_54_18

Theory : list_1


Home Index