Def  a  b  T == a = b  T

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:, 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*  ((x:{a...z-1}, y:{x+1...z}, p',q':Peg. Thm*  (((u:{a...x}. s(u,n) = p) & (u:{y...z}. s(u,n) = q) Thm*  ((& s(x) = (i.p')  {1...n-1}Peg & s(y) = (i.q')  {1...n-1}Peg Thm*  ((& p  p' Thm*  ((& q  q'))	[hanoi_sol2_analemma]
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:, 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:, 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*  (= 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:, 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:{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:, 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), 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  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*  p,r,q,s:Peg. p  q  r  s  permute(p to r ; q to s)(q) = s	[hanoi_peg_perm_comp2]
Thm*  p,r,q,s:Peg. p  q  r  s  permute(p to r ; q to s)(p) = r	[hanoi_peg_perm_comp1]
Thm*  p,r,q,s:Peg. p  q  r  s  Inj(Peg; Peg; permute(p to r ; q to s))	[hanoi_peg_perm_is_inj]
Thm*  p,r,q,s:Peg. p  q  r  s  permute(p to r ; q to s)  PegPeg	[hanoi_peg_perm_wf]
Thm*  x,y:Peg. x  y  y  otherPeg(x; y)	[hanoi_otherpeg_diff4]
Thm*  x,y:Peg. x  y  x  otherPeg(x; y)	[hanoi_otherpeg_diff3]
Thm*  x,y:Peg. x  y  otherPeg(x; y)  y	[hanoi_otherpeg_diff2]
Thm*  x,y:Peg. x  y  otherPeg(x; y)  x	[hanoi_otherpeg_diff1]
Thm*  x,y:Peg. x  y  otherPeg(x; y) = otherPeg(y; x)	[hanoi_otherpeg_sym]
Thm*  x,y,z:Peg. x  y  x  z  y  z  x = otherPeg(y; z)	[hanoi_otherpeg_only]
Thm*  x,y:Peg. x  y  otherPeg(x; y)  Peg	[hanoi_otherpeg_wf]
Thm*  p,q:Peg. Thm*  p  q Thm*   Thm*  (a:, z:{a...}, f:({a...z}Peg). Thm*  (f(a) = p & f(z) = q Thm*  ( Thm*  ((x:{a...z-1}, y:{x+1...z}. Thm*  (((u:{a...x}. f(u) = p) Thm*  ((& f(x+1)  p Thm*  ((& f(y-1)  q Thm*  ((& (u:{y...z}. f(u) = q)))	[hanoi_pegseq_analemma]
Def  Moving disk k of n takes f to g Def  == (i:{1...n}. f(i) = g(i)  Peg  i  k) Def  == & (i:{1...k-1}. f(i)  f(k)  Peg & g(i)  g(k)  Peg)	[hanoi_step_at]

In prior sections: int 1 bool 1 int 2

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