/*
   Example in Fig. 6 on p.15 from 
     Benny Godlin, Ofer Strichman:
     Regression verification: proving the equivalence of similar programs.
     Softw. Test., Verif. Reliab. 23(3): 241-258 (2013)

   The following is a variant of the original obtained by 
   decomposing the nesting of function calls by hand.

*/

int M1(int n);

int val1(int x){
  return x;
}

int F1(int n){
  if( n == 0 ) return 1;
  { int tmp = F1(n-1);
    return n - M1(tmp);
  }
}

int M1(int n){
  if( n == 0 ) return 0;
  { int tmp = M1(n-1);
    return n - F1(tmp);
  }
}

int main1(){
  int i=0, out=0;
  for( i=0 ; i < 20 ; i++ ){
    out = F1(i);
    if( i > 20 ) return 3;
  }
  for( i=0 ; i < 20 ; i++ ){
    int tmp = M1(i);
    out = val1(tmp);
  }
  return out;
}

int M2(int n);
int G2(int n);

int val2(int x){
  return x + 1;
}

int F2(int n){
  if( n == 0 ) return 1;
  { int tmp = F2(n-1);
    return n - M2(tmp);
  }
}

int M2(int n){
  if( n == 0 ) return 0;
  { int tmp = M2(n-1);
    return val2(n) - 1 - G2(tmp);
  }
}

int G2(int n){
  return F2(n);
}

int main2(){
  int i=0, out=0;
  for( i=0 ; i < 20 ; i++ ){
    out = F2(i);
    if( i > 25 ) return 12;
  }
  for( i=0 ; i < 20 ; i++ ){
    int tmp = M2(i);
    out = val2(tmp) - 1;
  }
  return out;
}

/* The following is original.

int M1(int n);

int val1(int x){
  return x;
}

int F1(int n){
  if( n == 0 ) return 1;
  return n - M1(F1(n-1));
}

int M1(int n){
  if( n == 0 ) return 0;
  return n - F1(M1(n-1));
}

int main1(){
  int i=0, out=0;
  for( i=0 ; i < 20 ; i++ ){
    out = F1(i);
    if( i > 20 ) return 3;
  }
  for( i=0 ; i < 20 ; i++ ){
    out = val1(M1(i));
  }
  return out;
}

int M2(int n);
int G2(int n);

int val2(int x){
  return x + 1;
}

int F2(int n){
  if( n == 0 ) return (n == 0);
  return n - M2(F2(n-1));
}

int M2(int n){
  if( n == 0 ) return 0;
  return val2(n) - 1 - G2(M2(n-1));
}

int G2(int n){
  return F2(n);
}

int main2(){
  int i=0, out=0;
  for( i=0 ; i < 20 ; i++ ){
    out = F2(i);
    if( i > 25 ) return 12;
  }
  for( i=0 ; i < 20 ; i++ ){
    out = val2(M2(i)) - 1;
  }
  return out;
}

*/
