GenAutomata
Sections
NuprlLIB
Doc
Def
interleaving_occurence(T;L1;L2;L;f1;f2) == ||L|| = ||L1||+||L2||
& increasing(f1;||L1||) & (
j:
||L1||. L1[j] = L[(f1(j))]
T) & increasing(f2;||L2||) & (
j:
||L2||. L2[j] = L[(f2(j))]
T) & (
j1:
||L1||, j2:
||L2||.
f1(j1) = f2(j2)
)
is mentioned
In prior sections:
mb
list
1
GenAutomata
Sections
NuprlLIB
Doc
& increasing(f1;||L1||) & (
j:||L1||. L1[j] = L[(f1(j))] T) & increasing(f2;||L2||) & (j:||L2||. L2[j] = L[(f2(j))] T) & (j1:||L1||, j2:||L2||. 
f1(j1) = f2(j2) 
)