~/jendhub

def sp.snd_go

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:155

import bend-osdev-cipher-modes@0.1.0.0/PROOF.bend as PROOF
import Base

155def sp.snd_go(n: Nat, m: Nat, d1: Nat, d2: Nat, r: Nat) -> {Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d1, r)) == Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d2, r)) : Nat}:
156  match n:
157    case 0n:
158      {==}
159    case 1n+np:
160      match m:
161        case 0n:
162          sp.snd_go(np, r, 1n+d1, 1n+d2, 0n)
163        case 1n+mp:
164          sp.snd_go(np, mp, d1, d2, 1n+r)

Uses (3)

Used by (1)