Nuprl - Pf fin_dec

PrintForm Definitions finite sets Sections AutomataTheory Doc

n:, T:Type, B:(TProp). (n ~ T) & (t:T. Dec(B(t))) (m:. m ~ {t:T| B(t) })

By: Unfold `one_one_corr` 0 THEN Analyze 0 THEN NatInd 1 THEN GenRepD THEN ExRepD

Generated subgoals:

1 1. T: Type
2. B: TProp
3. f: 0T
4. g: T0
5. InvFuns(0; T; f; g)
6. 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)

2 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. InvFuns(n; T; f; g)
9. 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)

About:

1	1. `T:` `Type` 2. `B:` `TProp` 3. `f:` `0T` 4. `g:` `T0` 5. `InvFuns(0; T; f; g)` 6. `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)`
2	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. `InvFuns(n; T; f; g)` 9. `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)`