Gc abs2

concept itp_b = ~Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Const('hroot', UninterpretedSort('Object',)), Const('mroot', UninterpretedSort('Addr',)))
concept itp_d = ~Apply(Const('taddr', FunctionSort(UninterpretedSort('Addr',), BooleanSort())), Const('mroot', UninterpretedSort('Addr',)))
concept itp_c = Eq(Const('tnext', UninterpretedSort('Addr',)), Const('talloc', UninterpretedSort('Addr',)))
concept itp_e = (Eq(Const('talloc', UninterpretedSort('Addr',)), Const('fhi', UninterpretedSort('Addr',))) * Eq(Const('tnext', UninterpretedSort('Addr',)), Const('fhi', UninterpretedSort('Addr',))) * ~Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Const('hroot', UninterpretedSort('Object',)), Const('mroot', UninterpretedSort('Addr',))))
concept itp_f = (Eq(Const('tnext', UninterpretedSort('Addr',)), Const('talloc', UninterpretedSort('Addr',))) * ~Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Const('hroot', UninterpretedSort('Object',)), Const('mroot', UninterpretedSort('Addr',))))
concept itp_g = Eq(Const('thi', UninterpretedSort('Addr',)), Const('temp_addr', UninterpretedSort('Addr',)))
concept itp_h = (~Apply(Const('taddr', FunctionSort(UninterpretedSort('Addr',), BooleanSort())), Const('talloc', UninterpretedSort('Addr',))) * Apply(Const('<', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Const('talloc', UninterpretedSort('Addr',)), Const('thi', UninterpretedSort('Addr',))))
concept itp_i = (Eq(Const('tnext', UninterpretedSort('Addr',)), Const('talloc', UninterpretedSort('Addr',))) * ~Apply(Const('taddr', FunctionSort(UninterpretedSort('Addr',), BooleanSort())), Const('talloc', UninterpretedSort('Addr',))))
concept itp_j = ~Apply(Const('taddr', FunctionSort(UninterpretedSort('Addr',), BooleanSort())), Const('tnext', UninterpretedSort('Addr',)))
concept itp_k(V0) = (~Apply(Const('dom[m1]', FunctionSort(UninterpretedSort('Addr',), BooleanSort())), Const('tnext', UninterpretedSort('Addr',))) * Apply(Const('h1', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Object',), BooleanSort())), Const('hroot', UninterpretedSort('Object',)), Var('V0', UninterpretedSort('Object',))))
concept itp_l(V1) = (Eq(Const('tnext', UninterpretedSort('Addr',)), Const('talloc', UninterpretedSort('Addr',))) * Apply(Const('h1', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Object',), BooleanSort())), Const('hroot', UninterpretedSort('Object',)), Var('V1', UninterpretedSort('Object',))))
concept itp_m(V0, V1, V2) = (~Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Var('V1', UninterpretedSort('Object',)), Var('V0', UninterpretedSort('Addr',))) * Apply(Const('h1', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Object',), BooleanSort())), Var('V2', UninterpretedSort('Object',)), Var('V1', UninterpretedSort('Object',))) * Apply(Const('m1', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Var('V0', UninterpretedSort('Addr',)), Var('V0', UninterpretedSort('Addr',))) * Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Var('V2', UninterpretedSort('Object',)), Var('V0', UninterpretedSort('Addr',))) * Apply(Const('taddr', FunctionSort(UninterpretedSort('Addr',), BooleanSort())), Var('V0', UninterpretedSort('Addr',))))
concept itp_n(V0, V1) = (Eq(Const('talloc', UninterpretedSort('Addr',)), Const('fhi', UninterpretedSort('Addr',))) * Eq(Const('tnext', UninterpretedSort('Addr',)), Const('fhi', UninterpretedSort('Addr',))) * ~Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Const('hroot', UninterpretedSort('Object',)), Var('V0', UninterpretedSort('Addr',))) * Apply(Const('h1', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Object',), BooleanSort())), Var('V1', UninterpretedSort('Object',)), Const('hroot', UninterpretedSort('Object',))) * Apply(Const('m1', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Var('V0', UninterpretedSort('Addr',)), Var('V0', UninterpretedSort('Addr',))) * Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Var('V1', UninterpretedSort('Object',)), Var('V0', UninterpretedSort('Addr',))) * Apply(Const('taddr', FunctionSort(UninterpretedSort('Addr',), BooleanSort())), Var('V0', UninterpretedSort('Addr',))))
concept itp_o(V0, V1) = (~Apply(Const('dom[m0]', FunctionSort(UninterpretedSort('Addr',), BooleanSort())), Var('V0', UninterpretedSort('Addr',))) * Apply(Const('<', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Const('tnext', UninterpretedSort('Addr',)), Var('V0', UninterpretedSort('Addr',))) * Apply(Const('h0', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Object',), BooleanSort())), Var('V1', UninterpretedSort('Object',)), Var('V1', UninterpretedSort('Object',))) * Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Var('V1', UninterpretedSort('Object',)), Var('V0', UninterpretedSort('Addr',))))
concept itp_p(V1) = (~Apply(Const('dom[m0]', FunctionSort(UninterpretedSort('Addr',), BooleanSort())), Const('talloc', UninterpretedSort('Addr',))) * Apply(Const('h0', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Object',), BooleanSort())), Var('V1', UninterpretedSort('Object',)), Var('V1', UninterpretedSort('Object',))) * Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Var('V1', UninterpretedSort('Object',)), Const('talloc', UninterpretedSort('Addr',))))
concept itp_q = Apply(Const('<', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Const('tnext', UninterpretedSort('Addr',)), Const('mroot', UninterpretedSort('Addr',)))
concept itp_r = Eq(Const('tnext', UninterpretedSort('Addr',)), Const('mroot', UninterpretedSort('Addr',)))
concept itp_s(V2) = (Apply(Const('<', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Const('talloc', UninterpretedSort('Addr',)), Const('flo', UninterpretedSort('Addr',))) * Apply(Const('h0', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Object',), BooleanSort())), Var('V2', UninterpretedSort('Object',)), Const('obj', UninterpretedSort('Object',))) * Apply(Const('m0', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Const('talloc', UninterpretedSort('Addr',)), Const('talloc', UninterpretedSort('Addr',))) * Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Var('V2', UninterpretedSort('Object',)), Const('talloc', UninterpretedSort('Addr',))))
concept itp_t(V3) = (Apply(Const('<', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Const('talloc', UninterpretedSort('Addr',)), Const('thi', UninterpretedSort('Addr',))) * Apply(Const('h0', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Object',), BooleanSort())), Var('V3', UninterpretedSort('Object',)), Const('obj', UninterpretedSort('Object',))) * Apply(Const('m0', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Const('thi', UninterpretedSort('Addr',)), Const('talloc', UninterpretedSort('Addr',))) * Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Var('V3', UninterpretedSort('Object',)), Const('thi', UninterpretedSort('Addr',))))
concept itp_u(V3) = (Apply(Const('<', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Const('talloc', UninterpretedSort('Addr',)), Const('thi', UninterpretedSort('Addr',))) * Apply(Const('h0', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Object',), BooleanSort())), Var('V3', UninterpretedSort('Object',)), Const('hroot', UninterpretedSort('Object',))) * Apply(Const('m0', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Const('thi', UninterpretedSort('Addr',)), Const('talloc', UninterpretedSort('Addr',))) * Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Var('V3', UninterpretedSort('Object',)), Const('thi', UninterpretedSort('Addr',))))
concept itp_v(V0, V2) = (Eq(Const('thi', UninterpretedSort('Addr',)), Const('flo', UninterpretedSort('Addr',))) * Apply(Const('<', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Var('V0', UninterpretedSort('Addr',)), Const('flo', UninterpretedSort('Addr',))) * Apply(Const('h0', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Object',), BooleanSort())), Var('V2', UninterpretedSort('Object',)), Const('hroot', UninterpretedSort('Object',))) * Apply(Const('m0', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Var('V0', UninterpretedSort('Addr',)), Var('V0', UninterpretedSort('Addr',))) * Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Var('V2', UninterpretedSort('Object',)), Var('V0', UninterpretedSort('Addr',))))
concept itp_w(V2) = (Apply(Const('<', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Const('talloc', UninterpretedSort('Addr',)), Const('flo', UninterpretedSort('Addr',))) * Apply(Const('h0', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Object',), BooleanSort())), Var('V2', UninterpretedSort('Object',)), Const('hroot', UninterpretedSort('Object',))) * Apply(Const('m0', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Const('talloc', UninterpretedSort('Addr',)), Const('talloc', UninterpretedSort('Addr',))) * Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Var('V2', UninterpretedSort('Object',)), Const('talloc', UninterpretedSort('Addr',))))
concept itp_x(V3) = (Apply(Const('<', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Const('talloc', UninterpretedSort('Addr',)), Const('thi', UninterpretedSort('Addr',))) * Apply(Const('h0', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Object',), BooleanSort())), Var('V3', UninterpretedSort('Object',)), Const('hroot', UninterpretedSort('Object',))) * Apply(Const('m0', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Const('talloc', UninterpretedSort('Addr',)), Const('talloc', UninterpretedSort('Addr',))) * Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Var('V3', UninterpretedSort('Object',)), Const('talloc', UninterpretedSort('Addr',))))
concept itp_y(V1, V4, V2) = (Apply(Const('<', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Var('V2', UninterpretedSort('Addr',)), Const('thi', UninterpretedSort('Addr',))) * Apply(Const('<', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Const('tnext', UninterpretedSort('Addr',)), Var('V2', UninterpretedSort('Addr',))) * Apply(Const('h0', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Object',), BooleanSort())), Var('V4', UninterpretedSort('Object',)), Const('hroot', UninterpretedSort('Object',))) * Apply(Const('m0', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Var('V1', UninterpretedSort('Addr',)), Var('V2', UninterpretedSort('Addr',))) * Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Var('V4', UninterpretedSort('Object',)), Var('V1', UninterpretedSort('Addr',))))
concept itp_z(V2, V0) = (Eq(Const('tnext', UninterpretedSort('Addr',)), Const('talloc', UninterpretedSort('Addr',))) * Apply(Const('h0', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Object',), BooleanSort())), Var('V2', UninterpretedSort('Object',)), Const('hroot', UninterpretedSort('Object',))) * Apply(Const('m0', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Var('V0', UninterpretedSort('Addr',)), Const('talloc', UninterpretedSort('Addr',))) * Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Var('V2', UninterpretedSort('Object',)), Var('V0', UninterpretedSort('Addr',))))
concept itp_a0 = Apply(Const('<', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Const('tnext', UninterpretedSort('Addr',)), Const('temp_addr', UninterpretedSort('Addr',)))
concept itp_b0(V0, V1) = (~Apply(Const('dom[m1]', FunctionSort(UninterpretedSort('Addr',), BooleanSort())), Var('V0', UninterpretedSort('Addr',))) * Apply(Const('<', FunctionSort(UninterpretedSort('Addr',), UninterpretedSort('Addr',), BooleanSort())), Const('tnext', UninterpretedSort('Addr',)), Var('V0', UninterpretedSort('Addr',))) * Apply(Const('h1', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Object',), BooleanSort())), Var('V1', UninterpretedSort('Object',)), Var('V1', UninterpretedSort('Object',))) * Apply(Const('repr', FunctionSort(UninterpretedSort('Object',), UninterpretedSort('Addr',), BooleanSort())), Var('V1', UninterpretedSort('Object',)), Var('V0', UninterpretedSort('Addr',))))
concept itp_c0(V0) = (<(V0, tnext) * taddr(V0))
concept itp_d0(V2, V1, V0) = (h0(V1, V2) * repr(V1, V0) * ~dom[m0](V0))
concept itp_e0(V0, V1, V2) = (<(V0, tnext) * h0(V1, V2) * repr(V1, V0) * ~dom[m0](V0))