AESZipLengthProof.reverse_go_length: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend as AESZipLengthProof
Lines 86-109 of qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&start_line=86&end_line=109

import Base

def reverse_go_length(+xs: List<&2, U32>, +acc: List<&2, U32>) ->
    {List.length(&2, U32, List.reverse.go(&2, U32, xs, acc)) ==
     (List.length(&2, U32, acc) + List.length(&2, U32, xs) : Nat) : Nat}:
    match xs:
        case Nil{}:
            Equal.sym(Nat, Nat.add(List.length(&2, U32, acc), 0n),
                List.length(&2, U32, acc),
                nat_add_zero_right(List.length(&2, U32, acc)))
        case x <> tail:
            Equal.trans(Nat,
                List.length(&2, U32,
                    List.reverse.go(&2, U32, x <> tail, acc)),
                (List.length(&2, U32, x <> acc) +
                    List.length(&2, U32, tail) : Nat),
                (List.length(&2, U32, acc) +
                    List.length(&2, U32, x <> tail) : Nat),
                reverse_go_length(tail, x <> acc),
                Equal.sym(Nat,
                    (List.length(&2, U32, acc) +
                        List.length(&2, U32, x <> tail) : Nat),
                    (List.length(&2, U32, x <> acc) +
                        List.length(&2, U32, tail) : Nat),
                    nat_add_succ_right(List.length(&2, U32, acc),
                        List.length(&2, U32, tail))))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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.reverse.go
  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=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&name=nat_add_succ_right
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&name=nat_add_zero_right