PROOF.tl.exp: def of bend-osdev-gf@0.1.1.0
Import: import bend-osdev-gf@0.1.1.0/PROOF.bend as PROOF
Lines 7887-7893 of bend-osdev-gf@0.1.1.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&start_line=7887&end_line=7893

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

# an exponential through the table
def 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}:
  %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}
  %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}
  %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}
  %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}
  {==}

Uses (29):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=index_of_u32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=of_list_get
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.index
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.nth
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8.exp
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8Field
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&name=gt.elist
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&name=gt.elist_nth
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&name=gt.hd9
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&name=gt.hl_elist
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&name=gt.lt_add_left
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&name=gt.tab
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/tables.bend&name=Gf8Tab
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/tables.bend&name=Gf8Tab.exp
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/tables.bend&name=gf8tab.exp.fin
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_zero