PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
fin
dec
fin
2
1
2
2
3
1.
n:
2.
0 < n
3.
T:Type, B:(T
Prop). (
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:
T
Prop
6.
f:
n
T
7.
g:
T
n
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)
(
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)))
By:
Analyze 0
Generated subgoals:
1
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)
2
t:{t:T| g(t) < n-1 }. Dec(B(t))
About: