~/bend-docscommunity

proofs/lib/sequence.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/lib/sequence.bend as Sequence

6 imports
import Base
import ./logic.bend as L
import ./nat.bend as N
import ./list.bend as LL
import ../../spec/lib/common.bend as SC
import ../../spec/lib/sequence.bend as Q

Definitions

def succ_sub_one source · line 14 · raw

@+n:Nat -> {Nat.sub(1n+n, 1n) == n : Nat}

def add_one source · line 18 · raw

@+i:Nat -> {Nat.add(i, 1n) == 1n+i : Nat}

def re_snoc source · line 23 · raw

@-A:Data -> @+xs:List<&2, A> -> @+x:A -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, xs, i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(A, xs, x), i) : Maybe<&2, A>}

def snoc_prefix source · line 32 · raw

@-A:Data -> @+xs:List<&2, A> -> @+x:A -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/sequence.EqualPrefix(A, xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(A, xs, x))

def snoc_last source · line 36 · raw

@-A:Data -> @+xs:List<&2, A> -> @+x:A -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(A, xs, x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs)) == Some{x} : Maybe<&2, A>}

def snoc_length source · line 43 · raw

@-A:Data -> @+xs:List<&2, A> -> @+x:A -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(A, xs, x)) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs) : Nat}

def snoc_last_elem source · line 47 · raw

@-A:Data -> @+xs:List<&2, A> -> @+x:A -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/sequence.last_elem(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(A, xs, x)) == Some{x} : Maybe<&2, A>}

Last_Element after Append is the new item

def cons_shift_at source · line 54 · raw

@-A:Data -> @+xs:List<&2, A> -> @+x:A -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, xs, i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, x <> xs, Nat.add(i, 1n)) : Maybe<&2, A>}

def cons_shifted source · line 58 · raw

@-A:Data -> @+xs:List<&2, A> -> @+x:A -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/sequence.RangeShifted(A, xs, x <> xs, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs), 1n)

def cons_first source · line 61 · raw

@-A:Data -> @+xs:List<&2, A> -> @+x:A -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, x <> xs, 0n) == Some{x} : Maybe<&2, A>}

def cons_length source · line 64 · raw

@-A:Data -> @+xs:List<&2, A> -> @+x:A -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, x <> xs) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs) : Nat}

def tail_shifted source · line 70 · raw

@-A:Data -> @+h:A -> @+t:List<&2, A> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/sequence.RangeShifted(A, t, h <> t, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, t), 1n)

def first_elem source · line 74 · raw

@-A:Data -> @+xs:List<&2, A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.head(A, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, xs, 0n) : Maybe<&2, A>}

First_Element is Element (Model, First_Index)

def re_init source · line 83 · raw

@-A:Data -> @+t:List<&2, A> -> @+h:A -> @+i:Nat -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(A, h <> t))) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(A, h <> t), i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, h <> t, i) : Maybe<&2, A>}

def init_length source · line 92 · raw

@-A:Data -> @+t:List<&2, A> -> @+h:A -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(A, h <> t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, t) : Nat}

def init_prefix source · line 99 · raw

@-A:Data -> @+t:List<&2, A> -> @+h:A -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/sequence.EqualPrefix(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(A, h <> t), h <> t)

def last_is_elem source · line 103 · raw

@-A:Data -> @+t:List<&2, A> -> @+h:A -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.last(A, h <> t) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/sequence.last_elem(A, h <> t) : Maybe<&2, A>}

def update_except source · line 113 · raw

@-A:Data -> @+xs:List<&2, A> -> @+i:Nat -> @+v:A -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/sequence.EqualExcept(A, xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(A, xs, i, v), i)

def update_at source · line 116 · raw

@-A:Data -> @+xs:List<&2, A> -> @+i:Nat -> @+v:A -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(A, xs, i, v), i) == Some{v} : Maybe<&2, A>}

def update_length source · line 119 · raw

@-A:Data -> @+xs:List<&2, A> -> @+i:Nat -> @+v:A -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(A, xs, i, v)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs) : Nat}

def same_prefix source · line 124 · raw

@-A:Data -> @+xs:List<&2, A> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/sequence.EqualPrefix(A, xs, xs)

def mid_equal source · line 132 · raw

@-A:Data -> @+a:List<&2, A> -> @+c:List<&2, A> -> @+n:A -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/sequence.RangeEqual(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(A, a, c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(A, a, n <> c), 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, a))

def mid_at source · line 135 · raw

@-A:Data -> @+a:List<&2, A> -> @+c:List<&2, A> -> @+n:A -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(A, a, n <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, a)) == Some{n} : Maybe<&2, A>}

def mid_shift_at source · line 140 · raw

@-A:Data -> @+a:List<&2, A> -> @+c:List<&2, A> -> @+n:A -> @+i:Nat -> @+h1:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, a), i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(A, a, c), i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(A, a, n <> c), Nat.add(i, 1n)) : Maybe<&2, A>}

def mid_shifted source · line 147 · raw

@-A:Data -> @+a:List<&2, A> -> @+c:List<&2, A> -> @+n:A -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/sequence.RangeShifted(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(A, a, c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(A, a, n <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(A, a, c)), 1n)

def mid_length source · line 150 · raw

@-A:Data -> @+a:List<&2, A> -> @+c:List<&2, A> -> @+n:A -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(A, a, n <> c)) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(A, a, c)) : Nat}