PrintForm
Definitions
relation
autom
Sections
AutomataTheory
Doc
At:
quotient
of
nsubn
1
1
1
1
2
1.
E:
1
1
Prop
2.
EquivRel x,y:
1. x E y
3.
x,y:
1. Dec(x E y)
4.
0
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)
By:
InstConcl [
x.0;
x.0]
Generated subgoal:
1
InvFuns(
1; i,j:
1//(i E j);
x.0;
x.0)
About:
InvFuns(
1; i,j:1//(i E j); 
x.0; x.0)1
1Prop1. x E y
x,y:1. Dec(x E y)
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)x.0;x.0] InvFuns(1; i,j:1//(i E j); x.0; x.0)
