const S = 1 const R = 2 const H = 2 const U = 1 const B = 0 range St = 0..2 const M = 3 range C = 0..M range G = S..R LB = (go[B][U]->go[U][H]->go[H][U]->go[U][B]->LB) +{go[St][St]}. CTL = T[0][0], T[s:C][r:C] = (when (s+r < M) enter[S]->T[s+1][r] |when (s+r < M) enter[R]->T[s][r+1] |when (s>0) leave[S]->T[s-1][r] |when (r>0) leave[R]->T[s][r-1] |when (s==0) go[U][H]->T[s][r] |when (s==0) go[H][U]->T[s][r]). SC = (enter[G]->SC |leave[G]->SC). property ND = (go[St][St]->ND |enter[S]->SD[1]), SD[s:C] = (enter[S]->SD[s+1] |when (s>1) leave[S]->SD[s-1] |when (s==1) leave[S]->ND |go[x:B..U][y:B..U]->SD[s]). progress HB = {go[H][U]} ||FUN = (LB || CTL || SC || ND) >> {leave[S]}.