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