Nuprl - Pf rel_mng_unprime 1 1 1 1

(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. 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))
14. 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))

By: Subst ([[u]] 1of(e) s a tr ~ [[unprime(u)]] 1of(e) s a tr) 0 THEN Try BackThruSomeHyp THEN Try (BackThru Thm* t:Term, e,a,s,tr:Top. [[t]] e s a tr ~ [[unprime(t)]] e s a tr)

Generated subgoals:

None

About:

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