(45steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
sublist
transitivity
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.
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.
x
L1.x(
eq) L2
12.
x
L2.x(
eq) L3
13.
f:
{T=
}
14.
f
T
T
15.
x,y:T. f(x,y)
x = y
16.
z:
T
17.
z(
f) L1
18.
x
L1.x(
eq) L2
(
z:T. z(
f) L1
z(
eq) L2)
19.
x
L2.x(
eq) L3
(
z:T. z(
f) L2
z(
eq) L3)
z(
eq) L3
By:
RenameVar `zz' 12
THEN
With zz (Analyze -1)
THEN
RenameVar `xx' 11
THEN
Witness18 xx
THEN
Thin 12
THEN
Thin 11
Generated subgoal:
1
11.
f:
{T=
}
12.
f
T
T
13.
x,y:T. f(x,y)
x = y
14.
z:
T
15.
z(
f) L1
16.
z:T. z(
f) L2
z(
eq) L3
17.
z:T. z(
f) L1
z(
eq) L2
z(
eq) L3
About:
(45steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc