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
1
1.
T: Type
2.
Discrete{T}
3.
eq: {T
}
4.
eq 
T
T
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)
29.
eq(z,u1) = true
if true
true else u(eq) v1 fi if true true else z(eq) v1 fi
By:
Rewrite (HigherC ifthenelse_evalC THENC HigherC assert_evalC) 0
Generated subgoals:
None
About:
