(8steps total)
PrintForm
Definitions
Lemmas
hol
list
1
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hnil
def
1
1.
'a
: S
nil = abs_list(<
n
:hnum. @
e
:
'a
. true
,0>)
By:
Inst
Thm*
'a
,
'b
:S,
P
:(
'b
),
rep
:(
'a
'b
),
abs
:(
'b
'a
),
a
:
'a
,
r
:
'b
.
Thm*
iso_pair(
'a
;
'b
;
P
;
rep
;
abs
)
rep
(
a
) =
r
a
=
abs
(
r
)
[
'a
List;(
'a
)
;is_list_rep;rep_list;abs_list;nil;<
n
:
. @
e
:
'a
. true
,0>]
THEN
StrongAuto
THEN
Try (Complete (Unfold `label` 0))
Generated subgoals:
1
iso_pair(
'a
List;(
'a
)
;is_list_rep;rep_list;abs_list)
1
step
2
rep_list(nil) = <
n
:
. @
e
:
'a
. true
,0>
(
'a
)
5
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(8steps total)
PrintForm
Definitions
Lemmas
hol
list
1
Sections
HOLlib
Doc