Nuprl - Pf incl_aux3_quo 1 2 1 2 2 1 2

PrintForm Definitions relation autom Sections AutomataTheory Doc

1. n: {1...}
2. m: n
3. E: nnProp
4. EquivRel i,j:n. i E j
5. EquivRel i,j:m. i E j
6. x: i,j:m//(i E j)
7. y: i,j:m//(i E j)
8. x i,j:n//(i E j)
9. y i,j:n//(i E j)
10. y1: m
11. y2: m
12. y1 E y2
13. x1: m
14. x2: m
15. x1 E x2

* = * (x1 = y1 i,j:n//(i E j) x1 = y1 i,j:m//(i E j))

By: Analyze THEN GenRepD

Generated subgoals:

1 16. x1 = y1 i,j:n//(i E j)
x1 = y1 i,j:m//(i E j)

2 x1 i,j:n//(i E j)

3 y1 i,j:n//(i E j)

4 16. x1 = y1 i,j:m//(i E j)
x1 = y1 i,j:n//(i E j)

About:

1	16. `x1 = y1 i,j:n//(i E j)` `x1 = y1 i,j:m//(i E j)`
2	`x1 i,j:n//(i E j)`
3	`y1 i,j:n//(i E j)`
4	16. `x1 = y1 i,j:m//(i E j)` `x1 = y1 i,j:n//(i E j)`