Constrain Algorithm, August 31, 2021 Question 1,d

Question

Constrain(β5, ϕ3) follows the rule:  Constrain(β1, ϕ1) when xϕ == xβ ∧ β0 == 0
which results in Constrain (1,0)

Then Constrain(1, ϕ) = ϕ is applied and results in 0 i.e false.

I am not able to understand why the highlighted line is in the solution.
Please correct me if I overlooked the steps in the Constrain algorithm/solution.

Answer 1

Well, that line is just expanding beta5 and phi3 so that we can see that both start with the same variable c and that therefore the reduction rule you mentioned has to be applied. If you see that directly, you can, of course, omit that line.

Comments

Thank you, Professor