(37steps 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:
list
iso
2
2
1.
'a
: S
2.
x
: (
'a
)
3. is_list_rep(
x
)
x'
:
'a
List.
x
= rep_list(
'a
;
x'
)
By:
Unab [`his_list_rep`] THEN Simp THEN StrongAuto
Generated subgoal:
1
3.
f
:(
'a
),
n
:
.
x
= <
m
:
. if
m
<
n
then
f
(
m
) else @
x
:
'a
. true
fi ,
n
>
x'
:
'a
List.
x
= rep_list(
'a
;
x'
)
16
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(37steps total)
PrintForm
Definitions
Lemmas
hol
list
1
Sections
HOLlib
Doc
'a)
x':'a List. x = rep_list('a;x')
m:
n then f(m) else @
x:'a. true
