Nuprl - Proof: injection le 1 1 2 1

(37steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: injection le 1 1 2 1

1. k :

2. 0<k
3.

. (

f:(

(k-1)

m). Inj(

(k-1);

m; f))

k-1

m
4. m :

5. f :

m
6. Inj(

m; f)
7. f(0)

m
8. g :

(k-1)

(m-1)
9.

(k-1). g(i) = if f(i)=

m-1

f(k-1) else f(i) fi

Inj(

(k-1);

(m-1); g)

By:	ParallelOp -4 THEN ParallelOp -1 THEN ParallelOp -3 THEN HypSubstSq -3 0 THEN HypSubstSq -1 0 THEN SplitOnConclITE THEN SplitOnConclITE

Generated subgoals:

1 6. a1,a2:k. f(a1) = f(a2)  a1 = a2
7. f(0)  m
8. g : (k-1)(m-1)
9. i:(k-1). g(i) = if f(i)=m-1 f(k-1) else f(i) fi
10. a1 : (k-1)
11. g(a1) = if f(a1)=m-1 f(k-1) else f(a1) fi
12. a2 : (k-1)
13. g(a2) = if f(a2)=m-1 f(k-1) else f(a2) fi
14. f(a1) = m-1
15. f(a2) = m-1
  f(k-1) = f(k-1)  (m-1)  a1 = a2
11 steps

2 6. a1,a2:k. f(a1) = f(a2)  a1 = a2
7. f(0)  m
8. g : (k-1)(m-1)
9. i:(k-1). g(i) = if f(i)=m-1 f(k-1) else f(i) fi
10. a1 : (k-1)
11. g(a1) = if f(a1)=m-1 f(k-1) else f(a1) fi
12. a2 : (k-1)
13. g(a2) = if f(a2)=m-1 f(k-1) else f(a2) fi
14. f(a1) = m-1
15. f(a2) = m-1
  f(k-1) = f(a2)  (m-1)  a1 = a2
6 steps

3 6. a1,a2:k. f(a1) = f(a2)  a1 = a2
7. f(0)  m
8. g : (k-1)(m-1)
9. i:(k-1). g(i) = if f(i)=m-1 f(k-1) else f(i) fi
10. a1 : (k-1)
11. g(a1) = if f(a1)=m-1 f(k-1) else f(a1) fi
12. a2 : (k-1)
13. g(a2) = if f(a2)=m-1 f(k-1) else f(a2) fi
14. f(a1) = m-1
15. f(a2) = m-1
  f(a1) = f(k-1)  (m-1)  a1 = a2
6 steps

4 6. a1,a2:k. f(a1) = f(a2)  a1 = a2
7. f(0)  m
8. g : (k-1)(m-1)
9. i:(k-1). g(i) = if f(i)=m-1 f(k-1) else f(i) fi
10. a1 : (k-1)
11. g(a1) = if f(a1)=m-1 f(k-1) else f(a1) fi
12. a2 : (k-1)
13. g(a2) = if f(a2)=m-1 f(k-1) else f(a2) fi
14. f(a1) = m-1
15. f(a2) = m-1
  f(a1) = f(a2)  (m-1)  a1 = a2
2 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(37steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc

1	6. a1,a2:k. f(a1) = f(a2) a1 = a2 7. f(0) m 8. g : (k-1)(m-1) 9. i:(k-1). g(i) = if f(i)=m-1 f(k-1) else f(i) fi 10. a1 : (k-1) 11. g(a1) = if f(a1)=m-1 f(k-1) else f(a1) fi 12. a2 : (k-1) 13. g(a2) = if f(a2)=m-1 f(k-1) else f(a2) fi 14. f(a1) = m-1 15. f(a2) = m-1 f(k-1) = f(k-1) (m-1) a1 = a2	11 steps
2	6. a1,a2:k. f(a1) = f(a2) a1 = a2 7. f(0) m 8. g : (k-1)(m-1) 9. i:(k-1). g(i) = if f(i)=m-1 f(k-1) else f(i) fi 10. a1 : (k-1) 11. g(a1) = if f(a1)=m-1 f(k-1) else f(a1) fi 12. a2 : (k-1) 13. g(a2) = if f(a2)=m-1 f(k-1) else f(a2) fi 14. f(a1) = m-1 15. f(a2) = m-1 f(k-1) = f(a2) (m-1) a1 = a2	6 steps
3	6. a1,a2:k. f(a1) = f(a2) a1 = a2 7. f(0) m 8. g : (k-1)(m-1) 9. i:(k-1). g(i) = if f(i)=m-1 f(k-1) else f(i) fi 10. a1 : (k-1) 11. g(a1) = if f(a1)=m-1 f(k-1) else f(a1) fi 12. a2 : (k-1) 13. g(a2) = if f(a2)=m-1 f(k-1) else f(a2) fi 14. f(a1) = m-1 15. f(a2) = m-1 f(a1) = f(k-1) (m-1) a1 = a2	6 steps
4	6. a1,a2:k. f(a1) = f(a2) a1 = a2 7. f(0) m 8. g : (k-1)(m-1) 9. i:(k-1). g(i) = if f(i)=m-1 f(k-1) else f(i) fi 10. a1 : (k-1) 11. g(a1) = if f(a1)=m-1 f(k-1) else f(a1) fi 12. a2 : (k-1) 13. g(a2) = if f(a2)=m-1 f(k-1) else f(a2) fi 14. f(a1) = m-1 15. f(a2) = m-1 f(a1) = f(a2) (m-1) a1 = a2	2 steps