1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../../src/containers/balanced_search_tree.bend as M 5 import ./state.bend as ST 6 import ./setters.bend as SE 7 import ./rotm.bend as RM 8 import ../../lib/order.bend as O 9 import ./agree.bend as AG 10 import ../../lib/nat_list.bend as NL 11 12 # Nodes through a sequence of setters: a setter skips other ids and applies 13 # its field change to its own; a node's links after field changes. 14 # (source: tools/generators/tm_hand/rotn.src) 15 16 17 def skipl(-K: Data, +nl: List<&2, M.Node>, +id: Nat, +v: Nat, +j: Nat, +h: {Nat.is_eq(id, j) == False{} : Bool}) -> {ST.nd(K, SE.setl(K, nl, id, v), j) == ST.nd(K, nl, j) : M.Node}: 18 %Equal.sym(M.Node, ST.nd(K, SE.setl(K, nl, id, v), j), ST.pk(M.Node, Nat.is_eq(id, j), SE.modl(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), SE.ndl(K, nl, id, v, j)) : {_ == ST.nd(K, nl, j) : M.Node} 19 %Equal.sym(Bool, Nat.is_eq(id, j), False{}, h) : {ST.pk(M.Node, _, SE.modl(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) == ST.nd(K, nl, j) : M.Node} 20 {==} 21 22 def hitl(-K: Data, +nl: List<&2, M.Node>, +id: Nat, +v: Nat) -> {ST.nd(K, SE.setl(K, nl, id, v), id) == SE.modl(K, ST.nd(K, nl, id), v) : M.Node}: 23 %Equal.sym(M.Node, ST.nd(K, SE.setl(K, nl, id, v), id), ST.pk(M.Node, Nat.is_eq(id, id), SE.modl(K, ST.nd(K, nl, id), v), ST.nd(K, nl, id)), SE.ndl(K, nl, id, v, id)) : {_ == SE.modl(K, ST.nd(K, nl, id), v) : M.Node} 24 %Equal.sym(Bool, Nat.is_eq(id, id), True{}, N.is_eq_refl(id)) : {ST.pk(M.Node, _, SE.modl(K, ST.nd(K, nl, id), v), ST.nd(K, nl, id)) == SE.modl(K, ST.nd(K, nl, id), v) : M.Node} 25 {==} 26 27 def skipr(-K: Data, +nl: List<&2, M.Node>, +id: Nat, +v: Nat, +j: Nat, +h: {Nat.is_eq(id, j) == False{} : Bool}) -> {ST.nd(K, SE.setr(K, nl, id, v), j) == ST.nd(K, nl, j) : M.Node}: 28 %Equal.sym(M.Node, ST.nd(K, SE.setr(K, nl, id, v), j), ST.pk(M.Node, Nat.is_eq(id, j), SE.modr(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), SE.ndr(K, nl, id, v, j)) : {_ == ST.nd(K, nl, j) : M.Node} 29 %Equal.sym(Bool, Nat.is_eq(id, j), False{}, h) : {ST.pk(M.Node, _, SE.modr(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) == ST.nd(K, nl, j) : M.Node} 30 {==} 31 32 def hitr(-K: Data, +nl: List<&2, M.Node>, +id: Nat, +v: Nat) -> {ST.nd(K, SE.setr(K, nl, id, v), id) == SE.modr(K, ST.nd(K, nl, id), v) : M.Node}: 33 %Equal.sym(M.Node, ST.nd(K, SE.setr(K, nl, id, v), id), ST.pk(M.Node, Nat.is_eq(id, id), SE.modr(K, ST.nd(K, nl, id), v), ST.nd(K, nl, id)), SE.ndr(K, nl, id, v, id)) : {_ == SE.modr(K, ST.nd(K, nl, id), v) : M.Node} 34 %Equal.sym(Bool, Nat.is_eq(id, id), True{}, N.is_eq_refl(id)) : {ST.pk(M.Node, _, SE.modr(K, ST.nd(K, nl, id), v), ST.nd(K, nl, id)) == SE.modr(K, ST.nd(K, nl, id), v) : M.Node} 35 {==} 36 37 def skipp(-K: Data, +nl: List<&2, M.Node>, +id: Nat, +v: Nat, +j: Nat, +h: {Nat.is_eq(id, j) == False{} : Bool}) -> {ST.nd(K, SE.setp(K, nl, id, v), j) == ST.nd(K, nl, j) : M.Node}: 38 %Equal.sym(M.Node, ST.nd(K, SE.setp(K, nl, id, v), j), ST.pk(M.Node, Nat.is_eq(id, j), SE.modp(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), SE.ndp(K, nl, id, v, j)) : {_ == ST.nd(K, nl, j) : M.Node} 39 %Equal.sym(Bool, Nat.is_eq(id, j), False{}, h) : {ST.pk(M.Node, _, SE.modp(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) == ST.nd(K, nl, j) : M.Node} 40 {==} 41 42 def hitp(-K: Data, +nl: List<&2, M.Node>, +id: Nat, +v: Nat) -> {ST.nd(K, SE.setp(K, nl, id, v), id) == SE.modp(K, ST.nd(K, nl, id), v) : M.Node}: 43 %Equal.sym(M.Node, ST.nd(K, SE.setp(K, nl, id, v), id), ST.pk(M.Node, Nat.is_eq(id, id), SE.modp(K, ST.nd(K, nl, id), v), ST.nd(K, nl, id)), SE.ndp(K, nl, id, v, id)) : {_ == SE.modp(K, ST.nd(K, nl, id), v) : M.Node} 44 %Equal.sym(Bool, Nat.is_eq(id, id), True{}, N.is_eq_refl(id)) : {ST.pk(M.Node, _, SE.modp(K, ST.nd(K, nl, id), v), ST.nd(K, nl, id)) == SE.modp(K, ST.nd(K, nl, id), v) : M.Node} 45 {==} 46 47 def skipc(-K: Data, +nl: List<&2, M.Node>, +id: Nat, +v: Bool, +j: Nat, +h: {Nat.is_eq(id, j) == False{} : Bool}) -> {ST.nd(K, SE.setc(K, nl, id, v), j) == ST.nd(K, nl, j) : M.Node}: 48 %Equal.sym(M.Node, ST.nd(K, SE.setc(K, nl, id, v), j), ST.pk(M.Node, Nat.is_eq(id, j), SE.modc(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), SE.ndc(K, nl, id, v, j)) : {_ == ST.nd(K, nl, j) : M.Node} 49 %Equal.sym(Bool, Nat.is_eq(id, j), False{}, h) : {ST.pk(M.Node, _, SE.modc(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) == ST.nd(K, nl, j) : M.Node} 50 {==} 51 52 def hitc(-K: Data, +nl: List<&2, M.Node>, +id: Nat, +v: Bool) -> {ST.nd(K, SE.setc(K, nl, id, v), id) == SE.modc(K, ST.nd(K, nl, id), v) : M.Node}: 53 %Equal.sym(M.Node, ST.nd(K, SE.setc(K, nl, id, v), id), ST.pk(M.Node, Nat.is_eq(id, id), SE.modc(K, ST.nd(K, nl, id), v), ST.nd(K, nl, id)), SE.ndc(K, nl, id, v, id)) : {_ == SE.modc(K, ST.nd(K, nl, id), v) : M.Node} 54 %Equal.sym(Bool, Nat.is_eq(id, id), True{}, N.is_eq_refl(id)) : {ST.pk(M.Node, _, SE.modc(K, ST.nd(K, nl, id), v), ST.nd(K, nl, id)) == SE.modc(K, ST.nd(K, nl, id), v) : M.Node} 55 {==} 56 57 def skipa(-K: Data, +nl: List<&2, M.Node>, +q: Nat, +y: Nat, +dir: Bool, +j: Nat, +h: {Nat.is_eq(q, j) == False{} : Bool}) -> {ST.nd(K, RM.attn(K, nl, q, y, dir), j) == ST.nd(K, nl, j) : M.Node}: 58 match q dir: 59 case 0n +dir: 60 {==} 61 case 1n+i True{}: 62 skipl(K, nl, 1n+i, y, j, h) 63 case 1n+i False{}: 64 skipr(K, nl, 1n+i, y, j, h) 65 66 # the parent's node after attach: the child on its side 67 def moda(-K: Data, x: M.Node, +y: Nat, +dir: Bool) -> M.Node: 68 match dir: 69 case True{}: 70 SE.modl(K, x, y) 71 case False{}: 72 SE.modr(K, x, y) 73 74 def hita(-K: Data, +nl: List<&2, M.Node>, +i: Nat, +y: Nat, +dir: Bool) -> {ST.nd(K, RM.attn(K, nl, 1n+i, y, dir), 1n+i) == moda(K, ST.nd(K, nl, 1n+i), y, dir) : M.Node}: 75 match dir: 76 case True{}: 77 hitl(K, nl, 1n+i, y) 78 case False{}: 79 hitr(K, nl, 1n+i, y) 80 81 # ---- links after field changes ---- 82 83 84 def isn_pr(-K: Data, +x: M.Node, +a: Nat, +b0: Nat, +q0: Nat, +b: Nat, +p: Nat, +h: {ST.is_node(K, x, a, b0, q0) == True{} : Bool}) -> {ST.is_node(K, SE.modp(K, SE.modr(K, x, b), p), a, b, p) == True{} : Bool}: 85 match x: 86 case M.Free{f}: 87 Empty.absurd({ST.is_node(K, SE.modp(K, SE.modr(K, M.Free{f}, b), p), a, b, p) == True{} : Bool}, L.false_true(h)) 88 case M.N{c, +x1, +x2, +x3, k}: 89 L.and_intro(Nat.is_eq(x1, a), Bool.and(Nat.is_eq(b, b), Nat.is_eq(p, p)), L.and_left(Nat.is_eq(x1, a), Bool.and(Nat.is_eq(x2, b0), Nat.is_eq(x3, q0)), h), L.and_intro(Nat.is_eq(b, b), Nat.is_eq(p, p), N.is_eq_refl(b), N.is_eq_refl(p))) 90 91 def isn_pl(-K: Data, +x: M.Node, +a0: Nat, +b: Nat, +q0: Nat, +a: Nat, +p: Nat, +h: {ST.is_node(K, x, a0, b, q0) == True{} : Bool}) -> {ST.is_node(K, SE.modp(K, SE.modl(K, x, a), p), a, b, p) == True{} : Bool}: 92 match x: 93 case M.Free{f}: 94 Empty.absurd({ST.is_node(K, SE.modp(K, SE.modl(K, M.Free{f}, a), p), a, b, p) == True{} : Bool}, L.false_true(h)) 95 case M.N{c, +x1, +x2, +x3, k}: 96 L.and_intro(Nat.is_eq(a, a), Bool.and(Nat.is_eq(x2, b), Nat.is_eq(p, p)), N.is_eq_refl(a), L.and_intro(Nat.is_eq(x2, b), Nat.is_eq(p, p), L.and_left(Nat.is_eq(x2, b), Nat.is_eq(x3, q0), L.and_right(Nat.is_eq(x1, a0), Bool.and(Nat.is_eq(x2, b), Nat.is_eq(x3, q0)), h)), N.is_eq_refl(p))) 97 98 def isn_lp(-K: Data, +x: M.Node, +a0: Nat, +b: Nat, +q0: Nat, +a: Nat, +p: Nat, +h: {ST.is_node(K, x, a0, b, q0) == True{} : Bool}) -> {ST.is_node(K, SE.modl(K, SE.modp(K, x, p), a), a, b, p) == True{} : Bool}: 99 match x: 100 case M.Free{f}: 101 Empty.absurd({ST.is_node(K, SE.modl(K, SE.modp(K, M.Free{f}, p), a), a, b, p) == True{} : Bool}, L.false_true(h)) 102 case M.N{c, +x1, +x2, +x3, k}: 103 L.and_intro(Nat.is_eq(a, a), Bool.and(Nat.is_eq(x2, b), Nat.is_eq(p, p)), N.is_eq_refl(a), L.and_intro(Nat.is_eq(x2, b), Nat.is_eq(p, p), L.and_left(Nat.is_eq(x2, b), Nat.is_eq(x3, q0), L.and_right(Nat.is_eq(x1, a0), Bool.and(Nat.is_eq(x2, b), Nat.is_eq(x3, q0)), h)), N.is_eq_refl(p))) 104 105 def isn_rp(-K: Data, +x: M.Node, +a: Nat, +b0: Nat, +q0: Nat, +b: Nat, +p: Nat, +h: {ST.is_node(K, x, a, b0, q0) == True{} : Bool}) -> {ST.is_node(K, SE.modr(K, SE.modp(K, x, p), b), a, b, p) == True{} : Bool}: 106 match x: 107 case M.Free{f}: 108 Empty.absurd({ST.is_node(K, SE.modr(K, SE.modp(K, M.Free{f}, p), b), a, b, p) == True{} : Bool}, L.false_true(h)) 109 case M.N{c, +x1, +x2, +x3, k}: 110 L.and_intro(Nat.is_eq(x1, a), Bool.and(Nat.is_eq(b, b), Nat.is_eq(p, p)), L.and_left(Nat.is_eq(x1, a), Bool.and(Nat.is_eq(x2, b0), Nat.is_eq(x3, q0)), h), L.and_intro(Nat.is_eq(b, b), Nat.is_eq(p, p), N.is_eq_refl(b), N.is_eq_refl(p))) 111 112 def isn_p(-K: Data, +x: M.Node, +a: Nat, +b: Nat, +q0: Nat, +p: Nat, +h: {ST.is_node(K, x, a, b, q0) == True{} : Bool}) -> {ST.is_node(K, SE.modp(K, x, p), a, b, p) == True{} : Bool}: 113 match x: 114 case M.Free{f}: 115 Empty.absurd({ST.is_node(K, SE.modp(K, M.Free{f}, p), a, b, p) == True{} : Bool}, L.false_true(h)) 116 case M.N{c, +x1, +x2, +x3, k}: 117 L.and_intro(Nat.is_eq(x1, a), Bool.and(Nat.is_eq(x2, b), Nat.is_eq(p, p)), L.and_left(Nat.is_eq(x1, a), Bool.and(Nat.is_eq(x2, b), Nat.is_eq(x3, q0)), h), L.and_intro(Nat.is_eq(x2, b), Nat.is_eq(p, p), L.and_left(Nat.is_eq(x2, b), Nat.is_eq(x3, q0), L.and_right(Nat.is_eq(x1, a), Bool.and(Nat.is_eq(x2, b), Nat.is_eq(x3, q0)), h)), N.is_eq_refl(p))) 118 119 # the parent's links with the child on the path's side replaced 120 def isn_a(-K: Data, +x: M.Node, +lft: Bool, +c0: Nat, +s: Nat, +q: Nat, +y: Nat, +h: {ST.is_node(K, x, ST.pk(Nat, lft, c0, s), ST.pk(Nat, lft, s, c0), q) == True{} : Bool}) -> {ST.is_node(K, moda(K, x, y, lft), ST.pk(Nat, lft, y, s), ST.pk(Nat, lft, s, y), q) == True{} : Bool}: 121 match x lft: 122 case M.Free{f} +lft: 123 Empty.absurd({ST.is_node(K, moda(K, M.Free{f}, y, lft), ST.pk(Nat, lft, y, s), ST.pk(Nat, lft, s, y), q) == True{} : Bool}, L.false_true(h)) 124 case M.N{c, +x1, +x2, +x3, k} True{}: 125 L.and_intro(Nat.is_eq(y, y), Bool.and(Nat.is_eq(x2, s), Nat.is_eq(x3, q)), N.is_eq_refl(y), L.and_right(Nat.is_eq(x1, c0), Bool.and(Nat.is_eq(x2, s), Nat.is_eq(x3, q)), h)) 126 case M.N{c, +x1, +x2, +x3, k} False{}: 127 L.and_intro(Nat.is_eq(x1, s), Bool.and(Nat.is_eq(y, y), Nat.is_eq(x3, q)), L.and_left(Nat.is_eq(x1, s), Bool.and(Nat.is_eq(x2, c0), Nat.is_eq(x3, q)), h), L.and_intro(Nat.is_eq(y, y), Nat.is_eq(x3, q), N.is_eq_refl(y), L.and_right(Nat.is_eq(x2, c0), Nat.is_eq(x3, q), L.and_right(Nat.is_eq(x1, s), Bool.and(Nat.is_eq(x2, c0), Nat.is_eq(x3, q)), h)))) 128 129 # ---- agreement through the rotations' writes ---- 130 131 132 def attn_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node>, +q: Nat, +y: Nat, +dir: Bool, +hq: {NL.memn(q, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, RM.attn(K, nl, q, y, dir)) == True{} : Bool}: 133 match q dir: 134 case 0n +dir: 135 AG.agr_refl(~K, ~cmp, ~o, xs, nl) 136 case 1n+i True{}: 137 SE.setl_agr(~K, ~cmp, ~o, xs, nl, 1n+i, y, hq) 138 case 1n+i False{}: 139 SE.setr_agr(~K, ~cmp, ~o, xs, nl, 1n+i, y, hq) 140 141 142 # ids the left rotation does not write keep their nodes 143 def rotl_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node>, +x: Nat, +y: Nat, +b: Nat, +q: Nat, +dir: Bool, +hx: {NL.memn(x, xs) == False{} : Bool}, +hy: {NL.memn(y, xs) == False{} : Bool}, +hb: {NL.memn(b, xs) == False{} : Bool}, +hq: {NL.memn(q, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, RM.rotl_nl(K, nl, x, y, b, q, dir)) == True{} : Bool}: 144 +a1 = SE.setr_agr(~K, ~cmp, ~o, xs, nl, x, b, hx) 145 +a2 = SE.setp_agr(~K, ~cmp, ~o, xs, SE.setr(K, nl, x, b), b, x, hb) 146 +a3 = attn_agr(~K, ~cmp, ~o, xs, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir, hq) 147 +a4 = SE.setp_agr(~K, ~cmp, ~o, xs, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q, hy) 148 +a5 = SE.setl_agr(~K, ~cmp, ~o, xs, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x, hy) 149 +a6 = SE.setp_agr(~K, ~cmp, ~o, xs, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y, hx) 150 AG.agr_trans(~K, ~cmp, ~o, xs, nl, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), SE.setp(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), AG.agr_trans(~K, ~cmp, ~o, xs, nl, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), AG.agr_trans(~K, ~cmp, ~o, xs, nl, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), AG.agr_trans(~K, ~cmp, ~o, xs, nl, SE.setp(K, SE.setr(K, nl, x, b), b, x), RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), AG.agr_trans(~K, ~cmp, ~o, xs, nl, SE.setr(K, nl, x, b), SE.setp(K, SE.setr(K, nl, x, b), b, x), a1, a2), a3), a4), a5), a6) 151 152 153 def rotr_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node>, +x: Nat, +y: Nat, +b: Nat, +q: Nat, +dir: Bool, +hx: {NL.memn(x, xs) == False{} : Bool}, +hy: {NL.memn(y, xs) == False{} : Bool}, +hb: {NL.memn(b, xs) == False{} : Bool}, +hq: {NL.memn(q, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, RM.rotr_nl(K, nl, x, y, b, q, dir)) == True{} : Bool}: 154 +a1 = SE.setl_agr(~K, ~cmp, ~o, xs, nl, x, b, hx) 155 +a2 = SE.setp_agr(~K, ~cmp, ~o, xs, SE.setl(K, nl, x, b), b, x, hb) 156 +a3 = attn_agr(~K, ~cmp, ~o, xs, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir, hq) 157 +a4 = SE.setp_agr(~K, ~cmp, ~o, xs, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q, hy) 158 +a5 = SE.setr_agr(~K, ~cmp, ~o, xs, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x, hy) 159 +a6 = SE.setp_agr(~K, ~cmp, ~o, xs, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y, hx) 160 AG.agr_trans(~K, ~cmp, ~o, xs, nl, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), SE.setp(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), AG.agr_trans(~K, ~cmp, ~o, xs, nl, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), AG.agr_trans(~K, ~cmp, ~o, xs, nl, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), AG.agr_trans(~K, ~cmp, ~o, xs, nl, SE.setp(K, SE.setl(K, nl, x, b), b, x), RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), AG.agr_trans(~K, ~cmp, ~o, xs, nl, SE.setl(K, nl, x, b), SE.setp(K, SE.setl(K, nl, x, b), b, x), a1, a2), a3), a4), a5), a6) 161 162 # ---- the rotated nodes ---- 163 164 165 # x: its right child b, its parent y 166 def rotl_x(-K: Data, +nl: List<&2, M.Node>, +x: Nat, +y: Nat, +b: Nat, +q: Nat, +dir: Bool, +a: Nat, +hxn: {ST.is_node(K, ST.nd(K, nl, x), a, y, q) == True{} : Bool}, +nyx: {Nat.is_eq(y, x) == False{} : Bool}, +nqx: {Nat.is_eq(q, x) == False{} : Bool}, +nbx: {Nat.is_eq(b, x) == False{} : Bool}) -> {ST.is_node(K, ST.nd(K, RM.rotl_nl(K, nl, x, y, b, q, dir), x), a, b, y) == True{} : Bool}: 167 +e = Equal.trans(M.Node, ST.nd(K, SE.setp(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), x), SE.modp(K, ST.nd(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x), y), SE.modp(K, SE.modr(K, ST.nd(K, nl, x), b), y), hitp(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), L.subst(M.Node, z => {SE.modp(K, ST.nd(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x), y) == SE.modp(K, z, y) : M.Node}, ST.nd(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x), SE.modr(K, ST.nd(K, nl, x), b), Equal.trans(M.Node, ST.nd(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x), ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), x), SE.modr(K, ST.nd(K, nl, x), b), skipl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x, x, nyx), Equal.trans(M.Node, ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), x), ST.nd(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), x), SE.modr(K, ST.nd(K, nl, x), b), skipp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q, x, nyx), Equal.trans(M.Node, ST.nd(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), x), ST.nd(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), x), SE.modr(K, ST.nd(K, nl, x), b), skipa(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir, x, nqx), Equal.trans(M.Node, ST.nd(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), x), ST.nd(K, SE.setr(K, nl, x, b), x), SE.modr(K, ST.nd(K, nl, x), b), skipp(K, SE.setr(K, nl, x, b), b, x, x, nbx), hitr(K, nl, x, b))))), {==})) 168 L.subst(M.Node, z => {ST.is_node(K, z, a, b, y) == True{} : Bool}, SE.modp(K, SE.modr(K, ST.nd(K, nl, x), b), y), ST.nd(K, SE.setp(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), x), Equal.sym(M.Node, ST.nd(K, SE.setp(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), x), SE.modp(K, SE.modr(K, ST.nd(K, nl, x), b), y), e), isn_pr(K, ST.nd(K, nl, x), a, y, q, b, y, hxn)) 169 170 # y: its left child x, its parent q 171 def rotl_y(-K: Data, +nl: List<&2, M.Node>, +x: Nat, +y: Nat, +b: Nat, +q: Nat, +dir: Bool, +cc: Nat, +hyn: {ST.is_node(K, ST.nd(K, nl, y), b, cc, x) == True{} : Bool}, +nxy: {Nat.is_eq(x, y) == False{} : Bool}, +nqy: {Nat.is_eq(q, y) == False{} : Bool}, +nby: {Nat.is_eq(b, y) == False{} : Bool}) -> {ST.is_node(K, ST.nd(K, RM.rotl_nl(K, nl, x, y, b, q, dir), y), x, cc, q) == True{} : Bool}: 172 +e = Equal.trans(M.Node, ST.nd(K, SE.setp(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), y), ST.nd(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), y), SE.modl(K, SE.modp(K, ST.nd(K, nl, y), q), x), skipp(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y, y, nxy), Equal.trans(M.Node, ST.nd(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), y), SE.modl(K, ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y), x), SE.modl(K, SE.modp(K, ST.nd(K, nl, y), q), x), hitl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), L.subst(M.Node, z => {SE.modl(K, ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y), x) == SE.modl(K, z, x) : M.Node}, ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y), SE.modp(K, ST.nd(K, nl, y), q), Equal.trans(M.Node, ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y), SE.modp(K, ST.nd(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y), q), SE.modp(K, ST.nd(K, nl, y), q), hitp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), L.subst(M.Node, z => {SE.modp(K, ST.nd(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y), q) == SE.modp(K, z, q) : M.Node}, ST.nd(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y), ST.nd(K, nl, y), Equal.trans(M.Node, ST.nd(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y), ST.nd(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), y), ST.nd(K, nl, y), skipa(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir, y, nqy), Equal.trans(M.Node, ST.nd(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), y), ST.n 173 L.subst(M.Node, z => {ST.is_node(K, z, x, cc, q) == True{} : Bool}, SE.modl(K, SE.modp(K, ST.nd(K, nl, y), q), x), ST.nd(K, SE.setp(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), y), Equal.sym(M.Node, ST.nd(K, SE.setp(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), y), SE.modl(K, SE.modp(K, ST.nd(K, nl, y), q), x), e), isn_lp(K, ST.nd(K, nl, y), b, cc, x, x, q, hyn)) 174 175 # b, the moved subtree's root: its parent x 176 def rotl_b(-K: Data, +nl: List<&2, M.Node>, +x: Nat, +y: Nat, +b: Nat, +q: Nat, +dir: Bool, +b1: Nat, +b2: Nat, +hbn: {ST.is_node(K, ST.nd(K, nl, b), b1, b2, y) == True{} : Bool}, +nxb: {Nat.is_eq(x, b) == False{} : Bool}, +nyb: {Nat.is_eq(y, b) == False{} : Bool}, +nqb: {Nat.is_eq(q, b) == False{} : Bool}) -> {ST.is_node(K, ST.nd(K, RM.rotl_nl(K, nl, x, y, b, q, dir), b), b1, b2, x) == True{} : Bool}: 177 +e = Equal.trans(M.Node, ST.nd(K, SE.setp(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), b), ST.nd(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), b), SE.modp(K, ST.nd(K, nl, b), x), skipp(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y, b, nxb), Equal.trans(M.Node, ST.nd(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), b), ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), b), SE.modp(K, ST.nd(K, nl, b), x), skipl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x, b, nyb), Equal.trans(M.Node, ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), b), ST.nd(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), b), SE.modp(K, ST.nd(K, nl, b), x), skipp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q, b, nyb), Equal.trans(M.Node, ST.nd(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), b), ST.nd(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), b), SE.modp(K, ST.nd(K, nl, b), x), skipa(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir, b, nqb), Equal.trans(M.Node, ST.nd(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), b), SE.modp(K, ST.nd(K, SE.setr(K, nl, x, b), b), x), SE.modp(K, ST.nd(K, nl, b), x), hitp(K, SE.setr(K, nl, x, b), b, x), L.subst(M.Node, z => {SE.modp(K, ST.nd(K, SE.setr(K, nl, x, b), b), x) == SE.modp(K, z, x) : M.Node}, ST.nd(K, SE.setr(K, nl, x, b), b), ST.nd(K, nl, b), skipr(K, nl, x, b, b, nxb), {==})))))) 178 L.subst(M.Node, z => {ST.is_node(K, z, b1, b2, x) == True{} : Bool}, SE.modp(K, ST.nd(K, nl, b), x), ST.nd(K, SE.setp(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), b), Equal.sym(M.Node, ST.nd(K, SE.setp(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), b), SE.modp(K, ST.nd(K, nl, b), x), e), isn_p(K, ST.nd(K, nl, b), b1, b2, y, x, hbn)) 179 180 # q, the parent: y on the path's side 181 def rotl_q(-K: Data, +nl: List<&2, M.Node>, +x: Nat, +y: Nat, +b: Nat, +i: Nat, +lft: Bool, +s: Nat, +q2: Nat, +hqn: {ST.is_node(K, ST.nd(K, nl, 1n+i), ST.pk(Nat, lft, x, s), ST.pk(Nat, lft, s, x), q2) == True{} : Bool}, +nxq: {Nat.is_eq(x, 1n+i) == False{} : Bool}, +nyq: {Nat.is_eq(y, 1n+i) == False{} : Bool}, +nbq: {Nat.is_eq(b, 1n+i) == False{} : Bool}) -> {ST.is_node(K, ST.nd(K, RM.rotl_nl(K, nl, x, y, b, 1n+i, lft), 1n+i), ST.pk(Nat, lft, y, s), ST.pk(Nat, lft, s, y), q2) == True{} : Bool}: 182 +e = Equal.trans(M.Node, ST.nd(K, SE.setp(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), 1n+i, y, lft), y, 1n+i), y, x), x, y), 1n+i), ST.nd(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), 1n+i, y, lft), y, 1n+i), y, x), 1n+i), moda(K, ST.nd(K, nl, 1n+i), y, lft), skipp(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), 1n+i, y, lft), y, 1n+i), y, x), x, y, 1n+i, nxq), Equal.trans(M.Node, ST.nd(K, SE.setl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), 1n+i, y, lft), y, 1n+i), y, x), 1n+i), ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), 1n+i, y, lft), y, 1n+i), 1n+i), moda(K, ST.nd(K, nl, 1n+i), y, lft), skipl(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), 1n+i, y, lft), y, 1n+i), y, x, 1n+i, nyq), Equal.trans(M.Node, ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), 1n+i, y, lft), y, 1n+i), 1n+i), ST.nd(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), 1n+i, y, lft), 1n+i), moda(K, ST.nd(K, nl, 1n+i), y, lft), skipp(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), 1n+i, y, lft), y, 1n+i, 1n+i, nyq), Equal.trans(M.Node, ST.nd(K, RM.attn(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), 1n+i, y, lft), 1n+i), moda(K, ST.nd(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), 1n+i), y, lft), moda(K, ST.nd(K, nl, 1n+i), y, lft), hita(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), i, y, lft), L.subst(M.Node, z => {moda(K, ST.nd(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), 1n+i), y, lft) == moda(K, z, y, lft) : M.Node}, ST.nd(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), 1n+i), ST.nd(K, nl, 1n+i), Equal.trans(M.Node, ST.nd(K, SE.setp(K, SE.setr(K, nl, x, b), b, x), 1n+i), ST.nd(K, SE.setr(K, nl, x, b), 1n+i), ST.nd(K, nl, 1n+i), skipp(K, SE.setr(K, nl, x, b), b, x, 1n+i, nbq), skipr(K, nl, x, b, 1n+i, nxq)), {==}))))) 183 L.subst(M.Node, z => {ST.is_node(K, z, ST.pk(Nat, lft, y, s), ST.pk(Nat, lft, s, y), q2) == True{} : Bool}, moda(K, ST.nd(K, nl, 1n+i), y, lft), ST.nd(K, RM.rotl_nl(K, nl, x, y, b, 1n+i, lft), 1n+i), Equal.sym(M.Node, ST.nd(K, RM.rotl_nl(K, nl, x, y, b, 1n+i, lft), 1n+i), moda(K, ST.nd(K, nl, 1n+i), y, lft), e), isn_a(K, ST.nd(K, nl, 1n+i), lft, x, s, q2, y, hqn)) 184 185 # ---- the right rotation's nodes ---- 186 187 def rotr_x(-K: Data, +nl: List<&2, M.Node>, +x: Nat, +y: Nat, +b: Nat, +q: Nat, +dir: Bool, +cc: Nat, +hxn: {ST.is_node(K, ST.nd(K, nl, x), y, cc, q) == True{} : Bool}, +nyx: {Nat.is_eq(y, x) == False{} : Bool}, +nqx: {Nat.is_eq(q, x) == False{} : Bool}, +nbx: {Nat.is_eq(b, x) == False{} : Bool}) -> {ST.is_node(K, ST.nd(K, RM.rotr_nl(K, nl, x, y, b, q, dir), x), b, cc, y) == True{} : Bool}: 188 +e = Equal.trans(M.Node, ST.nd(K, SE.setp(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), x), SE.modp(K, ST.nd(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x), y), SE.modp(K, SE.modl(K, ST.nd(K, nl, x), b), y), hitp(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), L.subst(M.Node, z => {SE.modp(K, ST.nd(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x), y) == SE.modp(K, z, y) : M.Node}, ST.nd(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x), SE.modl(K, ST.nd(K, nl, x), b), Equal.trans(M.Node, ST.nd(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x), ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), x), SE.modl(K, ST.nd(K, nl, x), b), skipr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x, x, nyx), Equal.trans(M.Node, ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), x), ST.nd(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), x), SE.modl(K, ST.nd(K, nl, x), b), skipp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q, x, nyx), Equal.trans(M.Node, ST.nd(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), x), ST.nd(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), x), SE.modl(K, ST.nd(K, nl, x), b), skipa(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir, x, nqx), Equal.trans(M.Node, ST.nd(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), x), ST.nd(K, SE.setl(K, nl, x, b), x), SE.modl(K, ST.nd(K, nl, x), b), skipp(K, SE.setl(K, nl, x, b), b, x, x, nbx), hitl(K, nl, x, b))))), {==})) 189 L.subst(M.Node, z => {ST.is_node(K, z, b, cc, y) == True{} : Bool}, SE.modp(K, SE.modl(K, ST.nd(K, nl, x), b), y), ST.nd(K, SE.setp(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), x), Equal.sym(M.Node, ST.nd(K, SE.setp(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), x), SE.modp(K, SE.modl(K, ST.nd(K, nl, x), b), y), e), isn_pl(K, ST.nd(K, nl, x), y, cc, q, b, y, hxn)) 190 191 def rotr_y(-K: Data, +nl: List<&2, M.Node>, +x: Nat, +y: Nat, +b: Nat, +q: Nat, +dir: Bool, +aa: Nat, +hyn: {ST.is_node(K, ST.nd(K, nl, y), aa, b, x) == True{} : Bool}, +nxy: {Nat.is_eq(x, y) == False{} : Bool}, +nqy: {Nat.is_eq(q, y) == False{} : Bool}, +nby: {Nat.is_eq(b, y) == False{} : Bool}) -> {ST.is_node(K, ST.nd(K, RM.rotr_nl(K, nl, x, y, b, q, dir), y), aa, x, q) == True{} : Bool}: 192 +e = Equal.trans(M.Node, ST.nd(K, SE.setp(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), y), ST.nd(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), y), SE.modr(K, SE.modp(K, ST.nd(K, nl, y), q), x), skipp(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y, y, nxy), Equal.trans(M.Node, ST.nd(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), y), SE.modr(K, ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y), x), SE.modr(K, SE.modp(K, ST.nd(K, nl, y), q), x), hitr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), L.subst(M.Node, z => {SE.modr(K, ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y), x) == SE.modr(K, z, x) : M.Node}, ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y), SE.modp(K, ST.nd(K, nl, y), q), Equal.trans(M.Node, ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y), SE.modp(K, ST.nd(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y), q), SE.modp(K, ST.nd(K, nl, y), q), hitp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), L.subst(M.Node, z => {SE.modp(K, ST.nd(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y), q) == SE.modp(K, z, q) : M.Node}, ST.nd(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y), ST.nd(K, nl, y), Equal.trans(M.Node, ST.nd(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y), ST.nd(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), y), ST.nd(K, nl, y), skipa(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir, y, nqy), Equal.trans(M.Node, ST.nd(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), y), ST.n 193 L.subst(M.Node, z => {ST.is_node(K, z, aa, x, q) == True{} : Bool}, SE.modr(K, SE.modp(K, ST.nd(K, nl, y), q), x), ST.nd(K, SE.setp(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), y), Equal.sym(M.Node, ST.nd(K, SE.setp(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), y), SE.modr(K, SE.modp(K, ST.nd(K, nl, y), q), x), e), isn_rp(K, ST.nd(K, nl, y), aa, b, x, x, q, hyn)) 194 195 def rotr_b(-K: Data, +nl: List<&2, M.Node>, +x: Nat, +y: Nat, +b: Nat, +q: Nat, +dir: Bool, +b1: Nat, +b2: Nat, +hbn: {ST.is_node(K, ST.nd(K, nl, b), b1, b2, y) == True{} : Bool}, +nxb: {Nat.is_eq(x, b) == False{} : Bool}, +nyb: {Nat.is_eq(y, b) == False{} : Bool}, +nqb: {Nat.is_eq(q, b) == False{} : Bool}) -> {ST.is_node(K, ST.nd(K, RM.rotr_nl(K, nl, x, y, b, q, dir), b), b1, b2, x) == True{} : Bool}: 196 +e = Equal.trans(M.Node, ST.nd(K, SE.setp(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), b), ST.nd(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), b), SE.modp(K, ST.nd(K, nl, b), x), skipp(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y, b, nxb), Equal.trans(M.Node, ST.nd(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), b), ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), b), SE.modp(K, ST.nd(K, nl, b), x), skipr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x, b, nyb), Equal.trans(M.Node, ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), b), ST.nd(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), b), SE.modp(K, ST.nd(K, nl, b), x), skipp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q, b, nyb), Equal.trans(M.Node, ST.nd(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), b), ST.nd(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), b), SE.modp(K, ST.nd(K, nl, b), x), skipa(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir, b, nqb), Equal.trans(M.Node, ST.nd(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), b), SE.modp(K, ST.nd(K, SE.setl(K, nl, x, b), b), x), SE.modp(K, ST.nd(K, nl, b), x), hitp(K, SE.setl(K, nl, x, b), b, x), L.subst(M.Node, z => {SE.modp(K, ST.nd(K, SE.setl(K, nl, x, b), b), x) == SE.modp(K, z, x) : M.Node}, ST.nd(K, SE.setl(K, nl, x, b), b), ST.nd(K, nl, b), skipl(K, nl, x, b, b, nxb), {==})))))) 197 L.subst(M.Node, z => {ST.is_node(K, z, b1, b2, x) == True{} : Bool}, SE.modp(K, ST.nd(K, nl, b), x), ST.nd(K, SE.setp(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), b), Equal.sym(M.Node, ST.nd(K, SE.setp(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), q, y, dir), y, q), y, x), x, y), b), SE.modp(K, ST.nd(K, nl, b), x), e), isn_p(K, ST.nd(K, nl, b), b1, b2, y, x, hbn)) 198 199 def rotr_q(-K: Data, +nl: List<&2, M.Node>, +x: Nat, +y: Nat, +b: Nat, +i: Nat, +lft: Bool, +s: Nat, +q2: Nat, +hqn: {ST.is_node(K, ST.nd(K, nl, 1n+i), ST.pk(Nat, lft, x, s), ST.pk(Nat, lft, s, x), q2) == True{} : Bool}, +nxq: {Nat.is_eq(x, 1n+i) == False{} : Bool}, +nyq: {Nat.is_eq(y, 1n+i) == False{} : Bool}, +nbq: {Nat.is_eq(b, 1n+i) == False{} : Bool}) -> {ST.is_node(K, ST.nd(K, RM.rotr_nl(K, nl, x, y, b, 1n+i, lft), 1n+i), ST.pk(Nat, lft, y, s), ST.pk(Nat, lft, s, y), q2) == True{} : Bool}: 200 +e = Equal.trans(M.Node, ST.nd(K, SE.setp(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), 1n+i, y, lft), y, 1n+i), y, x), x, y), 1n+i), ST.nd(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), 1n+i, y, lft), y, 1n+i), y, x), 1n+i), moda(K, ST.nd(K, nl, 1n+i), y, lft), skipp(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), 1n+i, y, lft), y, 1n+i), y, x), x, y, 1n+i, nxq), Equal.trans(M.Node, ST.nd(K, SE.setr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), 1n+i, y, lft), y, 1n+i), y, x), 1n+i), ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), 1n+i, y, lft), y, 1n+i), 1n+i), moda(K, ST.nd(K, nl, 1n+i), y, lft), skipr(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), 1n+i, y, lft), y, 1n+i), y, x, 1n+i, nyq), Equal.trans(M.Node, ST.nd(K, SE.setp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), 1n+i, y, lft), y, 1n+i), 1n+i), ST.nd(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), 1n+i, y, lft), 1n+i), moda(K, ST.nd(K, nl, 1n+i), y, lft), skipp(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), 1n+i, y, lft), y, 1n+i, 1n+i, nyq), Equal.trans(M.Node, ST.nd(K, RM.attn(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), 1n+i, y, lft), 1n+i), moda(K, ST.nd(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), 1n+i), y, lft), moda(K, ST.nd(K, nl, 1n+i), y, lft), hita(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), i, y, lft), L.subst(M.Node, z => {moda(K, ST.nd(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), 1n+i), y, lft) == moda(K, z, y, lft) : M.Node}, ST.nd(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), 1n+i), ST.nd(K, nl, 1n+i), Equal.trans(M.Node, ST.nd(K, SE.setp(K, SE.setl(K, nl, x, b), b, x), 1n+i), ST.nd(K, SE.setl(K, nl, x, b), 1n+i), ST.nd(K, nl, 1n+i), skipp(K, SE.setl(K, nl, x, b), b, x, 1n+i, nbq), skipl(K, nl, x, b, 1n+i, nxq)), {==}))))) 201 L.subst(M.Node, z => {ST.is_node(K, z, ST.pk(Nat, lft, y, s), ST.pk(Nat, lft, s, y), q2) == True{} : Bool}, moda(K, ST.nd(K, nl, 1n+i), y, lft), ST.nd(K, RM.rotr_nl(K, nl, x, y, b, 1n+i, lft), 1n+i), Equal.sym(M.Node, ST.nd(K, RM.rotr_nl(K, nl, x, y, b, 1n+i, lft), 1n+i), moda(K, ST.nd(K, nl, 1n+i), y, lft), e), isn_a(K, ST.nd(K, nl, 1n+i), lft, x, s, q2, y, hqn)) 202