The swaps of the flow signature

add is the swappable operation (Swap): add(a, b) consumes a, and add(b, a) consumes b. It commutes with log-weight 0, so the flow model is lawful for the front end.

def RoleFlow.Flow.isAdd {as bs : List FS} : FOp as bs → Bool

add (not sub).

Equations

• RoleFlow.Flow.isAdd (RoleFlow.Flow.FOp.add n) = true
• RoleFlow.Flow.isAdd x✝ = false

@[implicit_reducible]

instance RoleFlow.Flow.instSwapFSFlowSig : Swap flowSig

Equations

• One or more equations did not get rendered due to their size.

theorem RoleFlow.Flow.swapLawful : Swap.Lawful flowModel.toModel

add commutes, and its log-weight is 0.