~/bend-docscommunity

proofs/lib/nat_list.bend checks

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

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

Definitions

def memn source · line 12 · raw

@+s:Nat -> @xs:List<&2, Nat> -> Bool

stated in spec/lib/common.bend

def nodupn source · line 15 · raw

@xs:List<&2, Nat> -> Bool

def or_assoc source · line 22 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> {Bool.or(a, Bool.or(b, c)) == Bool.or(Bool.or(a, b), c) : Bool}

def or_comm source · line 29 · raw

@+a:Bool -> @+b:Bool -> {Bool.or(a, b) == Bool.or(b, a) : Bool}

def and_assoc source · line 40 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> {Bool.and(a, Bool.and(b, c)) == Bool.and(Bool.and(a, b), c) : Bool}

def and_comm source · line 47 · raw

@+a:Bool -> @+b:Bool -> {Bool.and(a, b) == Bool.and(b, a) : Bool}

def bt_mid source · line 58 · raw

@+x:Bool -> @+y:Bool -> @+z:Bool -> @+w:Bool -> {Bool.and(Bool.not(Bool.or(x, y)), Bool.and(z, Bool.not(w))) == Bool.and(Bool.and(Bool.not(x), z), Bool.not(Bool.or(y, w))) : Bool}

def is_eq_sym source · line 70 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_eq(a, b) == Nat.is_eq(b, a) : Bool}

def memn_app source · line 81 · raw

@+x:Nat -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> {memn(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == Bool.or(memn(x, a), memn(x, b)) : Bool}

def memn_mid source · line 88 · raw

@+x:Nat -> @+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> {memn(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)) == Bool.or(memn(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)), Nat.is_eq(s, x)) : Bool}

def nd_mid source · line 95 · raw

@+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> {nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)) == Bool.and(nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)), Bool.not(memn(s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)))) : Bool}

def not_t_f source · line 109 · raw

@+b:Bool -> @+h:{Bool.not(b) == True{} : Bool} -> {b == False{} : Bool}

def or_f_l source · line 112 · raw

@+a:Bool -> @+b:Bool -> @+h:{Bool.or(a, b) == False{} : Bool} -> {a == False{} : Bool}

def nd_r source · line 119 · raw

@+a:List<&2, Nat> -> @+x:List<&2, Nat> -> @+h:{nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, x)) == True{} : Bool} -> {nodupn(x) == True{} : Bool}

def nd_l source · line 126 · raw

@+a:List<&2, Nat> -> @+x:List<&2, Nat> -> @+h:{nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, x)) == True{} : Bool} -> {nodupn(a) == True{} : Bool}

def or_true_b source · line 135 · raw

@+b:Bool -> {Bool.or(b, True{}) == True{} : Bool}

def mem_app_r source · line 142 · raw

@+y:Nat -> @+a:List<&2, Nat> -> @+x:List<&2, Nat> -> @+h:{memn(y, x) == True{} : Bool} -> {memn(y, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, x)) == True{} : Bool}

def mem_app_l source · line 145 · raw

@+y:Nat -> @+a:List<&2, Nat> -> @+x:List<&2, Nat> -> @+h:{memn(y, a) == True{} : Bool} -> {memn(y, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, x)) == True{} : Bool}

def dj_c source · line 148 · raw

@+y:Nat -> @+h0:Nat -> @+t:List<&2, Nat> -> @+x:List<&2, Nat> -> @+hy:{memn(y, x) == True{} : Bool} -> @+hn:{Bool.not(memn(h0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, t, x))) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(h0, y) == c : Bool} -> {c == False{} : Bool}

def nd_dj source · line 157 · raw

@+a:List<&2, Nat> -> @+x:List<&2, Nat> -> @+h:{nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, x)) == True{} : Bool} -> @+y:Nat -> @+hy:{memn(y, x) == True{} : Bool} -> {memn(y, a) == False{} : Bool}

def dj2_c source · line 167 · raw

@+a:List<&2, Nat> -> @+x:List<&2, Nat> -> @+h:{nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, x)) == True{} : Bool} -> @+y:Nat -> @+hy:{memn(y, a) == True{} : Bool} -> @+c:Bool -> @+hc:{memn(y, x) == c : Bool} -> {c == False{} : Bool}

def nd_dj2 source · line 174 · raw

@+a:List<&2, Nat> -> @+x:List<&2, Nat> -> @+h:{nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, x)) == True{} : Bool} -> @+y:Nat -> @+hy:{memn(y, a) == True{} : Bool} -> {memn(y, x) == False{} : Bool}

def or_ff_l source · line 177 · raw

@+a:Bool -> @+b:Bool -> @+h:{Bool.or(a, b) == False{} : Bool} -> {a == False{} : Bool}

def or_ff_r source · line 184 · raw

@+a:Bool -> @+b:Bool -> @+h:{Bool.or(a, b) == False{} : Bool} -> {b == False{} : Bool}

def not_f source · line 191 · raw

@+a:Bool -> @+h:{a == False{} : Bool} -> {Bool.not(a) == True{} : Bool}

def or_tl source · line 194 · raw

@+a:Bool -> @+b:Bool -> @+h:{a == True{} : Bool} -> {Bool.or(a, b) == True{} : Bool}

def or_tr source · line 197 · raw

@+a:Bool -> @+b:Bool -> @+h:{b == True{} : Bool} -> {Bool.or(a, b) == True{} : Bool}

def and3 source · line 200 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> @+d:Bool -> {Bool.and(a, Bool.and(b, Bool.and(c, d))) == Bool.and(Bool.and(a, Bool.and(b, c)), d) : Bool}

def ne_sym source · line 209 · raw

@+x:Nat -> @+y:Nat -> @+h:{Nat.is_eq(x, y) == False{} : Bool} -> {Nat.is_eq(y, x) == False{} : Bool}

def lastn source · line 212 · raw

@t:List<&2, Nat> -> @+a:Nat -> Nat

def lastn_mem source · line 219 · raw

@+t:List<&2, Nat> -> @+a:Nat -> {memn(lastn(t, a), a <> t) == True{} : Bool}

def ne_mem_c source · line 226 · raw

@+a:Nat -> @+z:Nat -> @+xs:List<&2, Nat> -> @+h1:{Bool.not(memn(a, xs)) == True{} : Bool} -> @+h2:{memn(z, xs) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(z, a) == c : Bool} -> {c == False{} : Bool}

def ne_mem source · line 234 · raw

@+a:Nat -> @+z:Nat -> @+xs:List<&2, Nat> -> @+h1:{Bool.not(memn(a, xs)) == True{} : Bool} -> @+h2:{memn(z, xs) == True{} : Bool} -> {Nat.is_eq(z, a) == False{} : Bool}

def rapp source · line 237 · raw

@l:List<&2, Nat> -> @b:List<&2, Nat> -> List<&2, Nat>

def len_rapp source · line 244 · raw

@+l:List<&2, Nat> -> @+b:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, rapp(l, b)) == Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, l), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, b)) : Nat}

def Split source · line 251 · raw

@+s:Nat -> @+sl:List<&2, Nat> -> Type

def sp_up source · line 254 · raw

@+x:Nat -> @+s:Nat -> @+t:List<&2, Nat> -> @r:Split(s, t) -> Split(s, x <> t)

def sp_c source · line 259 · raw

@+x:Nat -> @+s:Nat -> @+t:List<&2, Nat> -> @+c:Bool -> @+hc:{Nat.is_eq(x, s) == c : Bool} -> @+hm:{Bool.or(c, memn(s, t)) == True{} : Bool} -> @rec:(@h:{memn(s, t) == True{} : Bool} -> Split(s, t)) -> Split(s, x <> t)

def split_mem source · line 266 · raw

@+s:Nat -> @+sl:List<&2, Nat> -> @+hm:{memn(s, sl) == True{} : Bool} -> Split(s, sl)