Nuprl - Pf fin_dec_fin 2 1 2 2 4 1 1

PrintForm Definitions finite sets Sections AutomataTheory Doc

1. n:
2. 0 < n
3. T:Type, B:(TProp). (f:((n-1)T), g:(T(n-1)). InvFuns((n-1); T; f; g)) & (t:T. Dec(B(t))) (m:, f:(m{t:T| B(t) }), g:({t:T| B(t) }m). InvFuns(m; {t:T| B(t) }; f; g))
4. T: Type
5. B: TProp
6. f: nT
7. g: Tn
8. g o f = Id
9. f o g = Id
10. t:T. Dec(B(t))
11. f (n-1){t:T| g(t) < n-1 }
12. g {t:T| g(t) < n-1 }(n-1)
13. m:
14. f1: m{t:{t:T| g(t) < n-1 }| B(t) }
15. g@0: {t:{t:T| g(t) < n-1 }| B(t) }m
16. InvFuns(m; {t:{t:T| g(t) < n-1 }| B(t) }; f1; g@0)
17. B(f(n-1))

m:, f:(m{t:T| B(t) }), g:({t:T| B(t) }m). InvFuns(m; {t:T| B(t) }; f; g)

By: Let (f2 = (x.if x=m f(n-1) else f1(x) fi)) THEN Let (g2 = (x.if g(x)=n-1 m else g@0(x) fi))

Generated subgoals:

1 (x.if x=m f(n-1) else f1(x) fi) (m+1){t:T| B(t) }

2 (m+1){t:T| B(t) } Type{[1 | i 0]}

3 18. f2: (m+1){t:T| B(t) }
19. f2 = (x.if x=m f(n-1) else f1(x) fi)
(x.if g(x)=n-1 m else g@0(x) fi) {t:T| B(t) }(m+1)

4 18. f2: (m+1){t:T| B(t) }
19. f2 = (x.if x=m f(n-1) else f1(x) fi)
{t:T| B(t) }(m+1) Type{[1 | i 0]}

5 18. f2: (m+1){t:T| B(t) }
19. f2 = (x.if x=m f(n-1) else f1(x) fi)
20. g2: {t:T| B(t) }(m+1)
21. g2 = (x.if g(x)=n-1 m else g@0(x) fi)
m:, f:(m{t:T| B(t) }), g:({t:T| B(t) }m). InvFuns(m; {t:T| B(t) }; f; g)

About:

1	`(x.if x=m f(n-1) else f1(x) fi) (m+1){t:T\| B(t) }`
2	`(m+1){t:T\| B(t) } Type{[1 \| i 0]}`
3	18. `f2:` `(m+1){t:T\| B(t) }` 19. `f2 = (x.if x=m f(n-1) else f1(x) fi)` `(x.if g(x)=n-1 m else g@0(x) fi) {t:T\| B(t) }(m+1)`
4	18. `f2:` `(m+1){t:T\| B(t) }` 19. `f2 = (x.if x=m f(n-1) else f1(x) fi)` `{t:T\| B(t) }(m+1) Type{[1 \| i 0]}`
5	18. `f2:` `(m+1){t:T\| B(t) }` 19. `f2 = (x.if x=m f(n-1) else f1(x) fi)` 20. `g2:` `{t:T\| B(t) }(m+1)` 21. `g2 = (x.if g(x)=n-1 m else g@0(x) fi)` `m:, f:(m{t:T\| B(t) }), g:({t:T\| B(t) }m). InvFuns(m; {t:T\| B(t) }; f; g)`