def rgo

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/random/bytes.bend:35

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend as SCR

35# reverse.go(xs, ys) = reverse(xs) ++ ys
36def rgo(+xs: List<&2, U32>, +ys: List<&2, U32>) -> {List.reverse.go(&2, U32, xs, ys) == SCR.append(rev(xs), ys) : List<&2, U32>}:
37  match xs:
38    case Nil{}:
39      {==}
40    case Con{+h, +t}:
41      Equal.trans(List<&2, U32>, List.reverse.go(&2, U32, t, Con{h, ys}), SCR.append(rev(t), Con{h, ys}), SCR.append(List.reverse.go(&2, U32, t, [h]), ys),
42        rgo(t, Con{h, ys}),
43        Equal.trans(List<&2, U32>, SCR.append(rev(t), Con{h, ys}), SCR.append(SCR.append(rev(t), [h]), ys), SCR.append(List.reverse.go(&2, U32, t, [h]), ys),
44          Equal.sym(List<&2, U32>, SCR.append(SCR.append(rev(t), [h]), ys), SCR.append(rev(t), SCR.append([h], ys)), app_assoc(rev(t), [h], ys)),
45          Equal.cong(List<&2, U32>, List<&2, U32>, l => SCR.append(l, ys), SCR.append(rev(t), [h]), List.reverse.go(&2, U32, t, [h]), Equal.sym(List<&2, U32>, List.reverse.go(&2, U32, t, [h]), SCR.append(rev(t), [h]), rgo(t, [h])))))