~/bend-docscommunity

proofs/containers/balanced_search_tree/dj.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/dj.bend as Dj

6 imports
import Base
import ../../lib/logic.bend as L
import ../../../spec/lib/common.bend as SC
import ./frame.bend as FR
import ./path.bend as P
import ../../lib/nat_list.bend as NL

Definitions

def nm_l source · line 13 · raw

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

def nm_r source · line 16 · raw

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

def nm_ch source · line 19 · raw

@+z:Nat -> @+i:Nat -> @+t:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(z, i <> t) == False{} : Bool} -> {Nat.is_eq(i, z) == False{} : Bool}

def nm_ct source · line 22 · raw

@+z:Nat -> @+i:Nat -> @+t:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(z, i <> t) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(z, t) == False{} : Bool}

def nm_app source · line 25 · raw

@+z:Nat -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(z, a) == False{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(z, b) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(z, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == False{} : Bool}

def nm_cons source · line 30 · raw

@+z:Nat -> @+i:Nat -> @+t:List<&2, Nat> -> @+hi:{Nat.is_eq(i, z) == False{} : Bool} -> @+ht:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(z, t) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(z, i <> t) == False{} : Bool}

def nd_head source · line 35 · raw

@+i:Nat -> @+t:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(i <> t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(i, t) == False{} : Bool}

the head of a list without repeats is not in its tail

def nd_tail source · line 38 · raw

@+i:Nat -> @+t:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(i <> t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(t) == True{} : Bool}

def dj_l source · line 42 · raw

@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool} -> @+z:Nat -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(z, b) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(z, a) == False{} : Bool}

an id of the right part is not in the left one, and conversely

def dj_r source · line 45 · raw

@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool} -> @+z:Nat -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(z, a) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(z, b) == False{} : Bool}

def ndl source · line 48 · raw

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

def ndr source · line 51 · raw

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

def mem_l source · line 54 · raw

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

def mem_r source · line 57 · raw

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

def mem_hd source · line 60 · raw

@+i:Nat -> @+t:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(i, i <> t) == True{} : Bool}

def mem_tl source · line 63 · raw

@+z:Nat -> @+i:Nat -> @+t:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(z, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(z, i <> t) == True{} : Bool}

def ne_nm source · line 67 · raw

@+a:Nat -> @+b:Nat -> @+xs:List<&2, Nat> -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(a, xs) == False{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(b, xs) == True{} : Bool} -> {Nat.is_eq(a, b) == False{} : Bool}

an absent id differs from a present one