Nuprl - Pf quotient_of

PrintForm Definitions relation autom Sections AutomataTheory Doc

1. n: {1+1...}
2. E:((n-1)(n-1)Prop). (EquivRel x,y:(n-1). x E y) & (x,y:(n-1). Dec(x E y)) (m:(n-1+1). m ~ (i,j:(n-1)//(i E j)))
3. E: nnProp
4. (EquivRel x,y:n. x E y) & (x,y:n. Dec(x E y))

m:(n+1). m ~ (i,j:n//(i E j))

By: Assert (EquivRel x,y:(n-1). x E y)

Generated subgoals:

1 4. EquivRel x,y:n. x E y
5. x,y:n. Dec(x E y)
EquivRel x,y:(n-1). x E y

2 5. EquivRel x,y:(n-1). x E y
m:(n+1). m ~ (i,j:n//(i E j))

About:

1	4. `EquivRel x,y:n. x E y` 5. `x,y:n. Dec(x E y)` `EquivRel x,y:(n-1). x E y`
2	5. `EquivRel x,y:(n-1). x E y` `m:(n+1). m ~ (i,j:n//(i E j))`