-apply rule (⇒_e ((∀n.(n + O) = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (∀n.(n + O) = n ⇒ ((S n) + O) = (S n)));
- [ apply rule (⇒_e ((O + O) = O ⇒ (∀n.n + O = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (O + O = O));
+apply rule (⇒#e ((∀n.(n + O) = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (∀n.(n + O) = n ⇒ ((S n) + O) = (S n)));
+ [ apply rule (⇒#e ((O + O) = O ⇒ (∀n.n + O = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (O + O = O));
- | apply rule (∀_i {n} (n + O = n ⇒ ((S n) + O) = (S n)));
- apply rule (⇒_i [H] (((S n) + O) = (S n)));
- apply rule (⇒_e ((S (n + O)) = (S n) ⇒ ((S n) + O) = (S n)) ((S (n + O)) = (S n)));
- [ apply rule (⇒_e (((S n) + O) =(S (n + O)) ⇒ (S (n + O)) = (S n)⇒((S n) + O) =(S n)) (((S n) + O) =(S (n + O))));
- [ apply rule (∀_e {S n} (∀z.((S n) + O) =(S (n + O))⇒(S (n + O))= z⇒((S n) + O) =z));
- apply rule (∀_e {(S (n + O))} (∀y.∀z.((S n) + O) =y ⇒ y = z ⇒ ((S n) + O) =z));
- apply rule (∀_e {(S n) + O} (∀x.∀y.∀z.x = y ⇒ y = z ⇒ x = z));
+ | apply rule (∀#i {n} (n + O = n ⇒ ((S n) + O) = (S n)));
+ apply rule (⇒#i [H] (((S n) + O) = (S n)));
+ apply rule (⇒#e ((S (n + O)) = (S n) ⇒ ((S n) + O) = (S n)) ((S (n + O)) = (S n)));
+ [ apply rule (⇒#e (((S n) + O) =(S (n + O)) ⇒ (S (n + O)) = (S n)⇒((S n) + O) =(S n)) (((S n) + O) =(S (n + O))));
+ [ apply rule (∀#e {S n} (∀z.((S n) + O) =(S (n + O))⇒(S (n + O))= z⇒((S n) + O) =z));
+ apply rule (∀#e {(S (n + O))} (∀y.∀z.((S n) + O) =y ⇒ y = z ⇒ ((S n) + O) =z));
+ apply rule (∀#e {(S n) + O} (∀x.∀y.∀z.x = y ⇒ y = z ⇒ x = z));
- | apply rule (∀_e {O} (∀m.(S n) + m = (S (n + m))));
- apply rule (∀_e {n} (∀n.∀m.(S n) + m = (S (n + m))));
+ | apply rule (∀#e {O} (∀m.(S n) + m = (S (n + m))));
+ apply rule (∀#e {n} (∀n.∀m.(S n) + m = (S (n + m))));
- | apply rule (⇒_e (n + O = n ⇒ (S (n + O)) = (S n)) (n + O = n));
- [ apply rule (∀_e {n} (∀w.n + O = w ⇒ (S (n + O)) = (S w)));
- apply rule (∀_e {(n + O)} (∀y.∀w.y = w ⇒ (S y) = (S w)));
+ | apply rule (⇒#e (n + O = n ⇒ (S (n + O)) = (S n)) (n + O = n));
+ [ apply rule (∀#e {n} (∀w.n + O = w ⇒ (S (n + O)) = (S w)));
+ apply rule (∀#e {(n + O)} (∀y.∀w.y = w ⇒ (S y) = (S w)));