- ((id ^ ((n + (S O)) + (S O))) ')
- = ((id ^ ((n + (S (S O))))) ') by _.
- = ((id ^ (S (n + S O))) ') by _.
- = ((id · (id ^ (n + (S O)))) ') by _.
- = ((id ' · (id ^ (n + (S O)))) ⊕ (id · (id ^ (n + (S O))) ')) by _.
- alias symbol "plus" (instance 4) = "natural plus".
- = ((R1 · (id ^ (n + (S O)))) ⊕ (id · ((i (n + S O)) · (id ^ n)))) by _.
- = ((R1 · (id ^ (n + (S O)))) ⊕ (((i (n + S O)) · id · (id ^ n)))) by _.
- alias symbol "plus" (instance 8) = "natural plus".
- = ((R1 · (id ^ (n + (S O)))) ⊕ ((i (n + S O)) · (id ^ (n + (S O))))) by _.
- = ((i R1 · (id ^ (n + (S O)))) ⊕ ((i (n + S O)) · (id ^ (n + (S O))))) by _.
- alias symbol "plus" = "natural plus".
- cut (((i R1 · (id ^ (n + (S O)))) ⊕ ((i (n + S O)) · (id ^ (n + (S O))))) =
- (((i R1 ⊕ (i (plus n (S O)))) · (id ^ (n + (S O))))));[| by _ done;]
- unfold F_OF_nat in Hcut;
- rewrite > Hcut;
- = (((i R1 ⊕ (i (plus n (S O)))) · (id ^ (n + (S O))))) by _.
- = ((i (n + S O + S O)) · (id ^ (n + S O))) by _
+ ((id ^ ((n + 1) + 1)) ')
+ = ((id ^ ((n + (S 1)))) ') by _.
+ = ((id ^ (S (n + 1))) ') by _.
+ = ((id · (id ^ (n + 1))) ') by _.
+ = ((id ' · (id ^ (n + 1))) + (id · (id ^ (n + 1)) ')) by _.
+ alias symbol "plus" (instance 1) = "function plus".
+ = ((R1 · (id ^ (n + 1))) + (id · (((n + 1)) · (id ^ n)))) by _.
+ = ((R1 · (id ^ (n + 1))) + (((n + 1) · id · (id ^ n)))) by _.
+ = ((R1 · (id ^ (n + 1))) + ((n + 1) · (id ^ (1 + n)))) by _.
+ = ((R1 · (id ^ (n + 1))) + ((n + 1) · (id ^ (n + 1)))) by _.
+ alias symbol "plus" (instance 2) = "function plus".
+ = (((R1 + (n + 1))) · (id ^ (n + 1))) by _.
+ = ((1 + (n + 1)) · (id ^ (n + 1))) by _;
+ = ((n + 1 + 1) · (id ^ (n + 1))) by _