def shift_extent

stelliferous@0.0.2.0 · proofs/storage_address_bounds.bend:16

import Base
import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

16def shift_extent(depth: Nat) -> {WordEncoding.shift(depth,1n) == Shape.extent(depth) : Nat}:
17  match depth:
18    case 0n: {==}
19    case 1n+rest:
20      Equal.cong(Nat,Nat,Nat.double,WordEncoding.shift(rest,1n),Shape.extent(rest),shift_extent(rest))