~/jendhub

def rev_twice

bend-osdev-bpf@0.1.0.0 · PROOF.bend:514

import bend-osdev-bpf@0.1.0.0/PROOF.bend as PROOF
import Base

514# reversing twice gives the list back
515def rev_twice(-A: Data, +xs: List<&2, A>) -> {List.reverse.go(&2, A, List.reverse.go(&2, A, xs, Nil{}), Nil{}) == xs : List<&2, A>}:
516  Equal.trans(List<&2, A>, List.reverse.go(&2, A, List.reverse.go(&2, A, xs, Nil{}), Nil{}), List.append(&2, A, xs, Nil{}), xs, rev_rr(A, xs, Nil{}, Nil{}), app_nil(A, xs))

Uses (6)

Used by (1)