Nuprl - Pf fin_dec

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)

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

By: InstHyp [{t:T| g(t) < n-1 };B] 3

Generated subgoals:

1 {t:T| g(t) < n-1 } Type

2 B {t:T| g(t) < n-1 }Prop

3 (f:((n-1){t:T| g(t) < n-1 }), g@0:({t:T| g(t) < n-1 }(n-1)). InvFuns((n-1); {t:T| g(t) < n-1 }; f; g@0)) & (t:{t:T| g(t) < n-1 }. Dec(B(t)))

4 13. m:, f:(m{t:{t:T| g(t) < n-1 }| B(t) }), g@0:({t:{t:T| g(t) < n-1 }| B(t) }m). InvFuns(m; {t:{t:T| g(t) < n-1 }| B(t) }; f; g@0)
m:, f:(m{t:T| B(t) }), g:({t:T| B(t) }m). InvFuns(m; {t:T| B(t) }; f; g)

About:

1	`{t:T\| g(t) < n-1 } Type`
2	`B {t:T\| g(t) < n-1 }Prop`
3	`(f:((n-1){t:T\| g(t) < n-1 }), g@0:({t:T\| g(t) < n-1 }(n-1)). InvFuns((n-1); {t:T\| g(t) < n-1 }; f; g@0)) & (t:{t:T\| g(t) < n-1 }. Dec(B(t)))`
4	13. `m:, f:(m{t:{t:T\| g(t) < n-1 }\| B(t) }), g@0:({t:{t:T\| g(t) < n-1 }\| B(t) }m). InvFuns(m; {t:{t:T\| g(t) < n-1 }\| B(t) }; f; g@0)` `m:, f:(m{t:T\| B(t) }), g:({t:T\| B(t) }m). InvFuns(m; {t:T\| B(t) }; f; g)`