PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
fin
dec
fin
1
1.
T:
Type
2.
B:
T
Prop
3.
f:
0
T
4.
g:
T
0
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)
By:
InstConcl [0;f;g]
Generated subgoal:
1
InvFuns(
0; {t:T| B(t) }; f; g)
About:
InvFuns(
0; {t:T| B(t) }; f; g)
Prop0T00; 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) InvFuns(0; {t:T| B(t) }; f; g)
