Nuprl - Pf sublist transitivity 1 1 1 1 1 1 1 1 1 1 2 1 1 1 1 1 2 1 1 1 2 1 1 1 1 1 1

(45steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc

At: sublist transitivity 1 1 1 1 1 1 1 1 1 1 2 1 1 1 1 1 2 1 1 1 2 1 1 1 1 1 1

1. T: Type
2. Discrete{T}
3. eq: {T}
4. eq TT
5. x:T. eq(x,x)
6. x,y:T. eq(x,y) eq(y,x)
7. L1: T List
8. L2: T List
9. L3: T List
10. f: {T=}
11. f TT
12. x,y:T. f(x,y) x = y
13. z: T
14. z(f) L1
15. u: T
16. v: T List
17. eq(z,u) = true
18. True
19. f(u,u)
20. f(u,u) = true
21. u1: T
22. v1: T List
23. u(eq) v1 z(eq) v1
24. eq(z,u)
25. eq(u,u1) = true
26. eq(u,u1)
27. eq(z,u) eq(u,u1) eq(z,u1)
28. eq(z,u1)

if true true else u(eq) v1 fi if eq(z,u1) true else z(eq) v1 fi

By: FwdThru Thm* P:. P P = true [28]

Generated subgoal:

1 29. eq(z,u1) = true
if true true else u(eq) v1 fi if eq(z,u1) true else z(eq) v1 fi

About:

(45steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc