def tb.srev

bend-osdev-acpi@0.1.1.0 · PROOF_tables.bend:265

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W
import bend-osdev-acpi@0.1.1.0/rsdt.bend as R

265def tb.srev(+xs: List<&2, W.W64>) -> {xs == R.sl.rev(R.sl.rev(xs, Nil{}), Nil{}) : List<&2, W.W64>}:
266  %tb.srv(R.sl.rev(xs, Nil{}), Nil{}) : {xs == _ : List<&2, W.W64>}
267  %tb.srv(xs, Nil{}) : {xs == List.reverse.go(&2, W.W64, _, Nil{}) : List<&2, W.W64>}
268  revrev(W.W64, xs)