~/bend-docscommunity

general/rose/LAWS.bend open laws/TODOs

raw source on the hub · import 0x3ffc69d4b5da64782dbe50fda425aa0c/general/rose/LAWS.bend as LAWS

3 imports
import Base
import ./type.bend as R
import ./ops.bend as O

Laws

law first_key_is_own provedin general/rose/PROOF.bendsource · line 6 · raw

@-N:Data -> @+r:0x3ffc69d4b5da64782dbe50fda425aa0c/general/rose/type.Rose<N> -> {0x3ffc69d4b5da64782dbe50fda425aa0c/general/rose/ops.first(0x3ffc69d4b5da64782dbe50fda425aa0c/general/rose/ops.keys(N, [r])) == 0x3ffc69d4b5da64782dbe50fda425aa0c/general/rose/ops.key(N, r) : String}

LAW: a tree's first key is its own