(43steps total)
PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
cons
sublist
cons
T
:Type,
x1
,
x2
:
T
,
L1
,
L2
:
T
List.
[
x1
/
L1
]
[
x2
/
L2
]
x1
=
x2
&
L1
L2
[
x1
/
L1
]
L2
By:
Auto THEN All (Unfold `sublist`) THEN All Reduce THEN ExRepD
Generated subgoals:
1
1.
T
: Type
2.
x1
:
T
3.
x2
:
T
4.
L1
:
T
List
5.
L2
:
T
List
6.
f
:
(||
L1
||+1)
(||
L2
||+1)
7. increasing(
f
;||
L1
||+1)
8.
j
:
(||
L1
||+1). [
x1
/
L1
][
j
] = [
x2
/
L2
][(
f
(
j
))]
x1
=
x2
& (
f
:(
||
L1
||
||
L2
||).
& (
increasing(
f
;||
L1
||) & (
j
:
||
L1
||.
L1
[
j
] =
L2
[(
f
(
j
))]))
(
f
:(
(||
L1
||+1)
||
L2
||).
(
increasing(
f
;||
L1
||+1) & (
j
:
(||
L1
||+1). [
x1
/
L1
][
j
] =
L2
[(
f
(
j
))]))
21
steps
2
1.
T
: Type
2.
x1
:
T
3.
x2
:
T
4.
L1
:
T
List
5.
L2
:
T
List
6.
x1
=
x2
6.
& (
f
:(
||
L1
||
||
L2
||).
6. & (
increasing(
f
;||
L1
||) & (
j
:
||
L1
||.
L1
[
j
] =
L2
[(
f
(
j
))]))
6.
(
f
:(
(||
L1
||+1)
||
L2
||).
6.
(
increasing(
f
;||
L1
||+1) & (
j
:
(||
L1
||+1). [
x1
/
L1
][
j
] =
L2
[(
f
(
j
))]))
f
:(
(||
L1
||+1)
(||
L2
||+1)).
increasing(
f
;||
L1
||+1) & (
j
:
(||
L1
||+1). [
x1
/
L1
][
j
] = [
x2
/
L2
][(
f
(
j
))])
21
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(43steps total)
PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc