def ud.fin.t

bend-osdev-u32@0.1.0.0 · PROOF.bend:1755

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

1755def ud.fin.t(+p: Nat, +q: Word(p), +bw: Word(32n), +a0: Bool, +rw: Word(32n), +x: Nat, +x2: Nat, +R1: Nat, +ex: {Nat.add(U.U32Nat.bit(a0), Nat.double(x)) == x2 : Nat}, +i1: {Nat.add(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)), Word.to_nat(32n, rw)) == x : Nat}, kp: {Nat.add(R1, Nat.mul(U.U32Nat.bit(True{}), Word.to_nat(32n, bw))) == Nat.add(U.U32Nat.bit(a0), Nat.double(Word.to_nat(32n, rw))) : Nat} & {Nat.is_lt(R1, Word.to_nat(32n, bw)) == True{} : Bool}) -> {Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), Word.to_nat(32n, bw)), R1) == x2 : Nat} & {Nat.is_lt(R1, Word.to_nat(32n, bw)) == True{} : Bool}:
1756  (+k1, +k2) = kp
1757  (Equal.trans(Nat, Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), Word.to_nat(32n, bw)), R1), Nat.add(U.U32Nat.bit(a0), Nat.double(x)), x2, Equal.trans(Nat, Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), Word.to_nat(32n, bw)), R1), Nat.add(U.U32Nat.bit(a0), Nat.double(Nat.add(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)), Word.to_nat(32n, rw)))), Nat.add(U.U32Nat.bit(a0), Nat.double(x)), Equal.trans(Nat, Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), Word.to_nat(32n, bw)), R1), Nat.add(Nat.add(U.U32Nat.bit(a0), Nat.double(Word.to_nat(32n, rw))), Nat.double(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)))), Nat.add(U.U32Nat.bit(a0), Nat.double(Nat.add(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)), Word.to_nat(32n, rw)))), Equal.trans(Nat, Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), Word.to_nat(32n, bw)), R1), Nat.add(Nat.add(R1, Nat.mul(1n, Word.to_nat(32n, bw))), Nat.double(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)))), Nat.add(Nat.add(U.U32Nat.bit(a0), Nat.double(Word.to_nat(32n, rw))), Nat.double(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)))), ur.r35(Word.to_nat(p, q), Word.to_nat(32n, bw), R1), Equal.cong(Nat, Nat, zz => Nat.add(zz, Nat.double(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)))), Nat.add(R1, Nat.mul(1n, Word.to_nat(32n, bw))), Nat.add(U.U32Nat.bit(a0), Nat.double(Word.to_nat(32n, rw))), k1)), ur.r36(U.U32Nat.bit(a0), Word.to_nat(32n, rw), Word.to_nat(p, q), Word.to_nat(32n, bw))), Equal.cong(Nat, Nat, zz => Nat.add(U.U32Nat.bit(a0), Nat.double(zz)), Nat.add(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)), Word.to_nat(32n, rw)), x, i1)), ex), k2)