(*
  rulefit  1RB0LC_1RC0RA_1RD0RF_0LE---_1LB1LA_1LD1RA
  hub: record L:C (direct, 158 transitions observed), 1 validated rule(s), coverage 61%, closed

  C0(a,b,c,d) := 0^inf <C 01^a 001101^b 01^c 001^d 0^inf
  C1(a,b,c,d) := 0^inf <C 01^a 001101^b 01^c 001^d 001101^3 01^6 001^14 0^inf
  C2(a,b,c) := 0^inf <C 01^a 001101^4 01^18 001101^3 01^b 001^c 0^inf
  C3(a,b) := 0^inf <C 01^a 001101^7 01^19 10^b 010^9 010011^3 01^7 001^14 0^inf
  C4(a,b) := 0^inf <C 01^a 001101^7 01^18 0 01^b 001^10 001101^3 01^6 001^14 0^inf
  C5(a,b,c) := 0^inf <C 01^a 001101^9 01^6 0011 01^b 001^c 0^inf
  C6 := 0^inf <C 01^2 0011 01^3 001^4 10^4 01001 0^inf
  C7 := 0^inf <C 0 101001^7 10^16 010011^4 01^9 001^10 001101^3 01^6 001^14 0^inf
  C8 := 0^inf <C 01^46 001101^7 01^30 101001^2 10^8 010^14 0^inf
  start: C0(3, 0, 0, 0) (first visit, step 28)

  C0(a, b, c, d+2) --> C0(a+2, b, c+2, d)   steps 6a+20b+6c+16   [21/21 sims, 96 obs]

  killed by validation: 1 fitted case(s)
*)

(*
  rulefit  1RB0LC_1RC0RA_1RD0RF_0LE---_1LB1LA_1LD1RA
  hub: record L:A (direct, 158 transitions observed), 2 validated rule(s), coverage 23%, closed

  A0(a,b,c,d) := 0^inf <A 10^a 011010^b 10^c 010^d 0^inf
  A1(a,b,c,d) := 0^inf <A 10^a 011010^b 10^c 010^d 010011^3 01^7 001^14 0^inf
  A2(a,b,c) := 0^inf <A 10^a 011010^4 10^18 011010^3 10^b 010^c 0^inf
  A3(a,b) := 0^inf <A 10^a 011010^7 10^18 1 10^b 010^9 010011^3 01^7 001^14 0^inf
  A4(a,b) := 0^inf <A 10^a 011010^7 10^18 01^b 001^10 001101^3 01^6 001^14 0^inf
  A5 := 0^inf <A 10111010011 01^3 001^2 0^inf
  A6 := 0^inf <A 1001101 001^6 10^4 01001 0^inf
  A7 := 0^inf <A 10 1^3 010011^3 01^7 001^14 0^inf
  A8 := 0^inf <A 1011 101001^9 10^8 011 01^15 001^4 0^inf
  A9 := 0^inf <A 100110^7 10^13 010^3 011010^4 10^8 010^9 010011^3 01^7 001^14 0^inf
  A10 := 0^inf <A 10^47 011010^7 10^29 1^2 010011^2 01^7 001^14 0^inf

  A0(5n+1, b, c, d+2)               --> A0(5n+3, b, c+2, d)                 steps 20b+6c+30n+16   [21/21 sims, 19 obs]
  A0(5n+2, b+3, 2b+5n+3, 38b-5n+17) --> A0(5n+4, b+3, 2b+5n+5, 38b-5n+15)   steps ?              if 38b-5n >= -15 [19/19 sims, 18 obs]

  killed by validation: 4 fitted case(s)
*)

(*
  rulefit  1RB0LC_1RC0RA_1RD0RF_0LE---_1LB1LA_1LD1RA
  hub: qsim edge A:R (qsim, 11 transitions observed), 1 validated rule(s), coverage 18%

  A0(a,b,c,d,e) := 0^inf 10^a 101^b 10^c 101^d 10^e A> 0^inf
  A1(a,b,c,d,e,f,g) := 0^inf 10^a 101^b 10^c 101^d 10^e 101^f 10^g A> 0^inf
  start: A0(1, 5, 2, 2, 3) (first visit, step 690)

  A0(60n+8, b, c, d, e) --> A1(55n+13, 37n+15, 40n+8, 39n+18, 26n+6, 3n+2, -16n+19)   steps ?  if 60n+8 <= 79 [1/1 sims, 2 obs]

  killed by validation: 3 fitted case(s)
  uncovered cases probed: 108 (no rule yet)
*)

(* low-level rules: sligocki prover (block size 6, 2000 loops), normalised to plain tapes, re-verified by direct simulation: 1/1 OK
   [0] 0^inf 10^(3a+9) 101^(2b+2) <A 1 0^2 1^2 0 10^(3c+6) 100^(2d+8) 0^inf  -->  0^inf 10^(3a+3) 101^(2b+8) <A 1 0^2 1^2 0 10^(3c+12) 100^(2d+2) 0^inf   steps 60b+54c+348   verified 10/10  (decrement >= 2: needs a mod split)
*)