public class TritCore{
  /**
   * Precondition: digit is an array of integers of length > 0 &&
   *                 from, to, intermediate are distinct elements of {0,1,2}
   * Postcondition: if (for some 0 <= k < digit.length
   *                      digit[0, ...,k-1] == intermediate && digit[k] == from) {
   *                      return true && set digit[k] = to}
   *                else {
   *                  return false;
   *                } &&
   *                no other element of digit is changed
   */
  public static boolean tweak(int[] digit, int from, int to){
    for (int i = 0; i < digit.length; i++) {
      if (digit[i] == from) {
        digit[i] = to;
        return true;
      }
      if (digit[i] == to) { return false; }
    }
    return false;
  }
  
  /**
   * Precondition: digit is an array of integers of length >= n > 0 with values in {0,1,2} &&
   *                   to, from, intermediate are distinct elements of {0,1,2} &&
   *                   if (n>1) {digit[0, ..., n-1] == from}
   *                     else if (n==1) {for some 0 <= k < digit.length
   *                                       digit[0, .., k-1] == intermediate && digit[k] == from} 
   * Postcondition:    if (n>1) {digit[0, ..., n-1] == to}
   *                     else if (n==1) {digit[k] == to}
   *                   all other elements of digit are unchanged && return true
   * */

  public static boolean groupTweak(int[] digit, int n, 
                                   int from, int to, int intermediate) {
    boolean status= true;
    if (n == 1) {
      status= tweak(digit, from, to);
    }
    else {
      status = status && groupTweak(digit, n-1, from, intermediate, to);
      status = status && groupTweak(digit, 1, from, to, intermediate);
      status = status && groupTweak(digit, n-1, intermediate, to, from);
    }
    return status;
  }
  
}