~/jendhub

def rev_cons

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

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

47# rev(b :: acc) ++ ts = rev(acc) ++ (b :: ts)
48def rev_cons(+b: U32, +acc: List<&2, U32>, +ts: List<&2, U32>) -> {SCR.append(rev(Con{b, acc}), ts) == SCR.append(rev(acc), Con{b, ts}) : List<&2, U32>}:
49  Equal.trans(List<&2, U32>, SCR.append(List.reverse.go(&2, U32, acc, [b]), ts), SCR.append(SCR.append(rev(acc), [b]), ts), SCR.append(rev(acc), Con{b, ts}),
50    Equal.cong(List<&2, U32>, List<&2, U32>, l => SCR.append(l, ts), List.reverse.go(&2, U32, acc, [b]), SCR.append(rev(acc), [b]), rgo(acc, [b])),
51    app_assoc(rev(acc), [b], ts))

Uses (9)

Used by (2)