Stalmarck's method: x ≡ x → z, does z have to be true?

I have been researching Ståmarck's method 1. In the paper cited here, some rules are given. Rules are made of triplets (x, y, z) such that:

y $\to$ z $\equiv$ x

where x, y and z are booleans which values are either 0 (false) or 1 (true). And rules then infer a consequence (bottom part of the rule).

For example:

$$ \frac{(x, y, 1)}{x/1} $$

means that given a triplet (x, y, 1), x has to be 1 (true). This makes sense because if the expression is $ y \to 1 $, then regardless of the value of y, the expression will be true (1). Now my question is, given the following rule:

$$ \frac{(x, x, z)}{x/1} $$

Why is it not possible to infer that z = 1 as well? If the truth table of this expression is drawn, this is the result (bear in mind that the result has to be the same value as x for it to make sense):

x | z | x -> z ($ \equiv x $)

0 | 0 | 1

0 | 1 | 1

1 | 0 | 0

1 | 1 | 1

Clearly, the only line that does not immediately lead to a contradiction is the last one, and in this case z = 1 as well.

1 Sheeran, Mary, and Gunnar Stålmarck. "A tutorial on Stålmarck’s proof procedure for propositional logic." International Conference on Formal Methods in Computer-Aided Design. Springer, Berlin, Heidelberg, 1998.

Yes, you are right. Having $x \leftrightarrow (x \rightarrow z)$ one can deduce that $x\equiv 1$ and $z \equiv 1$.

In the paper you cite (the link is to another one btw.), rule 6 allows only to deduce that $x\equiv 1$ holds.

But then you have the triplet $(1,1,z)$ and you can apply rule 4 $\frac{(x,1,z)}{x/z}$ to deduce $z\equiv x$, i.e., $z \equiv 1$ holds, too.

I have also seen other publications that include the conclusion $z \equiv 1$ directly in rule 6.

StackExchange Computer Science Q#148335, answer score: 3