Originally Posted by

**samantha12** I'm confused as to how you knew that you could only add /s, because the x is not defined?

inference rule: if x is a A-theorem, then so is x/

The rule says that if one starts from x, one can only add / to it.

And in the second example again how you knew the definition of x and y?

One proves the following theorems in sequence. I'll write the corresponding values of x and y from the rule next to the theorem provided it is not an axiom of the second system (i.e., a theorem of the first system).

Code:

#1. 0/ Axiom
#2. 0// Axiom
#3. [0/>0//] x = 0/ (#1), y = 0// (#2)
#4. 0 Axiom
#5. [0>0] x = 0 (#4), y = 0 (#4)
#6. [[0/>0//]>[0>0]] x = [0/>0//] (#3), y = [0>0] (#5)
#7. 0/// Axiom
#8. [[[0/>0//]>[0>0]]>0///] x = [[0/>0//]>[0>0]] (#6), y = 0/// (#7)