Gc abs

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 = (tnext = talloc)
concept itp_e = (talloc = fhi * tnext = fhi * ~repr(hroot, mroot))
concept itp_f = (tnext = talloc * ~repr(hroot, mroot))
concept itp_g = (thi = temp_addr)
concept itp_h = (~taddr(talloc) * <(talloc, thi))
concept itp_i = (tnext = talloc * ~taddr(talloc))
concept itp_j = (~taddr(tnext))
concept itp_k(V0) = (~dom[m1](tnext) * h1(hroot, V0))
concept itp_l(V1) = (tnext = talloc * h1(hroot, V1))
concept itp_m(V0, V1, V2) = (~repr(V1, V0) * h1(V2, V1) * m1(V0, V0) * repr(V2, V0) * taddr(V0))
concept itp_n(V0, V1) = (talloc = fhi * tnext = fhi * ~repr(hroot, V0) * h1(V1, hroot) * m1(V0, V0) * repr(V1, V0) * taddr(V0))
concept itp_o(V0, V1) = (~dom[m0](V0) * <(tnext, V0) * h0(V1, V1) * repr(V1, V0))
concept itp_p(V1) = (~dom[m0](talloc) * h0(V1, V1) * repr(V1, talloc))
concept itp_q = (<(tnext, mroot))
concept itp_r = (tnext = mroot)
concept itp_s(V2) = (<(talloc, flo) * h0(V2, obj) * m0(talloc, talloc) * repr(V2, talloc))
concept itp_t(V3) = (<(talloc, thi) * h0(V3, obj) * m0(thi, talloc) * repr(V3, thi))
concept itp_u(V3) = (<(talloc, thi) * h0(V3, hroot) * m0(thi, talloc) * repr(V3, thi))
concept itp_v(V0, V2) = (thi = flo * <(V0, flo) * h0(V2, hroot) * m0(V0, V0) * repr(V2, V0))
concept itp_w(V2) = (<(talloc, flo) * h0(V2, hroot) * m0(talloc, talloc) * repr(V2, talloc))
concept itp_x(V3) = (<(talloc, thi) * h0(V3, hroot) * m0(talloc, talloc) * repr(V3, talloc))
concept itp_y(V1, V4, V2) = (<(V2, thi) * <(tnext, V2) * h0(V4, hroot) * m0(V1, V2) * repr(V4, V1))
concept itp_z(V2, V0) = (tnext = talloc * h0(V2, hroot) * m0(V0, talloc) * repr(V2, V0))
concept itp_a0 = (<(tnext, temp_addr))
concept itp_b0(V0, V1) = (~dom[m1](V0) * <(tnext, V0) * h1(V1, V1) * repr(V1, V0))