PrintForm
Definitions
relation
autom
Sections
AutomataTheory
Doc
At:
quotient
of
nsubn
1
1
1
1.
E:
1
1
Prop
2.
EquivRel x,y:
1. x E y
3.
x,y:
1. Dec(x E y)
1 ~ (i,j:
1//(i E j))
By:
Unfold `one_one_corr` 0
Generated subgoal:
1
f:(
1
(i,j:
1//(i E j))), g:((i,j:
1//(i E j))
1). InvFuns(
1; i,j:
1//(i E j); f; g)
About:
f:(
1
(i,j:1//(i E j))), g:((i,j:1//(i E j))1). InvFuns(1; i,j:1//(i E j); f; g)11Prop1. x E y
x,y:1. Dec(x E y) 1 ~ (i,j:1//(i E j)) f:(1(i,j:1//(i E j))), g:((i,j:1//(i E j))1). InvFuns(1; i,j:1//(i E j); f; g)
