`step coordinate word` for every coordinate this role owns and every word.
384def dpoEachOwned =
385 (lambda unrestricted k : Nat .
386 (lambda unrestricted owners : Nat .
387 (lambda unrestricted role : Nat .
388 (lambda unrestricted q : Nat .
389 (lambda unrestricted step : (pi unrestricted coordinate : Nat . (pi unrestricted word : Nat . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)))) .
390 (lambda unrestricted tail : (family NativePhysicalCommands) .
391 (dpEach
392 k
393 (lambda unrestricted coordinate : Nat .
394 (lambda unrestricted rest : (family NativePhysicalCommands) .
395 (nat-eliminate
396 (lambda unrestricted owned : Nat . (family NativePhysicalCommands))
397 rest
398 (lambda unrestricted previous : Nat .
399 (lambda unrestricted ignored : (family NativePhysicalCommands) .
400 (dpEach q (step coordinate) rest)))
401 (dpoOwns owners role coordinate))))
402 tail)))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.