#complexity O(n) let strlen-nullterm = λ str : &[Char~Ascii~machine::Word] ~ & ~ machine::Address ~ machine::Word -> ℤ ~ ℤ_2^64 ~ machine::UInt64 ~ machine::Word { let mut len = 0; while ( @str ) { ! len (i+ len 1); ! str (i+ str 1); } len; }; #complexity O(1) let strlen-lenprefix = λ str : &[Char~Ascii~machine::Word] ~ & ~ &{ len : ℤ_2^64 ~ machine::UInt64 ~ machine::Word, data : [machine::Word] } ~ machine::Address ~ machine::Word -> ℤ ~ ℤ_2^64 ~ machine::UInt64 ~ machine::Word { str.len };