text: // This contrived example is not useful in any way; it just shows that you can do mutual lemma recursion using lemma function pointer chunks.
  
  /*@
  
  typedef lemma void oddfunc(oddfunc *odd, evenfunc *even, int x);
      requires multi_is_oddfunc(odd, x) &*& multi_is_evenfunc(even, x);
      ensures multi_is_oddfunc(odd, x) &*& multi_is_evenfunc(even, x);
  
  typedef lemma void evenfunc(oddfunc *odd, evenfunc *even, int x);
      requires multi_is_oddfunc(odd, x) &*& multi_is_evenfunc(even, x);
      ensures multi_is_oddfunc(odd, x) &*& multi_is_evenfunc(even, x);
  
  predicate multi_is_oddfunc(oddfunc *odd, int n) = n <= 0 ? emp : is_oddfunc(odd) &*& multi_is_oddfunc(odd, n - 1);
  predicate multi_is_evenfunc(evenfunc *even, int n) = n <= 0 ? emp : is_evenfunc(even) &*& multi_is_evenfunc(even, n - 1);
  
  lemma void odd_lemma(oddfunc *odd, evenfunc *even, int x) : oddfunc
      requires multi_is_oddfunc(odd, x) &*& multi_is_evenfunc(even, x);
      ensures multi_is_oddfunc(odd, x) &*& multi_is_evenfunc(even, x);
  {
      open multi_is_oddfunc(odd, x);
      open multi_is_evenfunc(even, x);
      if (x <= 0) {
      } else {
          even(odd, even, x - 1);
      }
      close multi_is_oddfunc(odd, x);
      close multi_is_evenfunc(even, x);
  }
  
  lemma void even_lemma(oddfunc *odd, evenfunc *even, int x) : evenfunc
      requires multi_is_oddfunc(odd, x) &*& multi_is_evenfunc(even, x);
      ensures multi_is_oddfunc(odd, x) &*& multi_is_evenfunc(even, x);
  {
      open multi_is_oddfunc(odd, x);
      open multi_is_evenfunc(even, x);
      if (x <= 0) {
      } else {
          odd(odd, even, x - 1);
      }
      close multi_is_oddfunc(odd, x);
      close multi_is_evenfunc(even, x);
  }
  
  inductive nat = zero | succ(nat);
  
  fixpoint int int_of_nat(nat n) {
      switch (n) {
          case zero: return 0;
          case succ(m): return 1 + int_of_nat(m);
      }
  }
  
  lemma void int_of_nat_nonneg(nat n)
      requires true;
      ensures 0 <= int_of_nat(n);
  {
      switch (n) {
          case zero:
          case succ(m):
              int_of_nat_nonneg(m);
      }
  }
  
  lemma void produce_chunks(int m, nat n)
      requires multi_is_oddfunc(odd_lemma, m - int_of_nat(n)) &*& multi_is_evenfunc(even_lemma, m - int_of_nat(n));
      ensures multi_is_oddfunc(odd_lemma, m - int_of_nat(n)) &*& multi_is_evenfunc(even_lemma, m - int_of_nat(n));
  {
      switch (n) {
          case zero: 
              odd_lemma(odd_lemma, even_lemma, m);
          case succ(n0):
              int_of_nat_nonneg(n0);
              produce_lemma_function_pointer_chunk(odd_lemma) {
                produce_lemma_function_pointer_chunk(even_lemma) {
                  close multi_is_oddfunc(odd_lemma, m - int_of_nat(n0));
                  close multi_is_evenfunc(even_lemma, m - int_of_nat(n0));
                  produce_chunks(m, n0);
                  open multi_is_oddfunc(odd_lemma, m - int_of_nat(n0));
                  open multi_is_evenfunc(even_lemma, m - int_of_nat(n0));
                }
              }
      }
  }
  lemma void main_lemma(nat n)
      requires true;
      ensures true;
  {
      close multi_is_evenfunc(even_lemma, 0);
      close multi_is_oddfunc(odd_lemma, 0);
      produce_chunks(int_of_nat(n), n);
      open multi_is_evenfunc(even_lemma, 0);
      open multi_is_oddfunc(odd_lemma, 0);
  }
  
  @*/