ProofTab.gt.fill_exp: def of bend-osdev-gf@0.1.1.0 Import: import bend-osdev-gf@0.1.1.0/proof_tab.bend as ProofTab Lines 204-211 of bend-osdev-gf@0.1.1.0/proof_tab.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&start_line=204&end_line=211 import Base 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/gf.bend as G import bend-osdev-gf@0.1.1.0/tables.bend as T def gt.fill_exp(n: Nat, +xs: List<&2, U32>, +f: G.Gf8Field, +k: Nat, +hl: {List.length(&2, U32, xs) == A.Arrays.slots(9n) : Nat}) -> {T.gf8tab.fill.exp(n, A.Arrays.of_list(U32, 9n, xs, 0), f, G.Gf8.exp(f, k), U32.from_nat(k)) == A.Arrays.of_list(U32, 9n, gt.fe(n, xs, f, k), 0) : Array}: match n: case 0n: {==} case 1n+j: %Equal.sym(U32, U32.add(U32.from_nat(k), 1), U32.inc(U32.from_nat(k)), gt.add_one(U32.from_nat(k))) : {T.gf8tab.fill.exp(j, Array.set(U32, A.Arrays.of_list(U32, 9n, xs, 0), U32.from_nat(k), G.Gf8.exp(f, k)), f, G.Gf8.mul(f, G.Gf8.gen(f), G.Gf8.exp(f, k)), _) == A.Arrays.of_list(U32, 9n, gt.fe(j, List.set(&2, U32, xs, A.Arrays.index(9n, U32.from_nat(k)), G.Gf8.exp(f, k)), f, 1n+k), 0) : Array} %Equal.sym(Array, Array.set(U32, A.Arrays.of_list(U32, 9n, xs, 0), U32.from_nat(k), G.Gf8.exp(f, k)), A.Arrays.of_list(U32, 9n, List.set(&2, U32, xs, A.Arrays.index(9n, U32.from_nat(k)), G.Gf8.exp(f, k)), 0), AL.of_list_set(U32, 9n, xs, 0, hl, gt.hd9(), U32.from_nat(k), G.Gf8.exp(f, k))) : {T.gf8tab.fill.exp(j, _, f, G.Gf8.mul(f, G.Gf8.gen(f), G.Gf8.exp(f, k)), U32.inc(U32.from_nat(k))) == A.Arrays.of_list(U32, 9n, gt.fe(j, List.set(&2, U32, xs, A.Arrays.index(9n, U32.from_nat(k)), G.Gf8.exp(f, k)), f, 1n+k), 0) : Array} gt.fill_exp(j, List.set(&2, U32, xs, A.Arrays.index(9n, U32.from_nat(k)), G.Gf8.exp(f, k)), f, 1n+k, gt.hl_set(9n, xs, A.Arrays.index(9n, U32.from_nat(k)), G.Gf8.exp(f, k), hl)) Uses (24): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.set 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=List.length https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.set https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.inc https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/LAWS.bend&name=of_list_set 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.of_list https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.slots 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=Gf8.gen https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8.mul 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.add_one https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&name=gt.fe 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_set https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/tables.bend&name=gf8tab.fill.exp