def len_rev

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bytes.bend:96

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR

96def len_rev(xs: List<&2, U32>) -> {List.length(&2, U32, List.reverse(&2, U32, xs)) == List.length(&2, U32, xs) : Nat}:
97  match xs:
98    case Nil{}:
99      {==}
100    case +x <> +t:
101      %Equal.sym(List<&2, U32>, List.reverse(&2, U32, x <> t), List.append(&2, U32, List.reverse(&2, U32, t), [x]), rev_cons(x, t)) : {List.length(&2, U32, _) == 1n+List.length(&2, U32, t) : Nat}
102      %Equal.sym(Nat, List.length(&2, U32, List.append(&2, U32, List.reverse(&2, U32, t), [x])), Nat.add(List.length(&2, U32, List.reverse(&2, U32, t)), List.length(&2, U32, [x])), len_app(List.reverse(&2, U32, t), [x])) : {_ == 1n+List.length(&2, U32, t) : Nat}
103      %Equal.sym(Nat, List.length(&2, U32, List.reverse(&2, U32, t)), List.length(&2, U32, t), len_rev(t)) : {Nat.add(_, List.length(&2, U32, [x])) == 1n+List.length(&2, U32, t) : Nat}
104      %Equal.sym(Nat, 1n+List.length(&2, U32, t), Nat.add(List.length(&2, U32, t), 1n), SR.succ_add(1n, List.length(&2, U32, t))) : {Nat.add(List.length(&2, U32, t), 1n) == _ : Nat}
105      {==}