─────╷────────── $𝖕𝖗𝖑𝖕/𝖕𝖚𝖗𝖊-𝖑𝖔𝖔𝖕-𝖗𝖚𝖑𝖊𝖘.𝖘𝖆𝖕𝖕𝖍𝖎𝖗𝖊 ──────────────────────────────────────────────────────

    0┊------------------------| Sapphire Rules for Pure Loop Pencil Puzzles |-------------------------

    1┊--|∙An∙n×m∙grid∙of∙cells,∙some∙open,∙some∙blocked;∙no∙row∙or∙column∙is∙entirely∙blocked        

    2┊--|∙The∙solution∙is∙a∙single,∙non-intersecting∙conterclockwise∙loop∙through∙all∙open∙squares   

    3┊                                                                                               

    4┊--|∙sol∙-∙solution∙giving∙the∙direction∙of∙loop∙travel:∙0∙1∙2∙3∙indicate∙↑∙↓∙←∙→,∙respectfully 

    5┊--|∙∙∙∙∙-∙if∙4,∙cell∙is∙closed                                                                 

    6┊                                                                                               

    7┊Idx={0⋯n⨫1}×{0⋯m⨫1}∙--|∙0∙based∙indexing∙by∙pairs                                              

    8┊                                                                                               

    9┊x0∈{0⋯n⨫2}∙∧∙⦗id∙x0∙0⦘=0                                                                       

   10┊                                                                                               

   11┊∀⟨x∙y⟩∈Idx                                                                                     

   12┊∙∙⦗id∙x∙y⦘∈{0⋯n·m}                                                                             

   13┊∙∙⦗id∙x∙y⦘=0∙⇐⇒∙x=x0∙∧∙y=0                                                                     

   14┊∙∙⦗sol∙x∙y⦘∈{0⋯4}                                                                              

   15┊∙∙⦗sol∙x∙y⦘=4∙⇐⇒∙⦗id∙x∙y⦘=n·m                                                                  

   16┊∙∙x=0∙∙∙⇒∙⦗sol∙x∙y⦘∈{1∙3∙4}                                                                    

   17┊∙∙x=n⨫1∙⇒∙⦗sol∙x∙y⦘∈{0∙2∙4}                                                                    

   18┊∙∙y=0∙∙∙⇒∙⦗sol∙x∙y⦘∈{0∙3∙4}                                                                    

   19┊∙∙y=m⨫1∙⇒∙⦗sol∙x∙y⦘∈{1∙2∙4}                                                                    

   20┊∙∙⦗sol∙x∙y⦘=0∙⇒∙y<m⨫1∙∧∙⦗sol∙x∙y+1⦘∈{0∙2∙3}                                                    

   21┊∙∙⦗sol∙x∙y⦘=1∙⇒∙y>0∙∙∙∧∙⦗sol∙x∙y⨫1⦘∈{1∙2∙3}                                                    

   22┊∙∙⦗sol∙x∙y⦘=2∙⇒∙x>0∙∙∙∧∙⦗sol∙x⨫1∙y⦘∈{0∙1∙2}                                                    

   23┊∙∙⦗sol∙x∙y⦘=3∙⇒∙x<n⨫1∙∧∙⦗sol∙x+1∙y⦘∈{0∙1∙3}                                                    

   24┊∙∙⦗sol∙x∙y⦘¬=4∙⇒∙y>0∙∙∙∧∙⦗sol∙x∙y⨫1⦘=0∙∧∙⦗id∙x∙y⦘=⦗id∙x∙y⨫1⦘+1∙∨                               

   25┊∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙y<m⨫1∙∧∙⦗sol∙x∙y+1⦘=1∙∧∙⦗id∙x∙y⦘=⦗id∙x∙y+1⦘+1∙∨                               

   26┊∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙x>0∙∙∙∧∙⦗sol∙x⨫1∙y⦘=3∙∧∙⦗id∙x∙y⦘=⦗id∙x⨫1∙y⦘+1∙∨                               

   27┊∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙x<n⨫1∙∧∙⦗sol∙x+1∙y⦘=2∙∧∙⦗id∙x∙y⦘=⦗id∙x+1∙y⦘+1∙∨                               

   28┊∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙x=x0∙∧∙y=0∙∧∙⦗sol∙x∙y⦘=3∙∧∙⦗sol∙x∙y+1⦘=1∙∧∙⦗id∙x∙y⦘=0                         

   29┊                                                                                               

   30┊--|∙Getting∙stuck∙on∙alternative∙to∙above,∙without∙the∙"x=x0∙∧∙..."∙line                       

   31┊--|∙but∙with∙the∙"y<m⨫1∙∧∙..."∙line∙being                                                      

   32┊--|∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙y<m⨫1∙∧∙⦗sol∙x∙y+1⦘=1∙∧∙(⦗id∙x∙y⦘=⦗id∙x∙y+1⦘+1∙∨∙⦗id∙x∙y⦘=0)∙∨             

   33┊--|∙Not∙sure∙where∙the∙bug∙in∙the∙alternative∙is:∙here∙or∙in∙Ag                                

   34┊                                                                                               

   35┊∀x∈{0⋯n⨫1}∙⦗sol∙x∙0⦘¬=4∙∧∙(x=0∙∨∙∀x'∈{0⋯x⨫1}∙⦗sol∙x'∙0⦘=4)∙⇐⇒∙⦗id∙x∙0⦘=0                       

   36┊                                                                                               

   37┊--|∙add∙in?∙to∙help∙solver∙(many∙x∙speedup);∙want∙to∙automate∙this∙in∙future                   

   38┊∀⟨x∙y⟩∈{0⋯n}×{0⋯m}                                                                             

   39┊∙∙⦗in?∙x∙y⦘∈{0∙1}                                                                              

   40┊∙∙x=0∙∨∙y=0∙∨∙x=n∙∨∙y=m∙⇒∙⦗in?∙x∙y⦘=0                                                          

   41┊∙∙x>0∙∧∙y>0∙∧∙y<m∙⇒∙(⦗in?∙x∙y⦘=⦗in?∙x⨫1∙y⦘∙⇐⇒∙⦗sol∙x⨫1∙y⨫1⦘¬=0∧⦗sol∙x⨫1∙y⦘¬=1)                 

   42┊∙∙x>0∙∧∙x<n∙∧∙y>0∙⇒∙(⦗in?∙x∙y⦘=⦗in?∙x∙y⨫1⦘∙⇐⇒∙⦗sol∙x⨫1∙y⨫1⦘¬=3∧⦗sol∙x∙y⨫1⦘¬=2)                 

─────╵────────────────────────────────────────────────────────────────────────────────────────────────