Nuprl Definition : append_rel

append_rel(T;L1;L2;L) ==  (L1 @ L2) = L ∈ (T List)



Definitions occuring in Statement :  append: as @ bs,  list: T List,  equal: s = t ∈ T
Definitions occuring in definition :  equal: s = t ∈ T,  list: T List,  append: as @ bs
FDL editor aliases :  append_rel

Latex:
append\_rel(T;L1;L2;L)  ==    (L1  @  L2)  =  L



Date html generated: 2016_05_15-PM-01_54_52
Last ObjectModification: 2015_09_23-AM-07_37_26

Theory : list!


Home Index