Nuprl - Pf rel_mng_2

(5steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

r:rel(), rho,ds,da,de,e,s,s',a,tr:Top. rel_mng_2((r)'; rho; ds; da; de; e; s; s'; a; tr) ~ [[r]] rho ds da de e s' a tr

By: UnivCD THEN Unfolds [`rel_addprime`;`rel_mng_2`;`rel_mng`] 0 THEN Analyze 1 THEN Reduce 0 THEN GenConcl ([[name]] rho 2of(e) = z) THEN Thin -1 THEN MoveToConcl -1 THEN ListInd 2 THEN All Reduce THEN Try (Complete Auto)

Generated subgoal:

1 1. name: relname()
2. r1: Term List
3. rho: Top
4. ds: Top
5. da: Top
6. de: Top
7. e: Top
8. s: Top
9. s': Top
10. a: Top
11. tr: Top
12. u: Term
13. v: Term List
14. z:Top. list_accum(x,t.x([[t]] 1of(e) s s' a tr);z;map(t. (t)';v)) ~ list_accum(x,t.x([[t]] 1of(e) s' a tr);z;v)
z:Top. list_accum(x,t.x([[t]] 1of(e) s s' a tr);z([[(u)']] 1of(e) s s' a tr);map(t. (t)';v)) ~ list_accum(x,t.x([[t]] 1of(e) s' a tr);z([[u]] 1of(e) s' a tr);v)

About:

(5steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc