(* ---------------------------------------------------------- *)
(* --- Global Definitions                                 --- *)
(* ---------------------------------------------------------- *)
theory Axiomatic

use import bool.Bool
use import int.Int
use import int.ComputerDivision
use import real.RealInfix
use import qed.Arith
use import map.Map
use import memory.Memory

predicate p_Length_of_str_is (mchar_0 : map addr int)
    (malloc_0 : map int int) (s_0 : addr) (n_0 : int) =
    let x_0 = s_0.base in let x_1 = s_0.offset in (0 <= n_0) /\
    ((valid_rw malloc_0 s_0 (1 + n_0))) /\
    (0 = mchar_0[{ s_0 with offset = n_0 + x_1 }]) /\
    (forall k_0 : int. (k_0 < n_0) -> (0 <= k_0) ->
     (0 <> mchar_0[{ s_0 with offset = k_0 + x_1 }]))

end