1. a : {2...}
2. b : 
3. k:, g,h:({a..b}).
3. is_prime_factorization(a; b; g)
3. 
3. is_prime_factorization(a; b; h)
3. 
3. {a..b}(g) = k  {a..b}(g) = {a..b}(h)  g = h
  g,h:({a..b}).
  is_prime_factorization(a; b; g)
  
  is_prime_factorization(a; b; h)  {a..b}(g) = {a..b}(h)  g = h

By:

Auto

1

4. g : {a..b} 5. h : {a..b} 6. is_prime_factorization(a; b; g) 7. is_prime_factorization(a; b; h) 8. {a..b}(g) = {a..b}(h)   g = h

2 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html