Proof step 15 from proof adr-in-index-node-key (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  # gndx1 = # lax1, ri[nodes(gstore ↓, ginval)[@(n, n0, n1)].key] = @(n, n0, n1), gstore[n] = groupblock(gndx0 + mkgnode(nd, m, boolvar, boolvar0) ' + gndx1, lax0 + @(n0, n1) ' + lax1, m0), inv(groupblock(gndx0 + mkgnode(nd, m, boolvar, boolvar0) ' + gndx1, lax0 + @(n0, n1) ' + lax1, m0)), n ∈ gstore, nodes(gstore ↓, ginval)[@(n, n0, n1)].key ∈ ri, @(n0, n1) ∈ prefixn(valid-group-nodes(gndx0 + mkgnode(nd, m, boolvar, boolvar0) ' + gndx1), lax0 + @(n0, n1) ' + lax1), nodes(gstore ↓, ginval)[@(n, n0, n1)].key.data? → nodes(gstore ↓, ginval)[@(n, n0, n1)].data?, nodes(gstore ↓, ginval)[@(n, n0, n1)].key.dentry? → nodes(gstore ↓, ginval)[@(n, n0, n1)].dentry?, nodes(gstore ↓, ginval)[@(n, n0, n1)].key.inode? → nodes(gstore ↓, ginval)[@(n, n0, n1)].inode? ∧ nodes(gstore ↓, ginval)[@(n, n0, n1)].key.ino ≠ 0 ⊦ n ∈ ginval, nd.key ∈ ri ∧ ri[nd.key] = @(n, n0, n1)

Rule argument

Additional information