def rest_room

stelliferous@0.0.2.0 · proofs/traversal_lanes_refinement.bend:191

import Base
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order

191def rest_room(+start: Nat,+rest: Nat,+capacity: Nat,room: {Nat.is_le(Nat.add(start,8n+rest),capacity) == True{} : Bool}) ->
192  {Nat.is_le(Nat.add(8n+start,rest),capacity) == True{} : Bool}:
193  Order.advance_room(7n+start,rest,capacity,Order.advance_room(6n+start,1n+rest,capacity,Order.advance_room(5n+start,2n+rest,capacity,
194    Order.advance_room(4n+start,3n+rest,capacity,Order.advance_room(3n+start,4n+rest,capacity,Order.advance_room(2n+start,5n+rest,capacity,
195      Order.advance_room(1n+start,6n+rest,capacity,Order.advance_room(start,7n+rest,capacity,room))))))))