MACHINE TuringMachine_Cook_SAT
SETS /* enumerated */
  Alphabet={O,I,`◻︎`};
  States={z0,z1,z2,ze};
  Direction={L,R,N}
CONCRETE_CONSTANTS
  Final,
  δ,
  state,
  head,
  tape
PROPERTIES
    δ = {z0 |-> O |-> (z0 |-> O |-> R),z0 |-> I |-> (z0 |-> I |-> R),z0 |-> `◻︎` |-> (z1 |-> `◻︎` |-> L),z1 |-> O |-> (z2 |-> I |-> L),z1 |-> I |-> (z1 |-> O |-> L),z1 |-> `◻︎` |-> (ze |-> I |-> N),z2 |-> O |-> (z2 |-> O |-> L),z2 |-> I |-> (z2 |-> I |-> L),z2 |-> `◻︎` |-> (ze |-> `◻︎` |-> R)}
  & Final = {ze}
  & state : (0 .. 6) * States --> BOOL
  & head : (0 .. 6) * (-6 .. 6) --> BOOL
  & tape : (0 .. 6) * (-6 .. 6) * Alphabet --> BOOL
  & !t.(
     t : 0 .. 6
     =>
     card({s|state(t |-> s) = TRUE}) = 1
    )
  & !t.(
     t : 0 .. 6
     =>
     card({p|p : -6 .. 6 & head(t |-> p) = TRUE}) = 1
    )
  & !t.(
     t : 0 .. 6
     =>
     !p.(
      p : -6 .. 6
      =>
      card({s|tape(t |-> p |-> s) = TRUE}) = 1
     )
    )
  & state(0 |-> z0) = TRUE
  & head(0 |-> 0) = TRUE
  & !i.(
     i : -6 .. -1
     =>
     tape(0 |-> i |-> `◻︎`) = TRUE
    )
  & tape(0 |-> 0 |-> I) = TRUE
  & tape(0 |-> 1 |-> O) = TRUE
  & !i.(
     i : 2 .. 6
     =>
     tape(0 |-> i |-> `◻︎`) = TRUE
    )
  & !t.(
     t : 0 .. 5
     =>
     !(s,i,a).(
      i : -6 .. 6
      =>
      (
       (
        state(t |-> s) = TRUE
        &
        head(t |-> i) = TRUE
        &
        tape(t |-> i |-> a) = TRUE
       )
       =>
       #(s2,a2,y).(
        s |-> a |-> (s2 |-> a2 |-> y) : δ
        &
        i + {L |-> -1,R |-> 1,N |-> 0}(y) : -6 .. 6
        &
        state(t + 1 |-> s2) = TRUE
        &
        head(t + 1 |-> i + {L |-> -1,R |-> 1,N |-> 0}(y)) = TRUE
        &
        tape(t + 1 |-> i |-> a2) = TRUE
       )
      )
     )
    )
  & #s.(
     s : Final
     &
     state(6 |-> s) = TRUE
    )
ASSERTIONS
     !t.(
      t : 0 .. 6
      =>
      card({s|state(t |-> s) = TRUE}) = 1
     )
     &
     !t.(
      t : 0 .. 6
      =>
      card({p|p : -6 .. 6 & head(t |-> p) = TRUE}) = 1
     )
     &
     !t.(
      t : 0 .. 6
      =>
      !p.(
       p : -6 .. 6
       =>
       card({s|tape(t |-> p |-> s) = TRUE}) = 1
      )
     )
   ; state(0 |-> z0) = TRUE
     &
     head(0 |-> 0) = TRUE
     &
     !i.(
      i : -6 .. -1
      =>
      tape(0 |-> i |-> `◻︎`) = TRUE
     )
     &
     tape(0 |-> 0 |-> I) = TRUE
     &
     tape(0 |-> 1 |-> O) = TRUE
     &
     !i.(
      i : 2 .. 6
      =>
      tape(0 |-> i |-> `◻︎`) = TRUE
     )
   ; !t.(
      t : 0 .. 5
      =>
      !(s,i,a).(
       i : -6 .. 6
       =>
       (
        (
         state(t |-> s) = TRUE
         &
         head(t |-> i) = TRUE
         &
         tape(t |-> i |-> a) = TRUE
        )
        =>
        #(s2,a2,y).(
         s |-> a |-> (s2 |-> a2 |-> y) : δ
         &
         i + {L |-> -1,R |-> 1,N |-> 0}(y) : -6 .. 6
         &
         state(t + 1 |-> s2) = TRUE
         &
         head(t + 1 |-> i + {L |-> -1,R |-> 1,N |-> 0}(y)) = TRUE
         &
         tape(t + 1 |-> i |-> a2) = TRUE
        )
       )
      )
     )
   ; !t.(
      t : 0 .. 5
      =>
      !(i,a).(
       i : -6 .. 6
       =>
       (
        (
         head(t |-> i) = FALSE
         &
         tape(t |-> i |-> a) = TRUE
        )
        =>
        tape(t + 1 |-> i |-> a) = TRUE
       )
      )
     )
   ; #s.(
      s : Final
      &
      state(6 |-> s) = TRUE
     )
INITIALISATION
    skip
DEFINITIONS
 "LibraryStrings.def";
 SET_PREF_RANDOMISE_ENUMERATION_ORDER == TRUE;
 SET_PREF_SMT == TRUE;
 SET_PREF_SOLVER_FOR_PROPERTIES == sat-z3;
 SET_PREF_SOLVER_STRENGTH == 1000;
 SET_PREF_TIME_OUT == 10000;

/* DEFINITIONS
  PREDICATE STRING_IS_ALPHANUMERIC(sss);
  PREDICATE Formula_E;
  PREDICATE Formula_K;
  EXPRESSION REAL_TO_DEC_STRING(realnr,precision);
  PREDICATE Formula_S;
  EXPRESSION SET_PREF_SOLVER_STRENGTH == 
  1000;
  EXPRESSION STRING_CHARS(xxx);
  EXPRESSION STRING_TO_REAL(sss);
  EXPRESSION VISB_SVG_HOVERS_state;
  PREDICATE STRING_EQUAL_CASE_INSENSITIVE(sss1,sss2);
  EXPRESSION STRING_APPEND(xxx,yyy);
  EXPRESSION VISB_SVG_OBJECTS_State;
  EXPRESSION TYPED_STRING_TO_ENUM(t,sss);
  PREDICATE STRING_IS_INT(sss);
  EXPRESSION GET_STRING_IS_NUMBER(sss);
  EXPRESSION StateNr;
  PREDICATE STRING_IS_NUMBER(sss);
  EXPRESSION FORMAT_TO_STRING(MyFormatString,ListOfValues);
  EXPRESSION POS;
  EXPRESSION GET_STRING_IS_ALPHANUMERIC(sss);
  EXPRESSION GET_STRING_IS_DECIMAL(sss);
  EXPRESSION STRING_CODES(string_codes_str);
  EXPRESSION OFF == 
  2;
  EXPRESSION VISB_JSON_FILE;
  EXPRESSION VISB_SVG_BOX;
  EXPRESSION GET_STRING_EQUAL_CASE_INSENSITIVE(sss1,sss2);
  EXPRESSION VISB_SVG_OBJECTS3_InfoText;
  EXPRESSION GET_STRING_IS_INT(sss);
  EXPRESSION STRING_PADLEFT(padleft_string,padleft_width,padleft_char);
  EXPRESSION STRING_TO_INT(sss);
  EXPRESSION STRING_REV(xxx);
  EXPRESSION SET_PREF_RANDOMISE_ENUMERATION_ORDER == 
  TRUE;
  PREDICATE STRING_IS_FREETYPE(sss);
  EXPRESSION INT_TO_STRING(sss);
  EXPRESSION STRING_CONTAINS_STRING(arg1,arg2);
  EXPRESSION INT_TO_DEC_STRING(integer,precision);
  EXPRESSION VISB_SVG_HOVERS_head;
  EXPRESSION SUB_STRING(substring_str,substring_from,substring_to);
  EXPRESSION STRING_LENGTH(xxx);
  EXPRESSION STRING_CONC(string_conc_list);
  EXPRESSION STRING_REPLACE(orig_str,pat_str,new_str);
  EXPRESSION SET_PREF_TIME_OUT == 
  10000;
  EXPRESSION STRING_JOIN(xxx,yyy);
  EXPRESSION TO_STRING(sss);
  EXPRESSION VISB_SVG_OBJECTS_Head;
  EXPRESSION INT_TO_HEX_STRING(integer);
  EXPRESSION VISB_SVG_HOVERS_tape;
  EXPRESSION offset;
  EXPRESSION VISB_SVG_OBJECTS_Tape;
  EXPRESSION WID;
  EXPRESSION STRING_TO_ENUM(sss);
  EXPRESSION STRING_SPLIT(xxx,yyy);
  PREDICATE Formula_U1;
  PREDICATE Formula_U2;
  EXPRESSION TIME1;
  EXPRESSION STRING_TO_LOWER(string_to_lower_str);
  EXPRESSION DEC_STRING_TO_INT(decimal_string,precision);
  EXPRESSION CODES_TO_STRING(codes_to_string_seq);
  PREDICATE STRING_IS_DECIMAL(sss);
  EXPRESSION SET_PREF_SMT == 
  TRUE;
  EXPRESSION TIME;
  EXPRESSION HEIGHT == 
  13;
  EXPRESSION STRING_TO_UPPER(string_to_upper_str);
  EXPRESSION SET_PREF_SOLVER_FOR_PROPERTIES;
  EXPRESSION STRING_TO_FREETYPE(sss);
  EXPRESSION STRINGIFY(sss);
  EXPRESSION pn == 
  6; */
END