Nuprl Definition : interleaving
interleaving(T;L1;L2;L) == (||L|| = (||L1|| + ||L2||) ∈ ℕ) ∧ disjoint_sublists(T;L1;L2;L)
Definitions occuring in Statement :
disjoint_sublists: disjoint_sublists(T;L1;L2;L),
length: ||as||,
nat: ℕ,
and: P ∧ Q,
add: n + m,
equal: s = t ∈ T
Definitions occuring in definition :
and: P ∧ Q,
equal: s = t ∈ T,
nat: ℕ,
add: n + m,
length: ||as||,
disjoint_sublists: disjoint_sublists(T;L1;L2;L)
FDL editor aliases :
interleaving
Latex:
interleaving(T;L1;L2;L) == (||L|| = (||L1|| + ||L2||)) \mwedge{} disjoint\_sublists(T;L1;L2;L)
Date html generated:
2016_05_15-PM-01_58_09
Last ObjectModification:
2015_09_23-AM-07_37_36
Theory : list!
Home
Index