Nuprl - Pf sublist transitivity 1 1 1 1 1 1 1 1 1 1 2 1 1 2 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 2 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. x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
8. L1: T List
9. L2: T List
10. L3: T List
11. f: {T=}
12. f TT
13. x,y:T. f(x,y) x = y
14. z: T
15. z(f) L1
16. u: T
17. v: T List
18. eq(z,u) = false
19. z(eq) v
20. z1: T
21. z1(f) v
22. if f(z1,u) true else z1(f) v fi z1(eq) L3

z1(eq) L3

By: MoveToConcl -1 THEN GenConcl (f(z1,u) = b) THEN BoolInd -2 THEN Rewrite (HigherC ifthenelse_evalC THENC TryC (HigherC assert_evalC)) 0 THEN UnivCD

Generated subgoals:

1 22. f(z1,u) = true
23. True z1(eq) L3
z1(eq) L3

2 22. f(z1,u) = false
23. z1(f) v z1(eq) L3
z1(eq) L3

About:

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

1	22. `f(z1,u) = true` 23. `True z1(eq) L3` `z1(eq) L3`
2	22. `f(z1,u) = false` 23. `z1(f) v z1(eq) L3` `z1(eq) L3`