A sixth element was added to each item, which indicates the local tree that the item is associated with. ~ is the default value, representing the lack of an index. t, t1, and t2 represent indices assigned to local trees. In our case they range from 0 to 3. * is a wildcard, representing any permissible value.
A seventh element was added, which is a boolean value indicating whether or not a third dimensional successor may yet be attached to the node.
Rules I1...I5 cover the two-dimensional inferences. Rules I6...I14 cover the three-dimensional inferences where the root of the rule is located at the head of its own local tree. Rule I15 covers the three-dimensional inference where the root of the rule is located at a leaf of its own local tree.
In all likelihood, rules I1...I4 could be compressed down to two rules and I6...I14 could be compressed down to one rule, using the same variable scheme that we used to compress the 3d-only inference rules. That would leave only 5 inference rules.
Axioms
======
A1: [x, i, ~, ~, i+1, t, False] x_i is a terminal leaf of local tree t
A2: [X, ~, ~, ~, ~, t, False] X is a nonterminal leaf of local tree t,
and also exists as a trivial tree
[Edit: I fixed A2 by changing the last element from True to False]
Inference Rules
========= =====
I1: [Z,i,~,~,n,t,*] [Y,n,j,k,l,t,*]
------------------------------- t = W->X(Z, Y)
[X,i,j,k,l,t,True]
I2: [Z,i,~,~,j,t,*] [Y,~,~,k,l,t,*]
------------------------------- t = W->X(Z, Y)
[X,i,j,k,l,t,True]
I3: [Y,i,j,k,m,t,*] [Z,m,~,~,l,t,*]
------------------------------- t = W->X(Y, Z)
[X, i, j, k, l, t, True]
I4: [Y,i,j,~,~,t,*] [Z,k,~,~,l,t,*]
------------------------------- t = W->X(Y, Z)
[X, i, j, k, l, t, True]
I5: [Y,i,j,k,l,t,*]
------------------ t = W->X(Y)
[X,i,j,k,l,t,True]
I6: [X,i,n,m,l,t1,*] [W,n,j,k,m,t2,True]
------------------------------------ t1 = W->X(*), t2 = *->W(*)
[W,i,j,k,l,t2,False]
I7: [X,i,j,~,~,t1,*] [W,~,~,k,l,t2,True]
------------------------------------ t1 = W->X(*), t2 = *->W(*)
[W,i,j,k,l,t2,False]
I8: [X,i,j,m,l,t1,*] [W,~,~,k,m,t2,True]
------------------------------------ t1 = W->X(*), t2 = *->W(*)
[W,i,j,k,l,t2,False]
I9: [X,~,~,k,l,t1,*] [W,i,j,~,~,t2,True]
------------------------------------ t1 = W->X(*), t2 = *->W(*)
[W,i,j,k,l,t2,False]
I10: [X,i,n,k,l,t1,*] [W,n,j,~,~,t2,True]
------------------------------------ t1 = W->X(*), t2 = *->W(*)
[W,i,j,k,l,t2,False]
I11: [X,~,~,m,l,t1,*] [W,i,j,k,m,t2,True]
------------------------------------ t1 = W->X(*), t2 = *->W(*)
[W,i,j,k,l,t2,False]
I12: [X,i,n,~,~,t1,*] [W,n,j,k,l,t2,True]
------------------------------------ t1 = W->X(*), t2 = *->W(*)
[W,i,j,k,l,t2,False]
I13: [X,~,~,~,~,t1,*] [W,i,j,k,l,t2,True]
------------------------------------ t1 = W->X(*), t2 = *->W(*)
[W,i,j,k,l,t2,False]
I14: [X,i,j,k,l,t1,*] [W,~,~,~,~,t2,True]
------------------------------------ t1 = W->X(*), t2 = *->W(*)
[W,i,j,k,l,t2,False]
I15: [X,i,j,k,l,t1,*]
-------------------- t1 = W->X(*), t2 = *->*(W)
[W,i,j,k,l,t2,False]