(3steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

At: all-nsub-add1 1 1
1. n:
2. P: (n+1)Prop
3. P(0)
4. x:n. P(x+1)
5. x: (n+1)
6. x = 0
7. P(x-1+1)
x ~ (x-1+1)
By: Analyze -3
Generated subgoals:

None

About:
intnatural_numberaddsubtractfunctionequalsqequalpropall

(3steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc