| gndx0.last = mkgnode(nd, m0, boolvar, boolvar0), gstore2[n1] = groupblock(gndx, lax, 0), gstore2[nx.last] = groupblock(gndx0, lax0, m), ¬ boolvar0, remove-refsize0(gstore1) = gstore1, elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, jro1 < jmaxino, p_os < pmaxino, fi2.inos < jmaxino, fi1.inos < pmaxino, inv(groupblock(gndx0, lax0, m)), inv(gstore2 \ jro0), inv(gstore1), refsize-cons(gstore2, range fi2), refsize-cons(gstore1, range fi1), ri-cons(fi2, nodes(gstore2 ↓, jro0)), ri-inj(fi2), ri-inj(fi1), valid-journal-head(nx, gstore2, jro0), nx.last ∈ gstore2, n1 ∈ gstore2, n1 ∈ gstore1, n1 ∈ dom gstore2 ∪ jro0, pmaxino ≤ jmaxino, fi2.lebs ⊆ dom gstore2, fi1.lebs ⊆ dom gstore1 ⊦ #(dom gstore2 ∪ jro0) = 0, nx.last = n1, gndx0 = [], jmaxino = 0, nx = [], pmaxino = 0, dom gstore2 ∪ jro0 = ∅, dups(nx), n1 ∈ nx |
gndx0.last = mkgnode(nd, m0, boolvar, false), gstore2[nx.last] = groupblock(gndx0, lax0, m), gstore2[n1] = groupblock(gndx, lax, 0), remove-refsize0(gstore1) = gstore1, elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, fi1.inos < pmaxino, fi2.inos < jmaxino, p_os < pmaxino, jro1 < jmaxino, inv(gstore1), inv(gstore2 \ jro0), inv(groupblock(gndx0, lax0, m)), refsize-cons(gstore1, range fi1), refsize-cons(gstore2, range fi2), ri-cons(fi2, nodes(gstore2 ↓, jro0)), ri-inj(fi1), ri-inj(fi2), valid-journal-head(nx, gstore2, jro0), n1 ∈ dom gstore2 ∪ jro0, n1 ∈ gstore1, n1 ∈ gstore2, nx.last ∈ gstore2, pmaxino ≤ jmaxino, fi1.lebs ⊆ dom gstore1, fi2.lebs ⊆ dom gstore2 ⊦ #(dom gstore2 ∪ jro0) = 0, nx.last = n1, gndx0 = [], jmaxino = 0, nx = [], pmaxino = 0, dom gstore2 ∪ jro0 = ∅, dups(nx), n1 ∈ nx