def reverse_go_length

qasim-bend-kit@0.1.0.2 · proof/AES_ZipLengthProof.bend:86

import Base

86def reverse_go_length(+xs: List<&2, U32>, +acc: List<&2, U32>) ->
87    {List.length(&2, U32, List.reverse.go(&2, U32, xs, acc)) ==
88     (List.length(&2, U32, acc) + List.length(&2, U32, xs) : Nat) : Nat}:
89    match xs:
90        case Nil{}:
91            Equal.sym(Nat, Nat.add(List.length(&2, U32, acc), 0n),
92                List.length(&2, U32, acc),
93                nat_add_zero_right(List.length(&2, U32, acc)))
94        case x <> tail:
95            Equal.trans(Nat,
96                List.length(&2, U32,
97                    List.reverse.go(&2, U32, x <> tail, acc)),
98                (List.length(&2, U32, x <> acc) +
99                    List.length(&2, U32, tail) : Nat),
100                (List.length(&2, U32, acc) +
101                    List.length(&2, U32, x <> tail) : Nat),
102                reverse_go_length(tail, x <> acc),
103                Equal.sym(Nat,
104                    (List.length(&2, U32, acc) +
105                        List.length(&2, U32, x <> tail) : Nat),
106                    (List.length(&2, U32, x <> acc) +
107                        List.length(&2, U32, tail) : Nat),
108                    nat_add_succ_right(List.length(&2, U32, acc),
109                        List.length(&2, U32, tail))))