1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/u32.bend as U 5 import ../../lib/u32alg.bend as A 6 import ../../lib/array.bend as AR 7 import ../../../spec/lib/common.bend as SC 8 import ../../lib/u32div.bend as UD 9 import ../../../src/containers/internal/dlist_storage.bend as R 10 import ./state.bend as ST 11 import ./links.bend as LK 12 import ../../lib/nat_list.bend as NL 13 import ../../lib/links.bend as LKx 14 import ../../lib/words32.bend as W32 15 import ../../lib/u32_tree.bend as UT 16 17 # Relinking: the writes of an insertion between two neighbours and of an 18 # unlink, over the prev and next lists. 19 20 21 # ---- writes at the first id of b / the last id of a ---- 22 23 # the first id of b is in xs 24 def fstin(b: List<&2, Nat>, xs: List<&2, Nat>) -> Bool: 25 match b: 26 case Nil{}: 27 False{} 28 case Con{+b0, t}: 29 NL.memn(b0, xs) 30 31 # the last id of a is in xs 32 def lastin(a: List<&2, Nat>, xs: List<&2, Nat>) -> Bool: 33 match a: 34 case Nil{}: 35 False{} 36 case Con{+a0, +t}: 37 NL.memn(NL.lastn(t, a0), xs) 38 39 def upd_first(+pl: List<&2, U32>, b: List<&2, Nat>, +v: U32) -> List<&2, U32>: 40 match b: 41 case Nil{}: 42 pl 43 case Con{+b0, t}: 44 SC.update(U32, pl, b0, v) 45 46 def upd_last(+nl: List<&2, U32>, a: List<&2, Nat>, +v: U32) -> List<&2, U32>: 47 match a: 48 case Nil{}: 49 nl 50 case Con{+a0, +t}: 51 SC.update(U32, nl, NL.lastn(t, a0), v) 52 53 def tu_first(+d: Nat, +tr: AR.Tree, b: List<&2, Nat>, +v: U32) -> AR.Tree: 54 match b: 55 case Nil{}: 56 tr 57 case Con{+b0, t}: 58 AR.upd(U32, d, tr, b0, v) 59 60 def tu_last(+d: Nat, +tr: AR.Tree, a: List<&2, Nat>, +v: U32) -> AR.Tree: 61 match a: 62 case Nil{}: 63 tr 64 case Con{+a0, +t}: 65 AR.upd(U32, d, tr, NL.lastn(t, a0), v) 66 67 # ---- bounds ---- 68 69 def hd1(+d: Nat, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}) -> {Nat.is_lt(1n+d, 32n) == True{} : Bool}: 70 N.lt_trans(d, 30n, 31n, hd, {==}) 71 72 def hd0(+d: Nat, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}) -> {Nat.is_lt(d, 32n) == True{} : Bool}: 73 N.lt_trans(d, 30n, 32n, hd, {==}) 74 75 def self_in(+b: Nat, +t: List<&2, Nat>) -> {NL.memn(b, Con{b, t}) == True{} : Bool}: 76 NL.or_tl(Nat.is_eq(b, b), NL.memn(b, t), N.is_eq_refl(b)) 77 78 79 def slok_c(~T: Data, +x: Nat, +y: Nat, +t: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +hy: {Bool.and(Nat.is_lt(y, fr), ST.live(T, vl, y)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(y, x) == c : Bool}, +hm: {Bool.or(c, NL.memn(x, t)) == True{} : Bool}, rec: @hm2: {NL.memn(x, t) == True{} : Bool} -> {Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)) == True{} : Bool}) -> {Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)) == True{} : Bool}: 80 match c: 81 case True{}: 82 L.subst(Nat, z => {Bool.and(Nat.is_lt(z, fr), ST.live(T, vl, z)) == True{} : Bool}, y, x, N.eq_from_is_eq(y, x, hc), hy) 83 case False{}: 84 rec(hm) 85 86 # a member of a slok list is below fr and live 87 def slok_mem(~T: Data, +x: Nat, +xs: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +h: {ST.slok(~T, xs, fr, vl) == True{} : Bool}, +hm: {NL.memn(x, xs) == True{} : Bool}) -> {Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)) == True{} : Bool}: 88 match xs: 89 case Nil{}: 90 Empty.absurd({Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)) == True{} : Bool}, L.false_true(hm)) 91 case Con{+y, +t}: 92 +hy = L.and_left(Bool.and(Nat.is_lt(y, fr), ST.live(T, vl, y)), ST.slok(~T, t, fr, vl), h) 93 +ht = L.and_right(Bool.and(Nat.is_lt(y, fr), ST.live(T, vl, y)), ST.slok(~T, t, fr, vl), h) 94 slok_c(~T, x, y, t, fr, vl, hy, Nat.is_eq(y, x), {==}, hm, hm2 => slok_mem(~T, x, t, fr, vl, ht, hm2)) 95 96 def flok_c(~T: Data, +x: Nat, +y: Nat, +t: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +hy: {Bool.and(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y))) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(y, x) == c : Bool}, +hm: {Bool.or(c, NL.memn(x, t)) == True{} : Bool}, rec: @hm2: {NL.memn(x, t) == True{} : Bool} -> {Bool.and(Nat.is_lt(x, fr), Bool.not(ST.live(T, vl, x))) == True{} : Bool}) -> {Bool.and(Nat.is_lt(x, fr), Bool.not(ST.live(T, vl, x))) == True{} : Bool}: 97 match c: 98 case True{}: 99 L.subst(Nat, z => {Bool.and(Nat.is_lt(z, fr), Bool.not(ST.live(T, vl, z))) == True{} : Bool}, y, x, N.eq_from_is_eq(y, x, hc), hy) 100 case False{}: 101 rec(hm) 102 103 # a member of a flok list is below fr and vacant 104 def flok_mem(~T: Data, +x: Nat, +xs: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +h: {ST.flok(~T, xs, fr, vl) == True{} : Bool}, +hm: {NL.memn(x, xs) == True{} : Bool}) -> {Bool.and(Nat.is_lt(x, fr), Bool.not(ST.live(T, vl, x))) == True{} : Bool}: 105 match xs: 106 case Nil{}: 107 Empty.absurd({Bool.and(Nat.is_lt(x, fr), Bool.not(ST.live(T, vl, x))) == True{} : Bool}, L.false_true(hm)) 108 case Con{+y, +t}: 109 +hy = L.and_left(Bool.and(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y))), ST.flok(~T, t, fr, vl), h) 110 +ht = L.and_right(Bool.and(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y))), ST.flok(~T, t, fr, vl), h) 111 flok_c(~T, x, y, t, fr, vl, hy, Nat.is_eq(y, x), {==}, hm, hm2 => flok_mem(~T, x, t, fr, vl, ht, hm2)) 112 113 def slok_app(~T: Data, +a: List<&2, Nat>, +b: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>) -> {ST.slok(~T, SC.append(Nat, a, b), fr, vl) == Bool.and(ST.slok(~T, a, fr, vl), ST.slok(~T, b, fr, vl)) : Bool}: 114 match a: 115 case Nil{}: 116 {==} 117 case Con{+x, +t}: 118 +ih = slok_app(~T, t, b, fr, vl) 119 Equal.trans(Bool, Bool.and(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, SC.append(Nat, t, b), fr, vl)), Bool.and(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), Bool.and(ST.slok(~T, t, fr, vl), ST.slok(~T, b, fr, vl))), Bool.and(Bool.and(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl)), ST.slok(~T, b, fr, vl)), Equal.cong(Bool, Bool, z => Bool.and(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), z), ST.slok(~T, SC.append(Nat, t, b), fr, vl), Bool.and(ST.slok(~T, t, fr, vl), ST.slok(~T, b, fr, vl)), ih), NL.and_assoc(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl), ST.slok(~T, b, fr, vl))) 120 121 # a live id is not on a vacant list 122 def dj_c(~T: Data, +x: Nat, +y: Nat, +t: List<&2, Nat>, +vl: List<&2, Maybe<&2, T>>, +hx: {ST.live(T, vl, x) == True{} : Bool}, +hy: {Bool.not(ST.live(T, vl, y)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(y, x) == c : Bool}, +ih: {NL.memn(x, t) == False{} : Bool}) -> {Bool.or(c, NL.memn(x, t)) == False{} : Bool}: 123 match c: 124 case True{}: 125 +hy2 = L.subst(Nat, z => {Bool.not(ST.live(T, vl, z)) == True{} : Bool}, y, x, N.eq_from_is_eq(y, x, hc), hy) 126 Empty.absurd({Bool.or(True{}, NL.memn(x, t)) == False{} : Bool}, L.true_not_false(ST.live(T, vl, x), hx, L.not_true(ST.live(T, vl, x), hy2))) 127 case False{}: 128 ih 129 130 def live_nf(~T: Data, +x: Nat, +ys: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +hx: {ST.live(T, vl, x) == True{} : Bool}, +h: {ST.flok(~T, ys, fr, vl) == True{} : Bool}) -> {NL.memn(x, ys) == False{} : Bool}: 131 match ys: 132 case Nil{}: 133 {==} 134 case Con{+y, +t}: 135 +hy = L.and_right(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y)), L.and_left(Bool.and(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y))), ST.flok(~T, t, fr, vl), h)) 136 +ht = L.and_right(Bool.and(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y))), ST.flok(~T, t, fr, vl), h) 137 dj_c(~T, x, y, t, vl, hx, hy, Nat.is_eq(y, x), {==}, live_nf(~T, x, t, fr, vl, hx, ht)) 138 139 # an id at or above fr is on no slok list 140 def hi_c(+x: Nat, +y: Nat, +fr: Nat, +hy: {Nat.is_lt(y, fr) == True{} : Bool}, +hx: {Nat.is_le(fr, x) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(y, x) == c : Bool}, +m: Bool, +ih: {m == False{} : Bool}) -> {Bool.or(c, m) == False{} : Bool}: 141 match c: 142 case True{}: 143 +hy2 = L.subst(Nat, z => {Nat.is_lt(z, fr) == True{} : Bool}, y, x, N.eq_from_is_eq(y, x, hc), hy) 144 Empty.absurd({Bool.or(True{}, m) == False{} : Bool}, N.lt_ne(x, x, N.lt_le_trans(x, fr, x, hy2, hx), {==})) 145 case False{}: 146 ih 147 148 def hi_ns(~T: Data, +x: Nat, +ys: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +hx: {Nat.is_le(fr, x) == True{} : Bool}, +h: {ST.slok(~T, ys, fr, vl) == True{} : Bool}) -> {NL.memn(x, ys) == False{} : Bool}: 149 match ys: 150 case Nil{}: 151 {==} 152 case Con{+y, +t}: 153 +hy = L.and_left(Nat.is_lt(y, fr), ST.live(T, vl, y), L.and_left(Bool.and(Nat.is_lt(y, fr), ST.live(T, vl, y)), ST.slok(~T, t, fr, vl), h)) 154 +ht = L.and_right(Bool.and(Nat.is_lt(y, fr), ST.live(T, vl, y)), ST.slok(~T, t, fr, vl), h) 155 hi_c(x, y, fr, hy, hx, Nat.is_eq(y, x), {==}, NL.memn(x, t), hi_ns(~T, x, t, fr, vl, hx, ht)) 156 157 def hi_nf(~T: Data, +x: Nat, +ys: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +hx: {Nat.is_le(fr, x) == True{} : Bool}, +h: {ST.flok(~T, ys, fr, vl) == True{} : Bool}) -> {NL.memn(x, ys) == False{} : Bool}: 158 match ys: 159 case Nil{}: 160 {==} 161 case Con{+y, +t}: 162 +hy = L.and_left(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y)), L.and_left(Bool.and(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y))), ST.flok(~T, t, fr, vl), h)) 163 +ht = L.and_right(Bool.and(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y))), ST.flok(~T, t, fr, vl), h) 164 hi_c(x, y, fr, hy, hx, Nat.is_eq(y, x), {==}, NL.memn(x, t), hi_nf(~T, x, t, fr, vl, hx, ht)) 165 166 # ---- first/last bounds ---- 167 168 def fstlt(b: List<&2, Nat>, +m: Nat) -> Bool: 169 match b: 170 case Nil{}: 171 True{} 172 case Con{+b0, t}: 173 Nat.is_lt(b0, m) 174 175 def lastlt(a: List<&2, Nat>, +m: Nat) -> Bool: 176 match a: 177 case Nil{}: 178 True{} 179 case Con{+a0, +t}: 180 Nat.is_lt(NL.lastn(t, a0), m) 181 182 def fstlt_of(~T: Data, +b: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +m: Nat, +hfr: {Nat.is_le(fr, m) == True{} : Bool}, +h: {ST.slok(~T, b, fr, vl) == True{} : Bool}) -> {fstlt(b, m) == True{} : Bool}: 183 match b: 184 case Nil{}: 185 {==} 186 case Con{+b0, +t}: 187 N.lt_le_trans(b0, fr, m, L.and_left(Nat.is_lt(b0, fr), ST.live(T, vl, b0), slok_mem(~T, b0, Con{b0, t}, fr, vl, h, self_in(b0, t))), hfr) 188 189 def lastlt_of(~T: Data, +a: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +m: Nat, +hfr: {Nat.is_le(fr, m) == True{} : Bool}, +h: {ST.slok(~T, a, fr, vl) == True{} : Bool}) -> {lastlt(a, m) == True{} : Bool}: 190 match a: 191 case Nil{}: 192 {==} 193 case Con{+a0, +t}: 194 N.lt_le_trans(NL.lastn(t, a0), fr, m, L.and_left(Nat.is_lt(NL.lastn(t, a0), fr), ST.live(T, vl, NL.lastn(t, a0)), slok_mem(~T, NL.lastn(t, a0), Con{a0, t}, fr, vl, h, NL.lastn_mem(t, a0))), hfr) 195 196 # ---- links of ids below 2^d ---- 197 198 def lnk_nz(+one: Nat, +h1: {one == 1n : Nat}, +b: Nat, +d: Nat, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +hb: {Nat.is_lt(b, SC.pow2(d)) == True{} : Bool}) -> {U32.is_eq(LKx.lnk(b), 0) == False{} : Bool}: 199 +hk = N.lt_le(d, 32n, hd0(d, hd)) 200 +e1 = U.to_nat_from_nat(b, d, hk, hb) 201 +hb2 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, b, UD.v(U32.from_nat(b)), Equal.sym(Nat, UD.v(U32.from_nat(b)), b, e1), hb) 202 W32.link_nz(one, h1, U32.from_nat(b), W32.bound32(one, h1, UD.v(U32.from_nat(b)), d, hd1(d, hd), hb2)) 203 204 def slot_lnk(+one: Nat, +h1: {one == 1n : Nat}, +b: Nat, +d: Nat, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +hb: {Nat.is_lt(b, SC.pow2(d)) == True{} : Bool}) -> {UD.v(R.slot(LKx.lnk(b))) == b : Nat}: 205 LKx.slot_lnk(one, h1, b, d, hd1(d, hd), hb) 206 207 208 # the write at the id of a link 209 def sn_c(+one: Nat, +h1: {one == 1n : Nat}, +d: Nat, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +tr: AR.Tree, +pf: {AR.perfect(U32, d, tr) == True{} : Bool}, +b0: Nat, +hb: {Nat.is_lt(b0, SC.pow2(d)) == True{} : Bool}, +v: U32) -> {R.set_next(AR.thaw(U32, tr), LKx.lnk(b0), v) == AR.thaw(U32, AR.upd(U32, d, tr, b0, v)) : Array}: 210 +i = R.slot(LKx.lnk(b0)) 211 +es = slot_lnk(one, h1, b0, d, hd, hb) 212 +hi = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, b0, UD.v(i), Equal.sym(Nat, UD.v(i), b0, es), hb) 213 +e1 = Equal.cong(Bool, Array, z => R.set_next_go(AR.thaw(U32, tr), LKx.lnk(b0), v, z), U32.is_eq(LKx.lnk(b0), 0), False{}, lnk_nz(one, h1, b0, d, hd, hb)) 214 +e2 = UT.uset_a(d, hd0(d, hd), tr, pf, i, hi, v) 215 +e3 = Equal.cong(Nat, Array, z => AR.thaw(U32, AR.upd(U32, d, tr, z, v)), UD.v(i), b0, es) 216 Equal.trans(Array, R.set_next(AR.thaw(U32, tr), LKx.lnk(b0), v), Array.set(U32, AR.thaw(U32, tr), i, v), AR.thaw(U32, AR.upd(U32, d, tr, b0, v)), e1, Equal.trans(Array, Array.set(U32, AR.thaw(U32, tr), i, v), AR.thaw(U32, AR.upd(U32, d, tr, UD.v(i), v)), AR.thaw(U32, AR.upd(U32, d, tr, b0, v)), e2, e3)) 217 218 # set_next at b's first link 219 def sn_first(+one: Nat, +h1: {one == 1n : Nat}, +d: Nat, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +tr: AR.Tree, +pf: {AR.perfect(U32, d, tr) == True{} : Bool}, +b: List<&2, Nat>, +hb: {fstlt(b, SC.pow2(d)) == True{} : Bool}, +v: U32) -> {R.set_next(AR.thaw(U32, tr), LKx.fst_or(b, 0), v) == AR.thaw(U32, tu_first(d, tr, b, v)) : Array}: 220 match b: 221 case Nil{}: 222 {==} 223 case Con{+b0, +t}: 224 sn_c(one, h1, d, hd, tr, pf, b0, hb, v) 225 226 # set_next at a's last link 227 def sn_last(+one: Nat, +h1: {one == 1n : Nat}, +d: Nat, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +tr: AR.Tree, +pf: {AR.perfect(U32, d, tr) == True{} : Bool}, +a: List<&2, Nat>, +ha: {lastlt(a, SC.pow2(d)) == True{} : Bool}, +v: U32) -> {R.set_next(AR.thaw(U32, tr), LKx.last_or(a, 0), v) == AR.thaw(U32, tu_last(d, tr, a, v)) : Array}: 228 match a: 229 case Nil{}: 230 {==} 231 case Con{+a0, +t}: 232 +e0 = Equal.cong(U32, Array, w => R.set_next(AR.thaw(U32, tr), w, v), LKx.last_or(t, LKx.lnk(a0)), LKx.lnk(NL.lastn(t, a0)), LKx.last_lnk(t, a0)) 233 Equal.trans(Array, R.set_next(AR.thaw(U32, tr), LKx.last_or(t, LKx.lnk(a0)), v), R.set_next(AR.thaw(U32, tr), LKx.lnk(NL.lastn(t, a0)), v), AR.thaw(U32, AR.upd(U32, d, tr, NL.lastn(t, a0), v)), e0, sn_c(one, h1, d, hd, tr, pf, NL.lastn(t, a0), ha, v)) 234 235 def tf_p(+d: Nat, +tr: AR.Tree, +pf: {AR.perfect(U32, d, tr) == True{} : Bool}, +b: List<&2, Nat>, +v: U32) -> {AR.perfect(U32, d, tu_first(d, tr, b, v)) == True{} : Bool}: 236 match b: 237 case Nil{}: 238 pf 239 case Con{+b0, +t}: 240 UT.uset_p(d, tr, pf, b0, v) 241 242 def tl_p(+d: Nat, +tr: AR.Tree, +pf: {AR.perfect(U32, d, tr) == True{} : Bool}, +a: List<&2, Nat>, +v: U32) -> {AR.perfect(U32, d, tu_last(d, tr, a, v)) == True{} : Bool}: 243 match a: 244 case Nil{}: 245 pf 246 case Con{+a0, +t}: 247 UT.uset_p(d, tr, pf, NL.lastn(t, a0), v) 248 249 def tf_s(+d: Nat, +tr: AR.Tree, +pf: {AR.perfect(U32, d, tr) == True{} : Bool}, +b: List<&2, Nat>, +hb: {fstlt(b, SC.pow2(d)) == True{} : Bool}, +v: U32) -> {AR.slots(U32, tu_first(d, tr, b, v)) == upd_first(AR.slots(U32, tr), b, v) : List<&2, U32>}: 250 match b: 251 case Nil{}: 252 {==} 253 case Con{+b0, +t}: 254 UT.uset_s(d, tr, pf, b0, hb, v) 255 256 def tl_s(+d: Nat, +tr: AR.Tree, +pf: {AR.perfect(U32, d, tr) == True{} : Bool}, +a: List<&2, Nat>, +ha: {lastlt(a, SC.pow2(d)) == True{} : Bool}, +v: U32) -> {AR.slots(U32, tu_last(d, tr, a, v)) == upd_last(AR.slots(U32, tr), a, v) : List<&2, U32>}: 257 match a: 258 case Nil{}: 259 {==} 260 case Con{+a0, +t}: 261 UT.uset_s(d, tr, pf, NL.lastn(t, a0), ha, v) 262 263 # ---- frames ---- 264 265 def seg_ffp(+pl: List<&2, U32>, +nl: List<&2, U32>, +b: List<&2, Nat>, +v: U32, +xs: List<&2, Nat>, +p: U32, +q: U32, +h: {fstin(b, xs) == False{} : Bool}) -> {ST.seg(upd_first(pl, b, v), nl, xs, p, q) == ST.seg(pl, nl, xs, p, q) : Bool}: 266 match b: 267 case Nil{}: 268 {==} 269 case Con{+b0, +t}: 270 LK.seg_fp(pl, nl, b0, v, xs, p, q, h) 271 272 def seg_lfn(+pl: List<&2, U32>, +nl: List<&2, U32>, +a: List<&2, Nat>, +v: U32, +xs: List<&2, Nat>, +p: U32, +q: U32, +h: {lastin(a, xs) == False{} : Bool}) -> {ST.seg(pl, upd_last(nl, a, v), xs, p, q) == ST.seg(pl, nl, xs, p, q) : Bool}: 273 match a: 274 case Nil{}: 275 {==} 276 case Con{+a0, +t}: 277 LK.seg_fn(pl, nl, NL.lastn(t, a0), v, xs, p, q, h) 278 279 def fll_lfn(+nl: List<&2, U32>, +a: List<&2, Nat>, +v: U32, +fl: List<&2, Nat>, +h: {lastin(a, fl) == False{} : Bool}) -> {ST.fll(upd_last(nl, a, v), fl) == ST.fll(nl, fl) : Bool}: 280 match a: 281 case Nil{}: 282 {==} 283 case Con{+a0, +t}: 284 LK.fll_fn(nl, NL.lastn(t, a0), v, fl, h) 285 286 def ne1(+n: Nat, +x: Nat, +h: {NL.memn(x, Con{n, Nil{}}) == False{} : Bool}) -> {Nat.is_eq(x, n) == False{} : Bool}: 287 NL.ne_sym(n, x, NL.or_ff_l(Nat.is_eq(n, x), False{}, h)) 288 289 def nth_uf(+pl: List<&2, U32>, +b: List<&2, Nat>, +v: U32, +n: Nat, +h: {fstin(b, Con{n, Nil{}}) == False{} : Bool}) -> {W32.nth0(upd_first(pl, b, v), n) == W32.nth0(pl, n) : U32}: 290 match b: 291 case Nil{}: 292 {==} 293 case Con{+b0, +t}: 294 W32.nth0_upd_other(pl, b0, n, v, ne1(n, b0, h)) 295 296 def nth_ul(+nl: List<&2, U32>, +a: List<&2, Nat>, +v: U32, +n: Nat, +h: {lastin(a, Con{n, Nil{}}) == False{} : Bool}) -> {W32.nth0(upd_last(nl, a, v), n) == W32.nth0(nl, n) : U32}: 297 match a: 298 case Nil{}: 299 {==} 300 case Con{+a0, +t}: 301 W32.nth0_upd_other(nl, NL.lastn(t, a0), n, v, ne1(n, NL.lastn(t, a0), h)) 302 303 # ---- re-targeting ---- 304 305 def seg_ufp(+pl: List<&2, U32>, +nl: List<&2, U32>, +b: List<&2, Nat>, +x: U32, +q: U32, +y: U32, +hs: {ST.seg(pl, nl, b, x, q) == True{} : Bool}, +hn: {NL.nodupn(b) == True{} : Bool}, +hl: {fstlt(b, SC.length(U32, pl)) == True{} : Bool}) -> {ST.seg(upd_first(pl, b, y), nl, b, y, q) == True{} : Bool}: 306 match b: 307 case Nil{}: 308 {==} 309 case Con{+b0, +t}: 310 LK.segp(pl, nl, b0, t, x, q, y, hs, hn, hl) 311 312 def seg_ulq(+pl: List<&2, U32>, +nl: List<&2, U32>, +a: List<&2, Nat>, +p: U32, +x: U32, +y: U32, +hs: {ST.seg(pl, nl, a, p, x) == True{} : Bool}, +hn: {NL.nodupn(a) == True{} : Bool}, +hl: {lastlt(a, SC.length(U32, nl)) == True{} : Bool}) -> {ST.seg(pl, upd_last(nl, a, y), a, p, y) == True{} : Bool}: 313 match a: 314 case Nil{}: 315 {==} 316 case Con{+a0, +t}: 317 LK.segq(pl, nl, t, a0, p, x, y, hs, hn, hl) 318 319 # ---- rewriting a truth ---- 320 321 # b1 is true when b1 == b2 and b2 is 322 def by_eq(+b1: Bool, +b2: Bool, +e: {b1 == b2 : Bool}, +h: {b2 == True{} : Bool}) -> {b1 == True{} : Bool}: 323 L.subst(Bool, z => {z == True{} : Bool}, b2, b1, Equal.sym(Bool, b1, b2, e), h) 324 325 # b2 is true when b1 == b2 and b1 is 326 def to_eq(+b1: Bool, +b2: Bool, +e: {b1 == b2 : Bool}, +h: {b1 == True{} : Bool}) -> {b2 == True{} : Bool}: 327 L.subst(Bool, z => {z == True{} : Bool}, b1, b2, e, h) 328 329 def u_is(+x: U32, +y: U32, +e: {x == y : U32}) -> {U32.is_eq(x, y) == True{} : Bool}: 330 L.subst(U32, z => {U32.is_eq(z, y) == True{} : Bool}, y, x, Equal.sym(U32, x, y, e), LKx.u_refl(y)) 331 332 # ---- disjointness of the parts of a list without repeats ---- 333 334 # a ++ s :: b: b's first id is not in a 335 def fin_dj(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hn: {NL.nodupn(SC.append(Nat, a, Con{s, b})) == True{} : Bool}) -> {fstin(b, a) == False{} : Bool}: 336 match b: 337 case Nil{}: 338 {==} 339 case Con{+b0, +t}: 340 NL.nd_dj(a, Con{s, Con{b0, t}}, hn, b0, NL.or_tr(Nat.is_eq(s, b0), NL.memn(b0, Con{b0, t}), self_in(b0, t))) 341 342 # a ++ s :: b: a's last id is not in b 343 def lin_dj(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hn: {NL.nodupn(SC.append(Nat, a, Con{s, b})) == True{} : Bool}) -> {lastin(a, b) == False{} : Bool}: 344 match a: 345 case Nil{}: 346 {==} 347 case Con{+a0, +t}: 348 NL.or_ff_r(Nat.is_eq(s, NL.lastn(t, a0)), NL.memn(NL.lastn(t, a0), b), NL.nd_dj2(Con{a0, t}, Con{s, b}, hn, NL.lastn(t, a0), NL.lastn_mem(t, a0))) 349 350 # a ++ b: b's first id is not in a 351 def fin_dj2(+a: List<&2, Nat>, +b: List<&2, Nat>, +hn: {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}) -> {fstin(b, a) == False{} : Bool}: 352 match b: 353 case Nil{}: 354 {==} 355 case Con{+b0, +t}: 356 NL.nd_dj(a, Con{b0, t}, hn, b0, self_in(b0, t)) 357 358 # a ++ b: a's last id is not in b 359 def lin_dj2(+a: List<&2, Nat>, +b: List<&2, Nat>, +hn: {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}) -> {lastin(a, b) == False{} : Bool}: 360 match a: 361 case Nil{}: 362 {==} 363 case Con{+a0, +t}: 364 NL.nd_dj2(Con{a0, t}, b, hn, NL.lastn(t, a0), NL.lastn_mem(t, a0)) 365 366 def or_f(+x: Bool, +h: {x == False{} : Bool}) -> {Bool.or(x, False{}) == False{} : Bool}: 367 L.subst(Bool, z => {Bool.or(z, False{}) == False{} : Bool}, False{}, x, Equal.sym(Bool, x, False{}, h), {==}) 368 369 # n off b: b's first id is not n 370 def fin1(+b: List<&2, Nat>, +n: Nat, +h: {NL.memn(n, b) == False{} : Bool}) -> {fstin(b, Con{n, Nil{}}) == False{} : Bool}: 371 match b: 372 case Nil{}: 373 {==} 374 case Con{+b0, +t}: 375 or_f(Nat.is_eq(n, b0), NL.ne_sym(b0, n, NL.or_ff_l(Nat.is_eq(b0, n), NL.memn(n, t), h))) 376 377 # n off a: a's last id is not n 378 def lin1(+a: List<&2, Nat>, +n: Nat, +h: {NL.memn(n, a) == False{} : Bool}) -> {lastin(a, Con{n, Nil{}}) == False{} : Bool}: 379 match a: 380 case Nil{}: 381 {==} 382 case Con{+a0, +t}: 383 or_f(Nat.is_eq(n, NL.lastn(t, a0)), NL.ne_sym(NL.lastn(t, a0), n, NL.ne_mem(n, NL.lastn(t, a0), Con{a0, t}, NL.not_f(NL.memn(n, Con{a0, t}), h), NL.lastn_mem(t, a0)))) 384 385 386 # THEOREM (unlink): s between a and b; b's first prev becomes a's last link 387 # and a's last next becomes b's first link: a ++ b is linked 388 def unl_seg(+pl: List<&2, U32>, +nl: List<&2, U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hs: {ST.seg(pl, nl, SC.append(Nat, a, Con{s, b}), 0, 0) == True{} : Bool}, +hn: {NL.nodupn(SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hlp: {fstlt(b, SC.length(U32, pl)) == True{} : Bool}, +hln: {lastlt(a, SC.length(U32, nl)) == True{} : Bool}) -> {ST.seg(upd_first(pl, b, LKx.last_or(a, 0)), upd_last(nl, a, LKx.fst_or(b, 0)), SC.append(Nat, a, b), 0, 0) == True{} : Bool}: 389 +pl2 = upd_first(pl, b, LKx.last_or(a, 0)) 390 +nl2 = upd_last(nl, a, LKx.fst_or(b, 0)) 391 +hsp = to_eq(ST.seg(pl, nl, SC.append(Nat, a, Con{s, b}), 0, 0), Bool.and(ST.seg(pl, nl, a, 0, LKx.lnk(s)), ST.seg(pl, nl, Con{s, b}, LKx.last_or(a, 0), 0)), LK.seg_app(pl, nl, a, Con{s, b}, 0, 0), hs) 392 +hsA = L.and_left(ST.seg(pl, nl, a, 0, LKx.lnk(s)), ST.seg(pl, nl, Con{s, b}, LKx.last_or(a, 0), 0), hsp) 393 +hsS = L.and_right(ST.seg(pl, nl, a, 0, LKx.lnk(s)), ST.seg(pl, nl, Con{s, b}, LKx.last_or(a, 0), 0), hsp) 394 +hsB = L.and_right(U32.is_eq(W32.nth0(nl, s), LKx.fst_or(b, 0)), ST.seg(pl, nl, b, LKx.lnk(s), 0), L.and_right(U32.is_eq(W32.nth0(pl, s), LKx.last_or(a, 0)), Bool.and(U32.is_eq(W32.nth0(nl, s), LKx.fst_or(b, 0)), ST.seg(pl, nl, b, LKx.lnk(s), 0)), hsS)) 395 +hnS = NL.nd_r(a, Con{s, b}, hn) 396 +hA1 = seg_ulq(pl, nl, a, 0, LKx.lnk(s), LKx.fst_or(b, 0), hsA, NL.nd_l(a, Con{s, b}, hn), hln) 397 +hA = by_eq(ST.seg(pl2, nl2, a, 0, LKx.fst_or(b, 0)), ST.seg(pl, nl2, a, 0, LKx.fst_or(b, 0)), seg_ffp(pl, nl2, b, LKx.last_or(a, 0), a, 0, LKx.fst_or(b, 0), fin_dj(a, s, b, hn)), hA1) 398 +hB1 = seg_ufp(pl, nl, b, LKx.lnk(s), 0, LKx.last_or(a, 0), hsB, L.and_right(Bool.not(NL.memn(s, b)), NL.nodupn(b), hnS), hlp) 399 +hB = by_eq(ST.seg(pl2, nl2, b, LKx.last_or(a, 0), 0), ST.seg(pl2, nl, b, LKx.last_or(a, 0), 0), seg_lfn(pl2, nl, a, LKx.fst_or(b, 0), b, LKx.last_or(a, 0), 0, lin_dj(a, s, b, hn)), hB1) 400 by_eq(ST.seg(pl2, nl2, SC.append(Nat, a, b), 0, 0), Bool.and(ST.seg(pl2, nl2, a, 0, LKx.fst_or(b, 0)), ST.seg(pl2, nl2, b, LKx.last_or(a, 0), 0)), LK.seg_app(pl2, nl2, a, b, 0, 0), L.and_intro(ST.seg(pl2, nl2, a, 0, LKx.fst_or(b, 0)), ST.seg(pl2, nl2, b, LKx.last_or(a, 0), 0), hA, hB)) 401 402 # ... and s's own links are a's last and b's first 403 def unl_p(+pl: List<&2, U32>, +nl: List<&2, U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hs: {ST.seg(pl, nl, SC.append(Nat, a, Con{s, b}), 0, 0) == True{} : Bool}) -> {W32.nth0(pl, s) == LKx.last_or(a, 0) : U32}: 404 +hsp = to_eq(ST.seg(pl, nl, SC.append(Nat, a, Con{s, b}), 0, 0), Bool.and(ST.seg(pl, nl, a, 0, LKx.lnk(s)), ST.seg(pl, nl, Con{s, b}, LKx.last_or(a, 0), 0)), LK.seg_app(pl, nl, a, Con{s, b}, 0, 0), hs) 405 +hsS = L.and_right(ST.seg(pl, nl, a, 0, LKx.lnk(s)), ST.seg(pl, nl, Con{s, b}, LKx.last_or(a, 0), 0), hsp) 406 A.eq_of(W32.nth0(pl, s), LKx.last_or(a, 0), L.and_left(U32.is_eq(W32.nth0(pl, s), LKx.last_or(a, 0)), Bool.and(U32.is_eq(W32.nth0(nl, s), LKx.fst_or(b, 0)), ST.seg(pl, nl, b, LKx.lnk(s), 0)), hsS)) 407 408 def unl_n(+pl: List<&2, U32>, +nl: List<&2, U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hs: {ST.seg(pl, nl, SC.append(Nat, a, Con{s, b}), 0, 0) == True{} : Bool}) -> {W32.nth0(nl, s) == LKx.fst_or(b, 0) : U32}: 409 +hsp = to_eq(ST.seg(pl, nl, SC.append(Nat, a, Con{s, b}), 0, 0), Bool.and(ST.seg(pl, nl, a, 0, LKx.lnk(s)), ST.seg(pl, nl, Con{s, b}, LKx.last_or(a, 0), 0)), LK.seg_app(pl, nl, a, Con{s, b}, 0, 0), hs) 410 +hsS = L.and_right(ST.seg(pl, nl, a, 0, LKx.lnk(s)), ST.seg(pl, nl, Con{s, b}, LKx.last_or(a, 0), 0), hsp) 411 +hr = L.and_right(U32.is_eq(W32.nth0(pl, s), LKx.last_or(a, 0)), Bool.and(U32.is_eq(W32.nth0(nl, s), LKx.fst_or(b, 0)), ST.seg(pl, nl, b, LKx.lnk(s), 0)), hsS) 412 A.eq_of(W32.nth0(nl, s), LKx.fst_or(b, 0), L.and_left(U32.is_eq(W32.nth0(nl, s), LKx.fst_or(b, 0)), ST.seg(pl, nl, b, LKx.lnk(s), 0), hr)) 413 414 415 # THEOREM (insert between): n off a ++ b takes a's last as prev and b's 416 # first as next, and becomes their next and prev: a ++ n :: b is linked 417 def ins_seg(+pl: List<&2, U32>, +nl: List<&2, U32>, +a: List<&2, Nat>, +b: List<&2, Nat>, +n: Nat, +hs: {ST.seg(pl, nl, SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +hn: {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}, +hna: {NL.memn(n, a) == False{} : Bool}, +hnb: {NL.memn(n, b) == False{} : Bool}, +hlp: {Nat.is_lt(n, SC.length(U32, pl)) == True{} : Bool}, +hlq: {Nat.is_lt(n, SC.length(U32, nl)) == True{} : Bool}, +hfp: {fstlt(b, SC.length(U32, SC.update(U32, pl, n, LKx.last_or(a, 0)))) == True{} : Bool}, +hfq: {lastlt(a, SC.length(U32, SC.update(U32, nl, n, LKx.fst_or(b, 0)))) == True{} : Bool}) -> {ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), SC.append(Nat, a, Con{n, b}), 0, 0) == True{} : Bool}: 418 +hsp = to_eq(ST.seg(pl, nl, SC.append(Nat, a, b), 0, 0), Bool.and(ST.seg(pl, nl, a, 0, LKx.fst_or(b, 0)), ST.seg(pl, nl, b, LKx.last_or(a, 0), 0)), LK.seg_app(pl, nl, a, b, 0, 0), hs) 419 +hsA = L.and_left(ST.seg(pl, nl, a, 0, LKx.fst_or(b, 0)), ST.seg(pl, nl, b, LKx.last_or(a, 0), 0), hsp) 420 +hsB = L.and_right(ST.seg(pl, nl, a, 0, LKx.fst_or(b, 0)), ST.seg(pl, nl, b, LKx.last_or(a, 0), 0), hsp) 421 +hA1 = by_eq(ST.seg(pl, SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, 0, LKx.fst_or(b, 0)), ST.seg(pl, nl, a, 0, LKx.fst_or(b, 0)), LK.seg_fn(pl, nl, n, LKx.fst_or(b, 0), a, 0, LKx.fst_or(b, 0), hna), hsA) 422 +hA2 = seg_ulq(pl, SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, 0, LKx.fst_or(b, 0), LKx.lnk(n), hA1, NL.nd_l(a, b, hn), hfq) 423 +hA3 = by_eq(ST.seg(SC.update(U32, pl, n, LKx.last_or(a, 0)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), a, 0, LKx.lnk(n)), ST.seg(pl, upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), a, 0, LKx.lnk(n)), LK.seg_fp(pl, upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), n, LKx.last_or(a, 0), a, 0, LKx.lnk(n), hna), hA2) 424 +hA = by_eq(ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), a, 0, LKx.lnk(n)), ST.seg(SC.update(U32, pl, n, LKx.last_or(a, 0)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), a, 0, LKx.lnk(n)), seg_ffp(SC.update(U32, pl, n, LKx.last_or(a, 0)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), b, LKx.lnk(n), a, 0, LKx.lnk(n), fin_dj2(a, b, hn)), hA3) 425 +ep = Equal.trans(U32, W32.nth0(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), n), W32.nth0(SC.update(U32, pl, n, LKx.last_or(a, 0)), n), LKx.last_or(a, 0), nth_uf(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n), n, fin1(b, n, hnb)), W32.nth0_upd_same(pl, n, LKx.last_or(a, 0), hlp)) 426 +eq = Equal.trans(U32, W32.nth0(upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), n), W32.nth0(SC.update(U32, nl, n, LKx.fst_or(b, 0)), n), LKx.fst_or(b, 0), nth_ul(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n), n, lin1(a, n, hna)), W32.nth0_upd_same(nl, n, LKx.fst_or(b, 0), hlq)) 427 +hB1 = by_eq(ST.seg(SC.update(U32, pl, n, LKx.last_or(a, 0)), nl, b, LKx.last_or(a, 0), 0), ST.seg(pl, nl, b, LKx.last_or(a, 0), 0), LK.seg_fp(pl, nl, n, LKx.last_or(a, 0), b, LKx.last_or(a, 0), 0, hnb), hsB) 428 +hB2 = seg_ufp(SC.update(U32, pl, n, LKx.last_or(a, 0)), nl, b, LKx.last_or(a, 0), 0, LKx.lnk(n), hB1, NL.nd_r(a, b, hn), hfp) 429 +hB3 = by_eq(ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), SC.update(U32, nl, n, LKx.fst_or(b, 0)), b, LKx.lnk(n), 0), ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), nl, b, LKx.lnk(n), 0), LK.seg_fn(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), nl, n, LKx.fst_or(b, 0), b, LKx.lnk(n), 0, hnb), hB2) 430 +hB = by_eq(ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), b, LKx.lnk(n), 0), ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), SC.update(U32, nl, n, LKx.fst_or(b, 0)), b, LKx.lnk(n), 0), seg_lfn(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n), b, LKx.lnk(n), 0, lin_dj2(a, b, hn)), hB3) 431 +hN = L.and_intro(U32.is_eq(W32.nth0(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), n), LKx.last_or(a, 0)), Bool.and(U32.is_eq(W32.nth0(upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), n), LKx.fst_or(b, 0)), ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), b, LKx.lnk(n), 0)), u_is(W32.nth0(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), n), LKx.last_or(a, 0), ep), L.and_intro(U32.is_eq(W32.nth0(upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), n), LKx.fst_or(b, 0)), ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), b, LKx.lnk(n), 0), u_is(W32.nth0(upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), n), LKx.fst_or(b, 0), eq), hB)) 432 by_eq(ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), SC.append(Nat, a, Con{n, b}), 0, 0), Bool.and(ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), a, 0, LKx.lnk(n)), ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), Con{n, b}, LKx.last_or(a, 0), 0)), LK.seg_app(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), a, Con{n, b}, 0, 0), L.and_intro(ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), a, 0, LKx.lnk(n)), ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), Con{n, b}, LKx.last_or(a, 0), 0), hA, hN))