Def   == {i:| 0i }

is mentioned by

Thm*  n:, p,q:Peg. Thm*  p  q Thm*   Thm*  (a:, z:{a...}, s:({a...z}{1...n}Peg). Thm*  (s is a Hanoi(n disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q) Thm*  ( Thm*  ((2^n)z-a+1)	[hanoi_sol2_lb]
Thm*  n:, p,q:Peg. Thm*  p  q Thm*   Thm*  (a:.  Thm*  (1of(HanoiSTD(n disks; from: p; to: q; indexing from: a)) = a+(2^n)-1)	[hanoi_general_exists_lemma2PROG_endpoint]
Thm*  n:, k:. (n^k)	[exponentiation_wf_nat_plus]
Thm*  n,k:. (n^k)	[exponentiation_wf_nat]
Thm*  n:, k:. (n^k)	[exponentiation_wf]
Thm*  n:, p,q:Peg. Thm*  p  q Thm*   Thm*  (a:.  Thm*  (z:{a...}, s:({a...z}{1...n}Peg). Thm*  (s is a Hanoi(n disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q))	[hanoi_sol2_via_general]
Thm*  n:, f,g:({1...n}Peg), a:. Thm*  z:{a...}, s:({a...z}{1...n}Peg). Thm*  s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g	[hanoi_general_exists]
Thm*  n:, p,q:Peg. Thm*  p  q Thm*   Thm*  (a:.  Thm*  (HanoiSTD(n disks; from: p; to: q; indexing from: a)/z,s. Thm*  (s is a Hanoi(n disk) seq on a..z Thm*  (& s(a) = (i.p)  {1...n}Peg Thm*  (& s(z) = (i.q)  {1...n}Peg)	[hanoi_sol2_ala_generalPROGworks]
Thm*  n:, p,q:Peg. Thm*  p  q Thm*   Thm*  (a:.  Thm*  (HanoiSTD(n disks; from: p; to: q; indexing from: a) Thm*  ( z:{a...}({a...z}{1...n}Peg))	[hanoi_sol2_ala_generalPROG_wf]
Thm*  n:, p,q:Peg. Thm*  p  q Thm*   Thm*  (a:.  Thm*  (z:{a...}, s:({a...z}{1...n}Peg). Thm*  (s is a Hanoi(n disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q))	[hanoi_sol2_ala_general]
Thm*  n:, p,q:Peg. Thm*  p  q Thm*   Thm*  (z:{1...}, s:({1...z}{1...n}Peg). Thm*  (s is a Hanoi(n disk) seq on 1..z & s(1) = (i.p) & s(z) = (i.q))	[hanoi_sol2_via_permshift]
Thm*  n:, a,z:, m:{a...z-1}, s1:({a...m}{1...n}Peg), Thm*  s2:({m+1...z}{1...n}Peg). Thm*  (k:{1...n}. Moving disk k of n takes s1(m) to s2(m+1)) Thm*   Thm*  s1 is a Hanoi(n disk) seq on a..m Thm*   Thm*  s2 is a Hanoi(n disk) seq on m+1..z Thm*   Thm*  (s1 @(m) s2) is a Hanoi(n disk) seq on a..z	[hanoi_seq_join_seq]
Thm*  n:, m,a,z:, s1:({a...m}{1...n}Peg), s2:({m+1...z}{1...n}Peg), Thm*  x:{m+1...z}. (s1 @(m) s2)(x) = s2(x)	[hanoi_seq_join_part2]
Thm*  n:, m,a,z:, s1:({a...m}{1...n}Peg), s2:({m+1...z}{1...n}Peg), Thm*  x:{a...m}. (s1 @(m) s2)(x) = s1(x)	[hanoi_seq_join_part1]
Thm*  n:, m,a,z:, s1:({a...m}{1...n}Peg), s2:({m+1...z}{1...n}Peg). Thm*  (s1 @(m) s2)  {a...z}{1...n}Peg	[hanoi_seq_join_wf]
Thm*  n':, n:{n'...}, a:, z:{a...}, s:({a...z}{1...n}Peg). Thm*  s is a Hanoi(n disk) seq on a..z Thm*   Thm*  (x:{a...z}, i:{n'+1...n}. s(a,i) = s(x,i)) Thm*   Thm*  s is a Hanoi(n' disk) seq on a..z	[hanoi_seq_shallower]
Thm*  n:, a,z:, s:({a...z}{1...n}Peg). Thm*  s is a Hanoi(n disk) seq on a..z Thm*   Thm*  (a',z':{a...z}. s is a Hanoi(n disk) seq on a'..z')	[hanoi_subseq]
Thm*  n:, a,z,d:, s:({a...z}{1...n}Peg). Thm*  s is a Hanoi(n disk) seq on a..z Thm*   Thm*  (x.s(x-d)) is a Hanoi(n disk) seq on a+d..z+d	[hanoi_seq_shift]
Thm*  a,z:, n:, s:({a...z}{1...n}Peg), n':. Thm*  nn' Thm*   Thm*  (h:({n+1...n'}Peg).  Thm*  (s is a Hanoi(n disk) seq on a..z Thm*  ( Thm*  ((s(?) {to n}  h {to n'}) is a Hanoi(n' disk) seq on a..z)	[hanoi_seq_deepen_seq]
Thm*  a,z:, n:, s:({a...z}{1...n}Peg), n':. Thm*  nn' Thm*   Thm*  (h:({n+1...n'}Peg), i:{1...n'}. Thm*  (in  (x:{a...z}. (s(?) {to n}  h {to n'})(x,i) = s(x,i)))	[hanoi_seq_deepen_loweq]
Thm*  a,z:, n:, s:({a...z}{1...n}Peg), n':. Thm*  nn' Thm*   Thm*  (h:({n+1...n'}Peg), i:{1...n'}. Thm*  (n<i  (x:{a...z}. (s(?) {to n}  h {to n'})(x,i) = h(i)))	[hanoi_seq_deepen_higheq]
Thm*  a,z:, n:, s:({a...z}{1...n}Peg), n':. Thm*  nn' Thm*   Thm*  (h:({n+1...n'}Peg). (s(?) {to n}  h {to n'})  {a...z}{1...n'}Peg)	[hanoi_seq_deepen_wf]
Thm*  n:, a,z:, s:({a...z}{1...n}Peg). Thm*  s is a Hanoi(n disk) seq on a..z Thm*   Thm*  (f:(PegPeg).  Thm*  (Inj(Peg; Peg; f)  (x,i. f(s(x,i))) is a Hanoi(n disk) seq on a..z)	[hanoi_seq_permutepegs]
Thm*  n':, n:{n'...}, a,z:, s:({a...z}{1...n}Peg). Thm*  s is a Hanoi(n disk) seq on a..z Thm*   Thm*  (a',z':{a...z}. Thm*  ((x:{a'...z'}, i:{n'+1...n}. s(a',i) = s(x,i)) Thm*  ( Thm*  (s is a Hanoi(n' disk) seq on a'..z')	[hanoi_seq_core]
Thm*  n:, a,z:, s:({a...z}{1...n}Peg). Thm*  s is a Hanoi(n disk) seq on a..z  Prop	[hanoi_seq_wf]
Thm*  n:, f,g:({1...n}Peg), k:{1...n}. Thm*  Moving disk k of n takes f to g  f(k)  g(k)	[hanoi_step_at_diff]
Thm*  n:, f,g:({1...n}Peg), k:{1...n}. Thm*  Moving disk k of n takes f to g  Moving disk k of n takes g to f	[hanoi_step_at_sym]
Thm*  n:, f,g:({1...n}Peg), j:{1...n}. Thm*  (k:{1...n}. Moving disk k of n takes f to g) Thm*   Thm*  f(j)  g(j)  Moving disk j of n takes f to g	[hanoi_step_at_change]
Thm*  n:, f,g:({1...n}Peg), i,k:{1...n}. Thm*  Moving disk k of n takes f to g  f(i)  g(i)  i = k	[hanoi_step_at_unique]
Thm*  n:, f,g:({1...n}Peg), k:{1...n}. Thm*  Moving disk k of n takes f to g Thm*   Thm*  f = (i.otherPeg(f(k); g(k)))  {1...k-1}Peg	[hanoi_step_at_otherpeg]
Thm*  n:, f,g:({1...n}Peg), k:{1...n}. Thm*  Moving disk k of n takes f to g  f(k)  g(k)	[hanoi_step_at_change2]
Thm*  n:, f,g:({1...n}Peg), k,i:{1...n}. Thm*  Moving disk k of n takes f to g  i  k  f(i) = g(i)	[hanoi_step_at_same]
Thm*  n:, f,g:({1...n}Peg), k:{1...n}. Thm*  Moving disk k of n takes f to g  Prop	[hanoi_step_at_wf]
Thm*  n:, f:({1...n}Peg), n':. Thm*  nn' Thm*   Thm*  (f':({n+1...n'}Peg), i:{1...n'}. Thm*  (n<i  (f {to n}  f' {to n'})(i) = f'(i))	[hanoi_extend_higheq]
Thm*  n:, f:({1...n}Peg), n':. Thm*  nn' Thm*   Thm*  (f':({n+1...n'}Peg), i:{1...n'}. Thm*  (in  (f {to n}  f' {to n'})(i) = f(i))	[hanoi_extend_loweq]
Thm*  n:, f:({1...n}Peg), n':. Thm*  nn'  (f':({n+1...n'}Peg). (f {to n}  f' {to n'})  {1...n'}Peg)	[hanoi_extend_wf]

In prior sections: int 1 bool 1 int 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html