LAWS.bend open laws/TODOs

raw source on the hub · import 0xc409b77d3230ca33374caf6b0993f0cb/LAWS.bend as LAWS

3 imports

import Base
import ./main.bend as B
import ./model.bend as M

Laws

law string_right provedin PROOF.bend
Also proved in bend-mathlib as string.append_nil: `import bend-mathlib@0.7.2.0/string.bend as MString`, then `MString.append_nil`.
source · line 6 · raw

@+s:String -> {String.append(s, "") == s : String}

Auxiliary string/list algebra, universal.

law string_assoc provedin PROOF.bend
Also proved in bend-mathlib as string.append_assoc: `import bend-mathlib@0.7.2.0/string.bend as MString`, then `MString.append_assoc`.
source · line 10 · raw

@+a:String -> @+b:String -> @+c:String -> {String.append(String.append(a, b), c) == String.append(a, String.append(b, c)) : String}

law flatten_join provedin PROOF.bendsource · line 16 · raw

@+a:List<&2, String> -> @+b:List<&2, String> -> {0xc409b77d3230ca33374caf6b0993f0cb/model.flatten(0xc409b77d3230ca33374caf6b0993f0cb/model.join(a, b)) == String.append(0xc409b77d3230ca33374caf6b0993f0cb/model.flatten(a), 0xc409b77d3230ca33374caf6b0993f0cb/model.flatten(b)) : String}

law emit_model provedin PROOF.bendsource · line 22 · raw

@+t:0xc409b77d3230ca33374caf6b0993f0cb/main.Builder -> @+suffix:String -> {0xc409b77d3230ca33374caf6b0993f0cb/main.emit(t, suffix) == String.append(0xc409b77d3230ca33374caf6b0993f0cb/model.flatten(0xc409b77d3230ca33374caf6b0993f0cb/model.chunks(t)), suffix) : String}

Universal refinement, including an arbitrary suffix.

law finish_model provedin PROOF.bendsource · line 27 · raw

@+t:0xc409b77d3230ca33374caf6b0993f0cb/main.Builder -> {0xc409b77d3230ca33374caf6b0993f0cb/main.finish(t) == 0xc409b77d3230ca33374caf6b0993f0cb/model.flatten(0xc409b77d3230ca33374caf6b0993f0cb/model.chunks(t)) : String}

law empty provedin PROOF.bendsource · line 31 · raw

{0xc409b77d3230ca33374caf6b0993f0cb/main.finish(0xc409b77d3230ca33374caf6b0993f0cb/main.empty) == "" : String}

law fragment provedin PROOF.bendsource · line 34 · raw

@+s:String -> {0xc409b77d3230ca33374caf6b0993f0cb/main.finish(0xc409b77d3230ca33374caf6b0993f0cb/main.fragment(s)) == s : String}

law compose provedin PROOF.bendsource · line 38 · raw

@+a:0xc409b77d3230ca33374caf6b0993f0cb/main.Builder -> @+b:0xc409b77d3230ca33374caf6b0993f0cb/main.Builder -> {0xc409b77d3230ca33374caf6b0993f0cb/main.finish(0xc409b77d3230ca33374caf6b0993f0cb/main.compose(a, b)) == String.append(0xc409b77d3230ca33374caf6b0993f0cb/main.finish(a), 0xc409b77d3230ca33374caf6b0993f0cb/main.finish(b)) : String}

law append provedin PROOF.bendsource · line 43 · raw

@+a:0xc409b77d3230ca33374caf6b0993f0cb/main.Builder -> @+s:String -> {0xc409b77d3230ca33374caf6b0993f0cb/main.finish(0xc409b77d3230ca33374caf6b0993f0cb/main.append(a, s)) == String.append(0xc409b77d3230ca33374caf6b0993f0cb/main.finish(a), s) : String}

law character provedin PROOF.bendsource · line 48 · raw

@+a:0xc409b77d3230ca33374caf6b0993f0cb/main.Builder -> @+c:Char -> {0xc409b77d3230ca33374caf6b0993f0cb/main.finish(0xc409b77d3230ca33374caf6b0993f0cb/main.character(a, c)) == String.append(0xc409b77d3230ca33374caf6b0993f0cb/main.finish(a), SCon{c, ""}) : String}

law left_identity provedin PROOF.bendsource · line 53 · raw

@+a:0xc409b77d3230ca33374caf6b0993f0cb/main.Builder -> {0xc409b77d3230ca33374caf6b0993f0cb/main.finish(0xc409b77d3230ca33374caf6b0993f0cb/main.compose(0xc409b77d3230ca33374caf6b0993f0cb/main.empty, a)) == 0xc409b77d3230ca33374caf6b0993f0cb/main.finish(a) : String}

law right_identity provedin PROOF.bendsource · line 57 · raw

@+a:0xc409b77d3230ca33374caf6b0993f0cb/main.Builder -> {0xc409b77d3230ca33374caf6b0993f0cb/main.finish(0xc409b77d3230ca33374caf6b0993f0cb/main.compose(a, 0xc409b77d3230ca33374caf6b0993f0cb/main.empty)) == 0xc409b77d3230ca33374caf6b0993f0cb/main.finish(a) : String}

law associativity provedin PROOF.bendsource · line 61 · raw

@+a:0xc409b77d3230ca33374caf6b0993f0cb/main.Builder -> @+b:0xc409b77d3230ca33374caf6b0993f0cb/main.Builder -> @+c:0xc409b77d3230ca33374caf6b0993f0cb/main.Builder -> {0xc409b77d3230ca33374caf6b0993f0cb/main.finish(0xc409b77d3230ca33374caf6b0993f0cb/main.compose(0xc409b77d3230ca33374caf6b0993f0cb/main.compose(a, b), c)) == 0xc409b77d3230ca33374caf6b0993f0cb/main.finish(0xc409b77d3230ca33374caf6b0993f0cb/main.compose(a, 0xc409b77d3230ca33374caf6b0993f0cb/main.compose(b, c))) : String}

law empty_fragment provedin PROOF.bendsource · line 67 · raw

@+a:0xc409b77d3230ca33374caf6b0993f0cb/main.Builder -> {0xc409b77d3230ca33374caf6b0993f0cb/main.finish(0xc409b77d3230ca33374caf6b0993f0cb/main.append(a, "")) == 0xc409b77d3230ca33374caf6b0993f0cb/main.finish(a) : String}

law snapshot provedin PROOF.bendsource · line 72 · raw

@+a:0xc409b77d3230ca33374caf6b0993f0cb/main.Builder -> @+s:String -> {(0xc409b77d3230ca33374caf6b0993f0cb/main.finish(a), 0xc409b77d3230ca33374caf6b0993f0cb/main.finish(0xc409b77d3230ca33374caf6b0993f0cb/main.append(a, s))) == (0xc409b77d3230ca33374caf6b0993f0cb/model.flatten(0xc409b77d3230ca33374caf6b0993f0cb/model.chunks(a)), String.append(0xc409b77d3230ca33374caf6b0993f0cb/model.flatten(0xc409b77d3230ca33374caf6b0993f0cb/model.chunks(a)), s)) : Pair(String, String)}

Both old and new observations, not merely old == old.

law witness provedin PROOF.bendsource · line 79 · raw

{0xc409b77d3230ca33374caf6b0993f0cb/main.finish(0xc409b77d3230ca33374caf6b0993f0cb/main.character(0xc409b77d3230ca33374caf6b0993f0cb/main.compose(0xc409b77d3230ca33374caf6b0993f0cb/main.append(0xc409b77d3230ca33374caf6b0993f0cb/main.fragment("λ"), ""), 0xc409b77d3230ca33374caf6b0993f0cb/main.fragment("🙂\r\n")), '\0')) == "λ🙂\r\n\0" : String}

Inhabited normalization witness: empty, nonempty, Unicode, LF, CR, NUL.