Def  (s1 @(m) s2)(x) == if xm s1(x) else s2(x) fi

is mentioned by

Thm*  n:, p,q:Peg. Thm*  p  q Thm*   Thm*  (a:.  Thm*  (HanoiSTD(n disks; from: p; to: q; indexing from: a) Thm*  (= Thm*  ((HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a)/m,s1. Thm*  ((HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1) Thm*  ((/z,s2. <z,HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2. r1 @(m) r2>))	[hanoi_sol2_ala_generalPROGcomp]
Thm*  n:, a:, z:{a...}, m:{a...z-1}, f,g:({1...n}Peg). Thm*  f(n)  g(n) Thm*   Thm*  (s1:({a...m}{1...n-1}Peg), s2:({m+1...z}{1...n-1}Peg). Thm*  (s1 is a Hanoi(n-1 disk) seq on a..m Thm*  (& s1(a) = f  {1...n-1}Peg Thm*  (& s2 is a Hanoi(n-1 disk) seq on m+1..z Thm*  (& s2(z) = g  {1...n-1}Peg Thm*  (& s1(m) = s2(m+1) Thm*  (& (i:{1...n-1}. s1(m,i)  f(n) & s2(m+1,i)  g(n)) Thm*  ( Thm*  ((HanoiHelper(n; s1; f; s2; g)/r1,r2. Thm*  (((r1 @(m) r2) is a Hanoi(n disk) seq on a..z & r1(a) = f & r2(z) = g))	[hanoi_general_exists_lemma2PROGworks]
Thm*  n:, a:, z:{a...}, m:{a...z-1}, f,g:({1...n}Peg). Thm*  f(n)  g(n) Thm*   Thm*  (s1:({a...m}{1...n-1}Peg), s2:({m+1...z}{1...n-1}Peg). Thm*  (s1 is a Hanoi(n-1 disk) seq on a..m Thm*  (& s1(a) = f  {1...n-1}Peg Thm*  (& s2 is a Hanoi(n-1 disk) seq on m+1..z Thm*  (& s2(z) = g  {1...n-1}Peg Thm*  (& s1(m) = s2(m+1) Thm*  (& (i:{1...n-1}. s1(m,i)  f(n) & s2(m+1,i)  g(n))) Thm*   Thm*  (r1:({a...m}{1...n}Peg), r2:({m+1...z}{1...n}Peg). Thm*  ((r1 @(m) r2) is a Hanoi(n disk) seq on a..z & r1(a) = f & r2(z) = g)	[hanoi_general_exists_lemma2]
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]
Def  HanoiSTD(n disks; from: p; to: q; indexing from: a) Def  == if n=0 <a,x,i. whatever> Def  == else HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a) Def  == else /m,s1. Def  == else HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m Def  == else HanoiSTD(+1) Def  == else /z,s2. <z,HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2. r1 @(m) r2> fi Def  (recursive)	[hanoi_sol2_ala_generalPROG]

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