Constant | Type |
---|---|
n2s | :num -> string |
s2n | :string -> num |
|- n2s = WFREC (@R. WF R ∧ ∀n r0 r. n ≠ 0 ∧ (r0 = n MOD 256) ∧ (r = if r0 = 0 then 256 else r0) ⇒ R ((n − r) DIV 256) n) (λn2s n. I (if n = 0 then "" else (let r0 = n MOD 256 in let r = if r0 = 0 then 256 else r0 in let s0 = n2s ((n − r) DIV 256) in STRING (CHR (r − 1)) s0)))
|- (s2n "" = 0) ∧ ∀c s. s2n (STRING c s) = s2n s * 256 + ORD c + 1
|- ∀P. (∀n. (∀r0 r. n ≠ 0 ∧ (r0 = n MOD 256) ∧ (r = if r0 = 0 then 256 else r0) ⇒ P ((n − r) DIV 256)) ⇒ P n) ⇒ ∀v. P v
|- ∀n. n2s n = if n = 0 then "" else (let r0 = n MOD 256 in let r = if r0 = 0 then 256 else r0 in let s0 = n2s ((n − r) DIV 256) in STRING (CHR (r − 1)) s0)
|- ∀n. s2n (n2s n) = n
|- n2s (s2n s) = s
|- (n2s x = n2s y) ⇔ (x = y)
|- (s2n x = s2n y) ⇔ (x = y)
|- ∀s. ∃n. s = n2s n
|- ∀n. ∃s. n = s2n s