Nuprl - Pf rel_mng

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

1. name: relname()
2. r1: Term List
3. e: Top
4. a: Top
5. s: Top
6. ds: Top
7. da: Top
8. de: Top
9. rho: Top
10. tr: Top
11. F: Top
12. [[name]] rho 2of(e) = F

list_accum(x,t.x([[t]] 1of(e) s a tr);F;r1) ~ list_accum(x,t.x([[t]] 1of(e) s a tr);F;map(t. unprime(t);r1))

By: Thin -1 THEN MoveToConcl -1 THEN ListInd 2 THEN Reduce 0 THEN Try (Complete Auto)

Generated subgoal:

1 11. u: Term
12. v: Term List
13. F:Top. list_accum(x,t.x([[t]] 1of(e) s a tr);F;v) ~ list_accum(x,t.x([[t]] 1of(e) s a tr);F;map(t. unprime(t);v))
F:Top. list_accum(x,t.x ([[t]] 1of(e) s a tr);F ([[u]] 1of(e) s a tr);v) ~ list_accum(x,t....;F (...);map(t. unprime(t);v))

About:

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