def tl.exp

bend-osdev-gf@0.1.1.0 · PROOF.bend:7887

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G
import bend-osdev-gf@0.1.1.0/tables.bend as T
import bend-osdev-array@0.1.0.1/array.bend as A
import bend-osdev-array@0.1.0.1/LAWS.bend as AL
import bend-osdev-gf@0.1.1.0/proof_tab.bend as GT
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

7887# an exponential through the table
7888def tl.exp(+f: G.Gf8Field, +l: List<&2, U32>, +i: U32, +hi: {Nat.is_lt(U32.to_nat(i), 510n) == True{} : Bool}) -> {T.Gf8Tab.exp(GT.gt.tab(f, l), i) == (GT.gt.tab(f, l), G.Gf8.exp(f, U32.to_nat(i))) : T.Gf8Tab & U32}:
7889  %Equal.sym(Array<U32> & U32, Array.get(U32, A.Arrays.of_list(U32, 9n, GT.gt.elist(510n, f, 0n), 0), i), (A.Arrays.of_list(U32, 9n, GT.gt.elist(510n, f, 0n), 0), A.Arrays.nth(U32, GT.gt.elist(510n, f, 0n), A.Arrays.index(9n, i), 0)), AL.of_list_get(U32, 9n, GT.gt.elist(510n, f, 0n), 0, GT.gt.hl_elist(f), GT.gt.hd9(), i)) : {T.gf8tab.exp.fin(_, A.Arrays.of_list(U32, 8n, l, 0)) == (GT.gt.tab(f, l), G.Gf8.exp(f, U32.to_nat(i))) : T.Gf8Tab & U32}
7890  %Equal.sym(Nat, A.Arrays.index(9n, i), U32.to_nat(i), AL.index_of_u32(9n, i, GT.gt.lt_add_left(2n, U32.to_nat(i), 510n, hi))) : {(T.Gf8Tab{A.Arrays.of_list(U32, 9n, GT.gt.elist(510n, f, 0n), 0), A.Arrays.of_list(U32, 8n, l, 0)}, A.Arrays.nth(U32, GT.gt.elist(510n, f, 0n), _, 0)) == (GT.gt.tab(f, l), G.Gf8.exp(f, U32.to_nat(i))) : T.Gf8Tab & U32}
7891  %Equal.sym(U32, A.Arrays.nth(U32, GT.gt.elist(510n, f, 0n), U32.to_nat(i), 0), G.Gf8.exp(f, Nat.add(U32.to_nat(i), 0n)), GT.gt.elist_nth(510n, f, 0n, U32.to_nat(i), hi)) : {(T.Gf8Tab{A.Arrays.of_list(U32, 9n, GT.gt.elist(510n, f, 0n), 0), A.Arrays.of_list(U32, 8n, l, 0)}, _) == (GT.gt.tab(f, l), G.Gf8.exp(f, U32.to_nat(i))) : T.Gf8Tab & U32}
7892  %Equal.sym(Nat, Nat.add(U32.to_nat(i), 0n), U32.to_nat(i), UL.nat_add_zero(U32.to_nat(i))) : {(T.Gf8Tab{A.Arrays.of_list(U32, 9n, GT.gt.elist(510n, f, 0n), 0), A.Arrays.of_list(U32, 8n, l, 0)}, G.Gf8.exp(f, _)) == (GT.gt.tab(f, l), G.Gf8.exp(f, U32.to_nat(i))) : T.Gf8Tab & U32}
7893  {==}