find_linear_modular: THEORY
BEGIN

  PCt: TYPE = { L1, L2, L3, L4, L5, L6, L7, L8, LEND }

  C: TYPE = [#
    size: nat,
    a: [nat -> integer],
    x: integer,
    i: nat,
    result: bool,
    PC: PCt
  #]

  L1(c: C):C= c WITH [i:=0]
  L2(c: C):C= c
  L3(c: C):C= c
  L4(c: C):C= c WITH [result:=TRUE]
  L5(c: C):C= c
  L6(c: C):C= c WITH [i:=c`i+1]
  L7(c: C):C= c
  L8(c: C):C= c WITH [result:=FALSE]

  t(c: C):C=CASES c`PC OF
    L1: L1(c) WITH [PC:=L2],
    L2: L2(c) WITH [PC:=IF NOT c`i < c`size THEN L8 ELSE L3 ENDIF],
    L3: L3(c) WITH [PC:=IF NOT c`a(c`i)=c`x THEN L6 ELSE L4 ENDIF],
    L4: L4(c) WITH [PC:=L5],
    L5: L5(c) WITH [PC:=LEND],
    L6: L6(c) WITH [PC:=L7],
    L7: L7(c) WITH [PC:=L2],
    L8: L8(c) WITH [PC:=LEND],
    LEND: c
  ENDCASES

  c(T: nat, initial: C):RECURSIVE C=
    IF T=0 THEN
      initial WITH [PC:=L1]
    ELSE
      t(c(T-1, initial))
    ENDIF MEASURE T

  correct_result(c: C): bool=
    EXISTS (i: below(c`size)): c`a(i)=c`x

  invar_constants(T: nat, initial: C): bool=
    c(T, initial)`size=initial`size AND
    c(T, initial)`a   =initial`a    AND
    c(T, initial)`x   =initial`x;

  constants: LEMMA
    FORALL (initial:C, T: nat):
    invar_constants(T, initial)

  invar(c: C):bool=CASES c`PC OF
    L1: TRUE,
    L2: FORALL (j: below(c`i)): c`a(j)/=c`x,
    L3: c`i<c`size AND FORALL (j: below(c`i)): c`a(j)/=c`x,
    L4: c`i<c`size AND c`a(c`i)=c`x,
    L5: c`i<c`size AND c`a(c`i)=c`x AND c`result=true,
    L6: FORALL (j: below(c`i+1)): c`a(j)/=c`x,
    L7: FORALL (j: below(c`i)): c`a(j)/=c`x,
    L8: c`i>=c`size AND FORALL (j: below(c`i)): c`a(j)/=c`x,
    LEND: c`result <=> EXISTS (j: below(c`size)): c`a(j)=c`x
  ENDCASES

  invar_step: LEMMA
    FORALL (c: C | invar(c)): invar(t(c))

  invar_holds: LEMMA
    FORALL (initial: C, T: nat): invar(c(T, initial))

  c_correct: THEOREM
    FORALL (initial: C):
    FORALL (T: nat | c(T, initial)`PC=LEND):
    c(T, initial)`result=correct_result(initial)

  termination: THEOREM
    FORALL (initial: C):
    EXISTS (T: nat): c(T, initial)`PC=LEND

  find_linear(start: C): C=
    c(epsilon! (T: nat): c(T, start)`PC=LEND, start)

  find_linear_correct: THEOREM
    FORALL (c: C):
    LET new=find_linear(c) IN
    new=c WITH
      [result:=correct_result(c),
       PC:=new`PC,
       i:=new`i]

END find_linear_modular