diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-08-16 15:04:14 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-13 19:21:13 -0400 |
| commit | 24b4ca565400d64b82626484044f72fd024477cd (patch) | |
| tree | 0f35b74427607bf5f6d97ec3f0f109182be022fd /test/regress/regress2/bug497.cvc | |
| parent | 14776d0aeb833a7e728a27af6ef545f20b495f7f (diff) | |
Move some regress benchmarks around that took too long, other test cleanup.
Diffstat (limited to 'test/regress/regress2/bug497.cvc')
| -rw-r--r-- | test/regress/regress2/bug497.cvc | 920 |
1 files changed, 920 insertions, 0 deletions
diff --git a/test/regress/regress2/bug497.cvc b/test/regress/regress2/bug497.cvc new file mode 100644 index 000000000..ce34ab6ad --- /dev/null +++ b/test/regress/regress2/bug497.cvc @@ -0,0 +1,920 @@ +% COMMAND-LINE: --decision=justification --incremental +% EXPECT: sat +% EXPECT: sat +% EXIT: 10 +OPTION "logic" "QF_UFLIA"; +_nat : TYPE = INT; +_base : INT; +ASSERT _base <= 0; +_n : _nat; +ASSERT _n >= _base; +_check_quant : BOOLEAN; + +% maxdepth = 1 +x100 : _nat -> INT; + % Chart_main_simp_rlt_node_state126_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState % LOCAL/200 +x101 : _nat -> INT; + % Chart_main_simp_rlt_node_state122_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState % LOCAL/201 +x2 : _nat -> INT; + % GroundTrack_OrbitalPosition % INPUT,STATE(1,)/102 +x102 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_OrbitalState_Attitude % LOCAL,STATE(1,)/202 +x3 : _nat -> INT; + % GroundTrack_OrbitalVelocity % INPUT,STATE(1,)/103 +x103 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteVelocity % LOCAL/203 +x4 : _nat -> INT; + % dockVisibility_status % INPUT,STATE(1,)/104 +x104 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_InertialNavigation_AbsolutePosition % LOCAL/204 +x5 : _nat -> BOOLEAN; + % opticsAvailability_status % INPUT,STATE(1,)/105 +x105 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_InertialNavigation_timer % LOCAL/205 +x6 : _nat -> BOOLEAN; + % sunlight_status % INPUT,STATE(1,)/106 +x106 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_OrbitalState_Velocity % LOCAL,STATE(1,)/206 +x7 : _nat -> INT; + % GPS_satelliteVisibility_status % INPUT,STATE(1,)/107 +x107 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_OrbitalState_Position % LOCAL,STATE(1,)/207 +x8 : _nat -> BOOLEAN; + % GPS_receiverAvailability_status % INPUT,STATE(1,)/108 +x108 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteAttitude % LOCAL/208 +x9 : _nat -> INT; + % StarPlanetTracker_planetVisibility % INPUT,STATE(1,)/109 +x109 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState % LOCAL,STATE(1,)/209 +x10 : _nat -> INT; + % StarPlanetTracker_starVisibility % INPUT,STATE(1,)/110 +x110 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation % LOCAL/210 +x11 : _nat -> BOOLEAN; + % InertialNavigation_time % INPUT/111 +x111 : _nat -> INT; + % Chart_main_simp_rlt_node_state367_rlt_chart_data_vars_Chart_OrbitalState_Time % LOCAL,STATE(1,)/211 +x12 : _nat -> INT; + % GroundTrack_Time % INPUT/112 +x112 : _nat -> INT; + % Chart_main_simp_rlt_node_state367_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState2 % LOCAL,STATE(1,)/212 +x13 : _nat -> INT; + % RealTimeClock_time % INPUT,STATE(1,)/113 +x113 : _nat -> INT; + % Chart_main_simp_rlt_node_state499_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteVelocity % LOCAL,STATE(1,)/213 +x14 : _nat -> INT; + % StageTransition % INPUT,STATE(1,)/114 +x114 : _nat -> INT; + % Chart_main_simp_rlt_node_state499_rlt_chart_data_vars_Chart_InertialNavigation_AbsolutePosition % LOCAL,STATE(1,)/214 +x15 : _nat -> BOOLEAN; + % CaptureApproachComplete % OUTPUT,STATE(1,)/115 +x115 : _nat -> INT; + % Chart_main_simp_rlt_node_state499_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteAttitude % LOCAL,STATE(1,)/215 +x16 : _nat -> BOOLEAN; + % DockingApproachComplete % OUTPUT,STATE(1,)/116 +x116 : _nat -> INT; + % Chart_main_simp_rlt_node_state499_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation % LOCAL,STATE(1,)/216 +x17 : _nat -> BOOLEAN; + % AttemptingToDock % OUTPUT,STATE(1,)/117 +x117 : _nat -> INT; + % Chart_main_simp_rlt_node_state627_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_dockingSensor % LOCAL,STATE(1,)/217 +x118 : _nat -> INT; + % Chart_main_simp_rlt_node_state545_rlt_chart_data_vars_Chart_dockingSensor_timer % LOCAL/218 +x119 : _nat -> INT; + % Chart_main_simp_rlt_node_state545_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_dockingSensor % LOCAL/219 +x20 : _nat -> BOOLEAN; + % ApproachOrbitComplete % OUTPUT,STATE(1,)/120 +x120 : _nat -> INT; + % Chart_main_simp_rlt_node_state542_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_dockingSensor % LOCAL/220 +x21 : _nat -> BOOLEAN; + % FarApproachComplete % OUTPUT,STATE(1,)/121 +x121 : _nat -> INT; + % Chart_main_simp_rlt_node_state540_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_dockingSensor % LOCAL/221 +x22 : _nat -> BOOLEAN; + % ProximityOperationsComplete % OUTPUT,STATE(1,)/122 +x122 : _nat -> INT; + % Chart_main_simp_rlt_node_state765_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch % LOCAL,STATE(1,)/222 +x123 : _nat -> INT; + % Chart_main_simp_rlt_node_state690_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_LatchCaptureCheck % LOCAL,STATE(1,)/223 +x124 : _nat -> INT; + % Chart_main_simp_rlt_node_state706_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch % LOCAL/224 +x125 : _nat -> INT; + % Chart_main_simp_rlt_node_state702_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch % LOCAL/225 +x26 : _nat -> INT; + % MWI_FcnMin_Out110 % LOCAL,STATE(1,)/126 +x126 : _nat -> INT; + % Chart_main_simp_rlt_node_state759_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch % LOCAL/226 +x27 : _nat -> INT; + % MWI_FcnMin_Out19 % LOCAL,STATE(1,)/127 +x127 : _nat -> INT; + % Chart_main_simp_rlt_node_state757_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch % LOCAL/227 +x28 : _nat -> INT; + % MWI_FcnMin_In1n8 % LOCAL/128 +x128 : _nat -> INT; + % Chart_main_simp_rlt_node_state753_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch % LOCAL/228 +x29 : _nat -> INT; + % MWI_FcnMin_Out18 % LOCAL,STATE(1,)/129 +x129 : _nat -> BOOLEAN; + % sequence1 % LOCAL/229 +x30 : _nat -> INT; + % MWI_FcnMin_Out17 % LOCAL/130 +x31 : _nat -> INT; + % MWI_FcnMin_Out13 % LOCAL,STATE(1,)/131 +x32 : _nat -> INT; + % MWI_FcnMin_Out12 % LOCAL,STATE(1,)/132 +x33 : _nat -> INT; + % MWI_FcnMin_Out11 % LOCAL,STATE(1,)/133 +x34 : _nat -> INT; + % MWI_FcnMin_In1n % LOCAL/134 +x35 : _nat -> INT; + % MWI_FcnMin_Out1 % LOCAL,STATE(1,)/135 +x36 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_OrbitalState_Time % LOCAL,STATE(1,)/136 +x37 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_LatchCapture_timer % LOCAL,STATE(1,)/137 +x38 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_StarPlanetTracker_timer % LOCAL,STATE(1,)/138 +x39 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_OrbitalState_Attitude % LOCAL,STATE(1,)/139 +x40 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_CaptureApproach_timer % LOCAL,STATE(1,)/140 +x41 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_GPS_timer % LOCAL,STATE(1,)/141 +x42 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteVelocity % LOCAL,STATE(1,)/142 +x43 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_InertialNavigation_AbsolutePosition % LOCAL,STATE(1,)/143 +x44 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_InertialNavigation_timer % LOCAL,STATE(1,)/144 +x45 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_latch_status % LOCAL,STATE(1,)/145 +x46 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_dockingSensor_timer % LOCAL,STATE(1,)/146 +x47 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_OrbitalState_Velocity % LOCAL,STATE(1,)/147 +x48 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_OrbitalState_Position % LOCAL,STATE(1,)/148 +x49 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_dockingSensor_RelativeAttitude % LOCAL,STATE(1,)/149 +x50 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_GPS_AbsolutePosition % LOCAL,STATE(1,)/150 +x51 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_DockingApproach_timer % LOCAL,STATE(1,)/151 +x52 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteAttitude % LOCAL,STATE(1,)/152 +x53 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_StarPlanetTracker_AbsolutePosition % LOCAL,STATE(1,)/153 +x54 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_dockingSensor % LOCAL,STATE(1,)/154 +x55 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_DockingApproach % LOCAL,STATE(1,)/155 +x56 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch % LOCAL,STATE(1,)/156 +x57 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_LatchCaptureCheck % LOCAL,STATE(1,)/157 +x58 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_GPS % LOCAL,STATE(1,)/158 +x59 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart % LOCAL,STATE(1,)/159 +x60 : _nat -> [0..2]; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState2 % LOCAL,STATE(1,)/160 +x61 : _nat -> [0..4]; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState % LOCAL,STATE(1,)/161 +x62 : _nat -> [0..3]; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_StarPlanetTracker % LOCAL,STATE(1,)/162 +x63 : _nat -> [0..5]; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_CaptureApproach % LOCAL,STATE(1,)/163 +x64 : _nat -> [0..3]; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation % LOCAL,STATE(1,)/164 +x65 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates % LOCAL,STATE(1,)/165 +x66 : _nat -> BOOLEAN; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_FarApproachComplete % LOCAL/166 +x68 : _nat -> BOOLEAN; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_AttemptingToDock % LOCAL/168 +x71 : _nat -> BOOLEAN; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_ProximityOperationsComplete % LOCAL/171 +x73 : _nat -> BOOLEAN; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_DockingApproachComplete % LOCAL/173 +x74 : _nat -> BOOLEAN; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_ApproachOrbitComplete % LOCAL/174 +x76 : _nat -> BOOLEAN; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_CaptureApproachComplete % LOCAL/176 +x77 : _nat -> INT; + % Chart_main_simp_rlt_node_state364_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteVelocity % LOCAL,STATE(1,)/177 +x78 : _nat -> INT; + % Chart_main_simp_rlt_node_state364_rlt_chart_data_vars_Chart_InertialNavigation_AbsolutePosition % LOCAL,STATE(1,)/178 +x79 : _nat -> INT; + % Chart_main_simp_rlt_node_state364_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteAttitude % LOCAL,STATE(1,)/179 +x80 : _nat -> INT; + % Chart_main_simp_rlt_node_state364_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation % LOCAL,STATE(1,)/180 +x81 : _nat -> INT; + % Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_GPS % LOCAL,STATE(1,)/181 +x82 : _nat -> INT; + % Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState2 % LOCAL,STATE(1,)/182 +x83 : _nat -> INT; + % Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState % LOCAL,STATE(1,)/183 +x84 : _nat -> INT; + % Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_StarPlanetTracker % LOCAL,STATE(1,)/184 +x85 : _nat -> INT; + % Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation % LOCAL/185 +x86 : _nat -> INT; + % Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates % LOCAL,STATE(1,)/186 +x87 : _nat -> INT; + % Chart_main_simp_rlt_node_state104_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation % LOCAL/187 +x88 : _nat -> INT; + % Chart_main_simp_rlt_node_state100_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_StarPlanetTracker % LOCAL/188 +x89 : _nat -> INT; + % Chart_main_simp_rlt_node_state98_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_StarPlanetTracker % LOCAL/189 +x90 : _nat -> INT; + % Chart_main_simp_rlt_node_state96_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_StarPlanetTracker % LOCAL/190 +x91 : _nat -> INT; + % Chart_main_simp_rlt_node_state82_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState % LOCAL/191 +x92 : _nat -> INT; + % Chart_main_simp_rlt_node_state78_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState % LOCAL/192 +x93 : _nat -> INT; + % Chart_main_simp_rlt_node_state148_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation % LOCAL/193 +x94 : _nat -> INT; + % Chart_main_simp_rlt_node_state144_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation % LOCAL/194 +x95 : _nat -> INT; + % Chart_main_simp_rlt_node_state136_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_GPS % LOCAL/195 +x96 : _nat -> INT; + % Chart_main_simp_rlt_node_state134_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_GPS % LOCAL/196 +x97 : _nat -> INT; + % Chart_main_simp_rlt_node_state132_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_GPS % LOCAL/197 +x98 : _nat -> INT; + % Chart_main_simp_rlt_node_state130_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState2 % LOCAL/198 +x99 : _nat -> INT; + % Chart_main_simp_rlt_node_state128_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState2 % LOCAL/199 + + +% Generic definitions +DEF__174 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x74(_M)) = (IF (_M = _base) THEN FALSE ELSE (x20((_M - 1))) ENDIF)); +DEF__176 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x76(_M)) = (IF (_M = _base) THEN FALSE ELSE (x15((_M - 1))) ENDIF)); +DEF__177 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x77(_M)) = (IF ((x83(_M)) = 1) THEN (x42(_M)) ELSE (IF ((x83(_M)) = 2) THEN (x42(_M)) ELSE (IF ((x83(_M)) = 3) THEN (x103(_M)) ELSE (IF ((x83(_M)) = 4) THEN (IF ((NOT ((((((((x2(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x2(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x2(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52(_M)) = 2) OR ((x53(_M)) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x3(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x3(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (x42(_M)) ELSE (x103(_M)) ENDIF) ELSE (x103(_M)) ENDIF) ELSE (x103(_M)) ENDIF) ELSE (x42(_M)) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__178 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x78(_M)) = (IF ((x83(_M)) = 1) THEN (x43(_M)) ELSE (IF ((x83(_M)) = 2) THEN (x43(_M)) ELSE (IF ((x83(_M)) = 3) THEN (x104(_M)) ELSE (IF ((x83(_M)) = 4) THEN (IF ((NOT ((((((((x2(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x2(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x2(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52(_M)) = 2) OR ((x53(_M)) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x3(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x3(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (x43(_M)) ELSE (x104(_M)) ENDIF) ELSE (x104(_M)) ENDIF) ELSE (x104(_M)) ENDIF) ELSE (x43(_M)) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__179 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x79(_M)) = (IF ((x83(_M)) = 1) THEN (x52(_M)) ELSE (IF ((x83(_M)) = 2) THEN (x52(_M)) ELSE (IF ((x83(_M)) = 3) THEN (x108(_M)) ELSE (IF ((x83(_M)) = 4) THEN (IF ((NOT ((((((((x2(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x2(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x2(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52(_M)) = 2) OR ((x53(_M)) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x3(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x3(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (x52(_M)) ELSE (x108(_M)) ENDIF) ELSE (x108(_M)) ENDIF) ELSE (x108(_M)) ENDIF) ELSE (x52(_M)) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__180 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x80(_M)) = (IF ((x83(_M)) = 1) THEN (x85(_M)) ELSE (IF ((x83(_M)) = 2) THEN (x85(_M)) ELSE (IF ((x83(_M)) = 3) THEN (x110(_M)) ELSE (IF ((x83(_M)) = 4) THEN (IF ((NOT ((((((((x2(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x2(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x2(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52(_M)) = 2) OR ((x53(_M)) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x3(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x3(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (x85(_M)) ELSE (x110(_M)) ENDIF) ELSE (x110(_M)) ENDIF) ELSE (x110(_M)) ENDIF) ELSE (x85(_M)) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__181 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x81(_M)) = (IF ((x63(_M)) = 1) THEN (x58(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x58(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x58(_M)) ELSE (IF ((x63(_M)) = 4) THEN (x95(_M)) ELSE (IF ((x63(_M)) = 5) THEN (x95(_M)) ELSE (x58(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__182 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x82(_M)) = (IF ((x63(_M)) = 1) THEN (x60(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x60(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x60(_M)) ELSE (IF ((x63(_M)) = 4) THEN (x98(_M)) ELSE (IF ((x63(_M)) = 5) THEN (x98(_M)) ELSE (x60(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__183 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x83(_M)) = (IF ((x63(_M)) = 1) THEN (x61(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x61(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x61(_M)) ELSE (IF ((x63(_M)) = 4) THEN (x100(_M)) ELSE (IF ((x63(_M)) = 5) THEN (x100(_M)) ELSE (x61(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__184 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x84(_M)) = (IF ((x63(_M)) = 1) THEN (x62(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x62(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x62(_M)) ELSE (IF ((x63(_M)) = 4) THEN (x88(_M)) ELSE (IF ((x63(_M)) = 5) THEN (x88(_M)) ELSE (x62(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__185 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x85(_M)) = (IF ((x63(_M)) = 1) THEN (x64(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x64(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x64(_M)) ELSE (IF ((x63(_M)) = 4) THEN (x93(_M)) ELSE (IF ((x63(_M)) = 5) THEN (x93(_M)) ELSE (x64(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__186 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x86(_M)) = (IF ((x63(_M)) = 1) THEN (x65(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x65(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x65(_M)) ELSE (IF ((x63(_M)) = 4) THEN 10 ELSE (IF ((x63(_M)) = 5) THEN 2 ELSE (x65(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__187 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x87(_M)) = (IF ((x94(_M)) = 2) THEN 0 ELSE (x94(_M)) ENDIF)); +DEF__188 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x88(_M)) = (IF ((x89(_M)) = 3) THEN 0 ELSE (x89(_M)) ENDIF)); +DEF__189 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x89(_M)) = (IF ((x90(_M)) = 2) THEN 0 ELSE (x90(_M)) ENDIF)); +DEF__190 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x90(_M)) = (IF ((x62(_M)) = 1) THEN 0 ELSE (x62(_M)) ENDIF)); +DEF__191 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x91(_M)) = (IF ((x101(_M)) = 3) THEN 0 ELSE (x101(_M)) ENDIF)); +DEF__192 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x92(_M)) = (IF ((x61(_M)) = 1) THEN 0 ELSE (x61(_M)) ENDIF)); +DEF__193 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x93(_M)) = (IF ((x87(_M)) = 3) THEN 0 ELSE (x87(_M)) ENDIF)); +DEF__194 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x94(_M)) = (IF ((x64(_M)) = 1) THEN 0 ELSE (x64(_M)) ENDIF)); +DEF__195 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x95(_M)) = (IF ((x96(_M)) = 3) THEN 0 ELSE (x96(_M)) ENDIF)); +DEF__196 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x96(_M)) = (IF ((x97(_M)) = 2) THEN 0 ELSE (x97(_M)) ENDIF)); +DEF__197 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x97(_M)) = (IF ((x58(_M)) = 1) THEN 0 ELSE (x58(_M)) ENDIF)); +DEF__198 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x98(_M)) = (IF ((x99(_M)) = 2) THEN 0 ELSE (x99(_M)) ENDIF)); +DEF__199 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x99(_M)) = (IF ((x60(_M)) = 1) THEN 0 ELSE (x60(_M)) ENDIF)); +DEF__200 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x100(_M)) = (IF ((x91(_M)) = 4) THEN 0 ELSE (x91(_M)) ENDIF)); +DEF__201 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x101(_M)) = (IF ((x92(_M)) = 2) THEN 0 ELSE (x92(_M)) ENDIF)); +DEF__202 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x102(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN 2 ELSE (x39(_M)) ENDIF)); +DEF__115 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x15(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 2) THEN ((NOT ((x14(_M)) = 8)) AND ((NOT ((x14(_M)) = 6)) AND (x76(_M)))) ELSE (IF ((x65(_M)) = 3) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 4) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 5) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 6) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 7) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 8) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 9) THEN (IF ((x63(_M)) = 1) THEN (x76(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x76(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x76(_M)) ELSE (((x63(_M)) = 4) OR (x76(_M))) ENDIF) ENDIF) ENDIF) ELSE (x76(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x76(_M)) ENDIF)); +DEF__203 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x103(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN (IF ((x86(_M)) = 9) THEN (IF ((x85(_M)) = 1) THEN 2 ELSE (IF ((x85(_M)) = 2) THEN (IF ((x30(_M)) = 6) THEN 1 ELSE (IF ((x30(_M)) < 6) THEN 2 ELSE (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x42(_M)) ENDIF) ENDIF) ENDIF) ELSE (IF ((x85(_M)) = 3) THEN 2 ELSE (x42(_M)) ENDIF) ENDIF) ENDIF) ELSE (x42(_M)) ENDIF) ELSE (x42(_M)) ENDIF)); +DEF__116 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x16(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 2) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 3) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 4) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 5) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 6) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 7) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 8) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 9) THEN (IF ((x63(_M)) = 1) THEN (x73(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x73(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x73(_M)) ELSE ((NOT ((x63(_M)) = 4)) AND (x73(_M))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65(_M)) = 10) THEN (IF ((x55(_M)) = 1) THEN (x73(_M)) ELSE (IF ((x55(_M)) = 2) THEN (x73(_M)) ELSE (((x55(_M)) = 3) OR (x73(_M))) ENDIF) ENDIF) ELSE (IF ((x65(_M)) = 11) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 12) THEN (IF ((x57(_M)) = 1) THEN (x73(_M)) ELSE (IF ((x57(_M)) = 2) THEN (x73(_M)) ELSE ((NOT ((x57(_M)) = 3)) AND (x73(_M))) ENDIF) ENDIF) ELSE (x73(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x73(_M)) ENDIF)); +DEF__204 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x104(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN (IF ((x86(_M)) = 9) THEN (IF ((x85(_M)) = 1) THEN 2 ELSE (IF ((x85(_M)) = 2) THEN (IF ((x30(_M)) = 6) THEN 1 ELSE (IF ((x30(_M)) < 6) THEN 2 ELSE (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x43(_M)) ENDIF) ENDIF) ENDIF) ELSE (IF ((x85(_M)) = 3) THEN 2 ELSE (x43(_M)) ENDIF) ENDIF) ENDIF) ELSE (x43(_M)) ENDIF) ELSE (x43(_M)) ENDIF)); +DEF__117 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x17(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 2) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 3) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 4) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 5) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 6) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 7) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 8) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 9) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 10) THEN (IF ((x55(_M)) = 1) THEN (x68(_M)) ELSE (IF ((x55(_M)) = 2) THEN (x68(_M)) ELSE (((x55(_M)) = 3) OR (x68(_M))) ENDIF) ENDIF) ELSE (IF ((x65(_M)) = 11) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 12) THEN (IF ((x57(_M)) = 1) THEN (x68(_M)) ELSE (IF ((x57(_M)) = 2) THEN (x68(_M)) ELSE ((NOT ((x57(_M)) = 3)) AND ((NOT ((x57(_M)) = 4)) AND (x68(_M)))) ENDIF) ENDIF) ELSE (x68(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x68(_M)) ENDIF)); +DEF__205 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x105(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN (IF ((x86(_M)) = 9) THEN (IF ((x85(_M)) = 1) THEN 0 ELSE (IF ((x85(_M)) = 2) THEN (IF ((x30(_M)) = 6) THEN (x30(_M)) ELSE (IF ((x30(_M)) < 6) THEN 0 ELSE (x30(_M)) ENDIF) ENDIF) ELSE (IF ((x85(_M)) = 3) THEN 0 ELSE (x30(_M)) ENDIF) ENDIF) ENDIF) ELSE (x44(_M)) ENDIF) ELSE (x44(_M)) ENDIF)); +DEF__206 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x106(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN 2 ELSE (x47(_M)) ENDIF)); +DEF__207 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x107(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN 2 ELSE (x48(_M)) ENDIF)); +DEF__120 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x20(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x74(_M)) ELSE (IF ((x65(_M)) = 2) THEN ((NOT ((x14(_M)) = 8)) AND ((NOT ((x14(_M)) = 6)) AND (x74(_M)))) ELSE (IF ((x65(_M)) = 3) THEN (((x14(_M)) = 2) OR (x74(_M))) ELSE (IF ((x65(_M)) = 4) THEN ((NOT ((x14(_M)) = 1)) AND (x74(_M))) ELSE (x74(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x74(_M)) ENDIF)); +DEF__208 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x108(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN (IF ((x86(_M)) = 9) THEN (IF ((x85(_M)) = 1) THEN 2 ELSE (IF ((x85(_M)) = 2) THEN (IF ((x30(_M)) = 6) THEN 1 ELSE (IF ((x30(_M)) < 6) THEN 2 ELSE (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x52(_M)) ENDIF) ENDIF) ENDIF) ELSE (IF ((x85(_M)) = 3) THEN 2 ELSE (x52(_M)) ENDIF) ENDIF) ENDIF) ELSE (x52(_M)) ENDIF) ELSE (x52(_M)) ENDIF)); +DEF__121 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x21(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x66(_M)) ELSE (IF ((x65(_M)) = 2) THEN ((NOT ((x14(_M)) = 8)) AND ((NOT ((x14(_M)) = 6)) AND (x66(_M)))) ELSE (IF ((x65(_M)) = 3) THEN (x66(_M)) ELSE (IF ((x65(_M)) = 4) THEN (x66(_M)) ELSE (IF ((x65(_M)) = 5) THEN (x66(_M)) ELSE (IF ((x65(_M)) = 6) THEN (IF ((x14(_M)) = 5) THEN (x66(_M)) ELSE (((x14(_M)) = 4) OR (x66(_M))) ENDIF) ELSE (x66(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x66(_M)) ENDIF)); +DEF__209 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x109(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN 4 ELSE (x83(_M)) ENDIF)); +DEF__122 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x22(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x71(_M)) ELSE (IF ((x65(_M)) = 2) THEN ((NOT ((x14(_M)) = 8)) AND ((NOT ((x14(_M)) = 6)) AND (x71(_M)))) ELSE (IF ((x65(_M)) = 3) THEN (x71(_M)) ELSE (IF ((x65(_M)) = 4) THEN (IF ((x14(_M)) = 1) THEN (x71(_M)) ELSE (((x14(_M)) = 3) OR (x71(_M))) ENDIF) ELSE (x71(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x71(_M)) ENDIF)); +DEF__210 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x110(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN (IF ((x86(_M)) = 9) THEN (IF ((x85(_M)) = 1) THEN 2 ELSE (IF ((x85(_M)) = 2) THEN (IF ((x30(_M)) = 6) THEN 3 ELSE (IF ((x30(_M)) < 6) THEN 2 ELSE (IF ((x11(_M)) <=> TRUE) THEN 1 ELSE (x85(_M)) ENDIF) ENDIF) ENDIF) ELSE (IF ((x85(_M)) = 3) THEN 2 ELSE (x85(_M)) ENDIF) ENDIF) ENDIF) ELSE (x85(_M)) ENDIF) ELSE (x85(_M)) ENDIF)); +DEF__211 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x111(_M)) = (IF (((((x12(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) <=> TRUE) THEN 2 ELSE (x36(_M)) ENDIF)); +DEF__212 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x112(_M)) = (IF (((((x12(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) <=> TRUE) THEN 2 ELSE (x82(_M)) ENDIF)); +DEF__126 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x26(_M)) = (IF (((x37(_M)) + 1) < 9) THEN ((x37(_M)) + 1) ELSE 9 ENDIF)); +DEF__213 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x113(_M)) = (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x77(_M)) ENDIF)); +DEF__127 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x27(_M)) = (IF (((x51(_M)) + 1) < 9) THEN ((x51(_M)) + 1) ELSE 9 ENDIF)); +DEF__214 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x114(_M)) = (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x78(_M)) ENDIF)); +DEF__128 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x28(_M)) = ((IF ((x55(_M)) = 1) THEN (x46(_M)) ELSE (IF ((x55(_M)) = 2) THEN (x46(_M)) ELSE (IF ((x55(_M)) = 3) THEN (x118(_M)) ELSE (IF ((x55(_M)) = 4) THEN (x118(_M)) ELSE (x46(_M)) ENDIF) ENDIF) ENDIF) ENDIF) + 1)); +DEF__215 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x115(_M)) = (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x79(_M)) ENDIF)); +DEF__216 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x116(_M)) = (IF ((x11(_M)) <=> TRUE) THEN 1 ELSE (x80(_M)) ENDIF)); +DEF__129 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x29(_M)) = (IF ((x28(_M)) < 6) THEN (x28(_M)) ELSE 6 ENDIF)); +DEF__217 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x117(_M)) = (IF ((x55(_M)) = 1) THEN (x54(_M)) ELSE (IF ((x55(_M)) = 2) THEN (x54(_M)) ELSE (IF ((x55(_M)) = 3) THEN (x119(_M)) ELSE (IF ((x55(_M)) = 4) THEN (x119(_M)) ELSE (x54(_M)) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__130 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x30(_M)) = (IF (((x44(_M)) + 1) < 6) THEN ((x44(_M)) + 1) ELSE 6 ENDIF)); +DEF__131 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x31(_M)) = (IF (((x40(_M)) + 1) < 11) THEN ((x40(_M)) + 1) ELSE 11 ENDIF)); +DEF__218 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x118(_M)) = (IF ((x120(_M)) = 3) THEN 0 ELSE (IF ((x54(_M)) = 1) THEN 0 ELSE (x46(_M)) ENDIF) ENDIF)); +DEF__132 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x32(_M)) = (IF (((x41(_M)) + 1) < 6) THEN ((x41(_M)) + 1) ELSE 6 ENDIF)); +DEF__219 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x119(_M)) = (IF ((x120(_M)) = 3) THEN 0 ELSE (x120(_M)) ENDIF)); +DEF__133 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x33(_M)) = (IF (((x38(_M)) + 1) < 6) THEN ((x38(_M)) + 1) ELSE 6 ENDIF)); +DEF__220 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x120(_M)) = (IF ((x121(_M)) = 2) THEN 0 ELSE (x121(_M)) ENDIF)); +DEF__134 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x34(_M)) = ((IF ((x83(_M)) = 1) THEN (x44(_M)) ELSE (IF ((x83(_M)) = 2) THEN (x44(_M)) ELSE (IF ((x83(_M)) = 3) THEN (x105(_M)) ELSE (IF ((x83(_M)) = 4) THEN (IF ((NOT ((((((((x2(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x2(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x2(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52(_M)) = 2) OR ((x53(_M)) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x3(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x3(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (x44(_M)) ELSE (x105(_M)) ENDIF) ELSE (x105(_M)) ENDIF) ELSE (x105(_M)) ENDIF) ELSE (x44(_M)) ENDIF) ENDIF) ENDIF) ENDIF) + 1)); +DEF__221 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x121(_M)) = (IF ((x54(_M)) = 1) THEN 0 ELSE (x54(_M)) ENDIF)); +DEF__222 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x122(_M)) = (IF ((x57(_M)) = 1) THEN (x56(_M)) ELSE (IF ((x57(_M)) = 2) THEN (x56(_M)) ELSE (IF ((x57(_M)) = 3) THEN (x126(_M)) ELSE (IF ((x57(_M)) = 4) THEN (x126(_M)) ELSE (x56(_M)) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__135 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x35(_M)) = (IF ((x34(_M)) < 6) THEN (x34(_M)) ELSE 6 ENDIF)); +DEF__223 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x123(_M)) = (IF ((x26(_M)) = 8) THEN 3 ELSE (x57(_M)) ENDIF)); +DEF__136 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x36(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x36((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x36((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x82((_M - 1))) = 1) THEN (x111((_M - 1))) ELSE (IF ((x82((_M - 1))) = 2) THEN (IF ((NOT ((x13((_M - 1))) = 2)) <=> TRUE) THEN 1 ELSE (x111((_M - 1))) ENDIF) ELSE (x36((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x36((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x36((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x36((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x36((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x36((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x36((_M - 1))) ENDIF) ENDIF)); +DEF__224 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x124(_M)) = (IF ((x128(_M)) = 3) THEN 0 ELSE (x128(_M)) ENDIF)); +DEF__137 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x37(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x37((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x37((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN 0 ELSE (x37((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (x26((_M - 1))) ELSE (x37((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x37((_M - 1))) ENDIF) ENDIF)); +DEF__225 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x125(_M)) = (IF ((x56(_M)) = 1) THEN 0 ELSE (x56(_M)) ENDIF)); +DEF__138 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x38(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x84((_M - 1))) = 1) THEN (IF (((NOT (((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0))) AND (x5((_M - 1)))) <=> TRUE) THEN 0 ELSE (x33((_M - 1))) ENDIF) ELSE (IF ((x84((_M - 1))) = 2) THEN (IF ((((x33((_M - 1))) = 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) <=> TRUE) THEN (x33((_M - 1))) ELSE (IF (((((((x33((_M - 1))) = 6) AND ((x9((_M - 1))) = 2)) AND ((x10((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN (x33((_M - 1))) ELSE (IF (((((x33((_M - 1))) < 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) OR ((x5((_M - 1))) AND (((x6((_M - 1))) OR ((x9((_M - 1))) = 1)) OR ((x10((_M - 1))) = 1)))) <=> TRUE) THEN 0 ELSE (x33((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x84((_M - 1))) = 3) THEN (IF (((((NOT ((x9((_M - 1))) = 2)) AND (NOT ((x10((_M - 1))) = 2))) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 0 ELSE (x33((_M - 1))) ENDIF) ELSE (x33((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x38((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x38((_M - 1))) ENDIF) ENDIF)); +DEF__226 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x126(_M)) = (IF ((x127(_M)) = 5) THEN 0 ELSE (x127(_M)) ENDIF)); +DEF__139 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x39(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x39((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x39((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x83((_M - 1))) = 1) THEN (IF (((NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0))) AND (NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)))) <=> TRUE) THEN 0 ELSE (IF ((((((((x50((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)) <=> TRUE) THEN 0 ELSE (x39((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 2) THEN (IF ((((((x2((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((((x3((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0))) <=> TRUE) THEN 0 ELSE (IF (((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF (((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2)) <=> TRUE) THEN 1 ELSE (x39((_M - 1))) ENDIF) ELSE (x39((_M - 1))) ENDIF) ELSE (x39((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 3) THEN (x102((_M - 1))) ELSE (IF ((x83((_M - 1))) = 4) THEN (IF ((NOT ((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN 0 ELSE (x102((_M - 1))) ENDIF) ELSE (x102((_M - 1))) ENDIF) ELSE (x102((_M - 1))) ENDIF) ELSE (x39((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x39((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x39((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x39((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x39((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x39((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x39((_M - 1))) ENDIF) ENDIF)); +DEF__227 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x127(_M)) = (IF ((x124(_M)) = 4) THEN 0 ELSE (x124(_M)) ENDIF)); +DEF__140 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x40(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x40((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x40((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x31((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x40((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x40((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x40((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x40((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x40((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x40((_M - 1))) ENDIF) ENDIF)); +DEF__228 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x128(_M)) = (IF ((x125(_M)) = 2) THEN 0 ELSE (x125(_M)) ENDIF)); +DEF__141 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x41(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x81((_M - 1))) = 1) THEN (IF (((NOT ((x7((_M - 1))) = 0)) AND (x8((_M - 1)))) <=> TRUE) THEN 0 ELSE (x32((_M - 1))) ENDIF) ELSE (IF ((x81((_M - 1))) = 2) THEN (IF ((((x32((_M - 1))) = 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) <=> TRUE) THEN (x32((_M - 1))) ELSE (IF ((((((x32((_M - 1))) = 6) AND ((x7((_M - 1))) = 2)) AND (x8((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN (x32((_M - 1))) ELSE (IF (((((x32((_M - 1))) < 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) OR ((x8((_M - 1))) AND (((x7((_M - 1))) = 1) OR (x6((_M - 1)))))) <=> TRUE) THEN 0 ELSE (x32((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x81((_M - 1))) = 3) THEN (IF (((NOT (((x7((_M - 1))) = 2) AND (x8((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 0 ELSE (x32((_M - 1))) ENDIF) ELSE (x32((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x41((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x41((_M - 1))) ENDIF) ENDIF)); +DEF__229 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x129(_M)) = ((NOT (x17(_M))) OR (((((x20(_M)) AND (x22(_M))) AND (x21(_M))) AND (x15(_M))) AND (x16(_M))))); +DEF__142 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x42(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x42((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x42((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x80((_M - 1))) = 1) THEN (x77((_M - 1))) ELSE (IF ((x80((_M - 1))) = 2) THEN (IF ((x35((_M - 1))) = 6) THEN 1 ELSE (IF ((x35((_M - 1))) < 6) THEN 2 ELSE (x113((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x80((_M - 1))) = 3) THEN (x113((_M - 1))) ELSE (x77((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x42((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x42((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x42((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x42((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x42((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x42((_M - 1))) ENDIF) ENDIF)); +DEF__143 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x43(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x43((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x43((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x80((_M - 1))) = 1) THEN (x78((_M - 1))) ELSE (IF ((x80((_M - 1))) = 2) THEN (IF ((x35((_M - 1))) = 6) THEN 1 ELSE (IF ((x35((_M - 1))) < 6) THEN 2 ELSE (x114((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x80((_M - 1))) = 3) THEN (x114((_M - 1))) ELSE (x78((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x43((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x43((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x43((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x43((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x43((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x43((_M - 1))) ENDIF) ENDIF)); +DEF__144 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x44(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x80((_M - 1))) = 1) THEN (x35((_M - 1))) ELSE (IF ((x80((_M - 1))) = 2) THEN (IF ((x35((_M - 1))) = 6) THEN (x35((_M - 1))) ELSE (IF ((x35((_M - 1))) < 6) THEN 0 ELSE (x35((_M - 1))) ENDIF) ENDIF) ELSE (x35((_M - 1))) ENDIF) ENDIF) ELSE (x44((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x44((_M - 1))) ENDIF) ENDIF)); +DEF__145 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x45(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x45((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x45((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN 0 ELSE (x45((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x122((_M - 1))) = 1) THEN 1 ELSE (IF ((x122((_M - 1))) = 2) THEN 0 ELSE (IF ((x122((_M - 1))) = 3) THEN 3 ELSE (IF ((x122((_M - 1))) = 4) THEN 0 ELSE (IF ((x122((_M - 1))) = 5) THEN 0 ELSE (x45((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x45((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x45((_M - 1))) ENDIF) ENDIF)); +DEF__146 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x46(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x117((_M - 1))) = 1) THEN (IF (((NOT ((x4((_M - 1))) = 0)) AND (x5((_M - 1)))) <=> TRUE) THEN 0 ELSE (IF ((((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1))))) <=> TRUE) THEN 0 ELSE (x29((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x117((_M - 1))) = 2) THEN (x29((_M - 1))) ELSE (IF ((x117((_M - 1))) = 3) THEN (IF ((((NOT ((x4((_M - 1))) = 2)) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 0 ELSE (IF (((((x4((_M - 1))) = 2) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 0 ELSE (x29((_M - 1))) ENDIF) ENDIF) ELSE (x29((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x46((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x46((_M - 1))) ENDIF) ENDIF)); +DEF__147 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x47(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x47((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x47((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x83((_M - 1))) = 1) THEN (IF (((NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0))) AND (NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)))) <=> TRUE) THEN 1 ELSE (IF ((((((((x50((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)) <=> TRUE) THEN 0 ELSE (x47((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 2) THEN (IF ((((((x2((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((((x3((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0))) <=> TRUE) THEN 0 ELSE (IF (((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF (((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2)) <=> TRUE) THEN 2 ELSE (x47((_M - 1))) ENDIF) ELSE (x47((_M - 1))) ENDIF) ELSE (x47((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 3) THEN (x106((_M - 1))) ELSE (IF ((x83((_M - 1))) = 4) THEN (IF ((NOT ((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN 1 ELSE (x106((_M - 1))) ENDIF) ELSE (x106((_M - 1))) ENDIF) ELSE (x106((_M - 1))) ENDIF) ELSE (x47((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x47((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x47((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x47((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x47((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x47((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x47((_M - 1))) ENDIF) ENDIF)); +DEF__148 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x48(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x48((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x48((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x83((_M - 1))) = 1) THEN (IF (((NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0))) AND (NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)))) <=> TRUE) THEN 1 ELSE (IF ((((((((x50((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)) <=> TRUE) THEN 0 ELSE (x48((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 2) THEN (IF ((((((x2((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((((x3((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0))) <=> TRUE) THEN 0 ELSE (IF (((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF (((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2)) <=> TRUE) THEN 2 ELSE (x48((_M - 1))) ENDIF) ELSE (x48((_M - 1))) ENDIF) ELSE (x48((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 3) THEN (x107((_M - 1))) ELSE (IF ((x83((_M - 1))) = 4) THEN (IF ((NOT ((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN 1 ELSE (x107((_M - 1))) ENDIF) ELSE (x107((_M - 1))) ENDIF) ELSE (x107((_M - 1))) ENDIF) ELSE (x48((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x48((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x48((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x48((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x48((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x48((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x48((_M - 1))) ENDIF) ENDIF)); +DEF__149 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x49(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x63((_M - 1))) = 1) THEN (x49((_M - 1))) ELSE (IF ((x63((_M - 1))) = 2) THEN (x49((_M - 1))) ELSE (IF ((x63((_M - 1))) = 3) THEN (x49((_M - 1))) ELSE (IF ((x63((_M - 1))) = 4) THEN 0 ELSE (x49((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x117((_M - 1))) = 1) THEN (IF (((NOT ((x4((_M - 1))) = 0)) AND (x5((_M - 1)))) <=> TRUE) THEN 1 ELSE (IF ((((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1))))) <=> TRUE) THEN 0 ELSE (x49((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x117((_M - 1))) = 2) THEN (IF ((((x29((_M - 1))) = 6) AND (((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1)))))) <=> TRUE) THEN 0 ELSE (IF ((((((x29((_M - 1))) < 6) AND ((x4((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 2 ELSE (IF (((((x29((_M - 1))) < 6) AND (((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1)))))) OR ((x5((_M - 1))) AND (((x4((_M - 1))) = 1) OR (x6((_M - 1)))))) <=> TRUE) THEN 1 ELSE (x49((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x117((_M - 1))) = 3) THEN (IF ((((NOT ((x4((_M - 1))) = 2)) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 1 ELSE (IF (((((x4((_M - 1))) = 2) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 2 ELSE (x49((_M - 1))) ENDIF) ENDIF) ELSE (x49((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (x49((_M - 1))) ELSE (IF ((x57((_M - 1))) = 2) THEN (x49((_M - 1))) ELSE (IF ((x57((_M - 1))) = 3) THEN 0 ELSE (x49((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x49((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x49((_M - 1))) ENDIF) ENDIF)); +DEF__150 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x50(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x50((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x50((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x81((_M - 1))) = 1) THEN (IF (((NOT ((x7((_M - 1))) = 0)) AND (x8((_M - 1)))) <=> TRUE) THEN 1 ELSE (IF ((((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1))))) <=> TRUE) THEN 0 ELSE (x50((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x81((_M - 1))) = 2) THEN (IF ((((x32((_M - 1))) = 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) <=> TRUE) THEN 0 ELSE (IF ((((((x32((_M - 1))) = 6) AND ((x7((_M - 1))) = 2)) AND (x8((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 2 ELSE (IF (((((x32((_M - 1))) < 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) OR ((x8((_M - 1))) AND (((x7((_M - 1))) = 1) OR (x6((_M - 1)))))) <=> TRUE) THEN 1 ELSE (x50((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x81((_M - 1))) = 3) THEN (IF (((NOT (((x7((_M - 1))) = 2) AND (x8((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 1 ELSE 2 ENDIF) ELSE (x50((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x50((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x50((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x50((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x50((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x50((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x50((_M - 1))) ENDIF) ENDIF)); +DEF__151 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x51(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x63((_M - 1))) = 1) THEN (x51((_M - 1))) ELSE (IF ((x63((_M - 1))) = 2) THEN (x51((_M - 1))) ELSE (IF ((x63((_M - 1))) = 3) THEN (x51((_M - 1))) ELSE (IF ((x63((_M - 1))) = 4) THEN 0 ELSE (x51((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (x27((_M - 1))) ELSE (IF ((x65((_M - 1))) = 11) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (x51((_M - 1))) ELSE (IF ((x57((_M - 1))) = 2) THEN (x51((_M - 1))) ELSE (IF ((x57((_M - 1))) = 3) THEN 0 ELSE (x51((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x51((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x51((_M - 1))) ENDIF) ENDIF)); +DEF__152 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x52(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x52((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x52((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x80((_M - 1))) = 1) THEN (x79((_M - 1))) ELSE (IF ((x80((_M - 1))) = 2) THEN (IF ((x35((_M - 1))) = 6) THEN 1 ELSE (IF ((x35((_M - 1))) < 6) THEN 2 ELSE (x115((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x80((_M - 1))) = 3) THEN (x115((_M - 1))) ELSE (x79((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x52((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x52((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x52((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x52((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x52((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x52((_M - 1))) ENDIF) ENDIF)); +DEF__153 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x53(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x53((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x53((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x84((_M - 1))) = 1) THEN (IF (((NOT (((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0))) AND (x5((_M - 1)))) <=> TRUE) THEN 1 ELSE 0 ENDIF) ELSE (IF ((x84((_M - 1))) = 2) THEN (IF ((((x33((_M - 1))) = 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) <=> TRUE) THEN 0 ELSE (IF (((((((x33((_M - 1))) = 6) AND ((x9((_M - 1))) = 2)) AND ((x10((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 2 ELSE (IF (((((x33((_M - 1))) < 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) OR ((x5((_M - 1))) AND (((x6((_M - 1))) OR ((x9((_M - 1))) = 1)) OR ((x10((_M - 1))) = 1)))) <=> TRUE) THEN 1 ELSE (x53((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x84((_M - 1))) = 3) THEN (IF (((((NOT ((x9((_M - 1))) = 2)) AND (NOT ((x10((_M - 1))) = 2))) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 1 ELSE (IF ((((((x9((_M - 1))) = 2) AND ((x10((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 2 ELSE (x53((_M - 1))) ENDIF) ENDIF) ELSE (x53((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x53((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x53((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x53((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x53((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x53((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x53((_M - 1))) ENDIF) ENDIF)); +DEF__154 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x54(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x63((_M - 1))) = 1) THEN (x54((_M - 1))) ELSE (IF ((x63((_M - 1))) = 2) THEN (x54((_M - 1))) ELSE (IF ((x63((_M - 1))) = 3) THEN (x54((_M - 1))) ELSE (IF ((x63((_M - 1))) = 4) THEN 1 ELSE (x54((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x117((_M - 1))) = 1) THEN (IF (((NOT ((x4((_M - 1))) = 0)) AND (x5((_M - 1)))) <=> TRUE) THEN 2 ELSE (IF ((((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1))))) <=> TRUE) THEN 1 ELSE (x117((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x117((_M - 1))) = 2) THEN (IF ((((x29((_M - 1))) = 6) AND (((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1)))))) <=> TRUE) THEN 1 ELSE (IF ((((((x29((_M - 1))) < 6) AND ((x4((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 3 ELSE (IF (((((x29((_M - 1))) < 6) AND (((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1)))))) OR ((x5((_M - 1))) AND (((x4((_M - 1))) = 1) OR (x6((_M - 1)))))) <=> TRUE) THEN 2 ELSE (x117((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x117((_M - 1))) = 3) THEN (IF ((((NOT ((x4((_M - 1))) = 2)) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 2 ELSE (IF (((((x4((_M - 1))) = 2) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 3 ELSE (x117((_M - 1))) ENDIF) ENDIF) ELSE (x117((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (x54((_M - 1))) ELSE (IF ((x57((_M - 1))) = 2) THEN (x54((_M - 1))) ELSE (IF ((x57((_M - 1))) = 3) THEN 1 ELSE (x54((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x54((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x54((_M - 1))) ENDIF) ENDIF)); +DEF__155 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x55(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x63((_M - 1))) = 1) THEN (x55((_M - 1))) ELSE (IF ((x63((_M - 1))) = 2) THEN (x55((_M - 1))) ELSE (IF ((x63((_M - 1))) = 3) THEN (x55((_M - 1))) ELSE (IF ((x63((_M - 1))) = 4) THEN 1 ELSE (x55((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (IF (((((NOT ((x49((_M - 1))) = 0)) AND (NOT ((x49((_M - 1))) = 0))) AND (NOT ((x49((_M - 1))) = 0))) AND ((x27((_M - 1))) < 9)) <=> TRUE) THEN 2 ELSE (IF ((x27((_M - 1))) = 9) THEN 4 ELSE (x55((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x55((_M - 1))) = 2) THEN (IF (((((x49((_M - 1))) = 2) AND (((x49((_M - 1))) = 2) AND ((x49((_M - 1))) = 2))) AND ((x49((_M - 1))) = 2)) <=> TRUE) THEN 3 ELSE (IF ((((((x49((_M - 1))) = 1) AND ((x49((_M - 1))) = 1)) AND ((x49((_M - 1))) = 1)) AND ((x49((_M - 1))) = 1)) <=> TRUE) THEN 5 ELSE (IF ((x27((_M - 1))) = 9) THEN 4 ELSE (IF (((((x49((_M - 1))) = 0) OR ((x49((_M - 1))) = 0)) OR ((x49((_M - 1))) = 0)) <=> TRUE) THEN 4 ELSE (IF ((NOT ((x49((_M - 1))) = 2)) <=> TRUE) THEN 4 ELSE (x55((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x55((_M - 1))) = 3) THEN 0 ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (IF ((x55((_M - 1))) = 5) THEN 4 ELSE (x55((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (x55((_M - 1))) ELSE (IF ((x57((_M - 1))) = 2) THEN (x55((_M - 1))) ELSE (IF ((x57((_M - 1))) = 3) THEN 1 ELSE (x55((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x55((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x55((_M - 1))) ENDIF) ENDIF)); +DEF__156 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x56(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x56((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x56((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN 1 ELSE (x56((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x122((_M - 1))) = 1) THEN 2 ELSE (IF ((x122((_M - 1))) = 2) THEN 3 ELSE (IF ((x122((_M - 1))) = 3) THEN 4 ELSE (IF ((x122((_M - 1))) = 4) THEN 1 ELSE (IF ((x122((_M - 1))) = 5) THEN 1 ELSE (x122((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x56((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x56((_M - 1))) ENDIF) ENDIF)); +DEF__157 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x57(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x57((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x57((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN 1 ELSE (x57((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (IF ((x45((_M - 1))) = 1) THEN 2 ELSE (x123((_M - 1))) ENDIF) ELSE (IF ((x57((_M - 1))) = 2) THEN (IF ((x45((_M - 1))) = 3) THEN 4 ELSE (IF ((x45((_M - 1))) = 2) THEN 3 ELSE (x123((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x57((_M - 1))) = 3) THEN 0 ELSE (IF ((x57((_M - 1))) = 4) THEN 0 ELSE (x57((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x57((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x57((_M - 1))) ENDIF) ENDIF)); +DEF__158 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x58(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x58((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x58((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x81((_M - 1))) = 1) THEN (IF (((NOT ((x7((_M - 1))) = 0)) AND (x8((_M - 1)))) <=> TRUE) THEN 2 ELSE (IF ((((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1))))) <=> TRUE) THEN 1 ELSE (x81((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x81((_M - 1))) = 2) THEN (IF ((((x32((_M - 1))) = 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) <=> TRUE) THEN 1 ELSE (IF ((((((x32((_M - 1))) = 6) AND ((x7((_M - 1))) = 2)) AND (x8((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 3 ELSE (IF (((((x32((_M - 1))) < 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) OR ((x8((_M - 1))) AND (((x7((_M - 1))) = 1) OR (x6((_M - 1)))))) <=> TRUE) THEN 2 ELSE (x81((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x81((_M - 1))) = 3) THEN (IF (((NOT (((x7((_M - 1))) = 2) AND (x8((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 2 ELSE 3 ENDIF) ELSE (x81((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x58((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x58((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x58((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x58((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x58((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x58((_M - 1))) ENDIF) ENDIF)); +DEF__159 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x59(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (x59((_M - 1))) ELSE 1 ENDIF) ENDIF)); +DEF__160 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x60(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x60((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x60((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x82((_M - 1))) = 1) THEN (x112((_M - 1))) ELSE (IF ((x82((_M - 1))) = 2) THEN (IF ((NOT ((x13((_M - 1))) = 2)) <=> TRUE) THEN 1 ELSE (x112((_M - 1))) ENDIF) ELSE (x82((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x60((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x60((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x60((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x60((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x60((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x60((_M - 1))) ENDIF) ENDIF)); +DEF__161 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x61(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x61((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x61((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x83((_M - 1))) = 1) THEN (IF (((NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0))) AND (NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)))) <=> TRUE) THEN 2 ELSE (IF ((((((((x50((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)) <=> TRUE) THEN 1 ELSE (x83((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 2) THEN (IF ((((((x2((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((((x3((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0))) <=> TRUE) THEN 1 ELSE (IF (((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF (((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2)) <=> TRUE) THEN 3 ELSE (x83((_M - 1))) ENDIF) ELSE (x83((_M - 1))) ENDIF) ELSE (x83((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 3) THEN (x109((_M - 1))) ELSE (IF ((x83((_M - 1))) = 4) THEN (IF ((NOT ((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN 2 ELSE (x109((_M - 1))) ENDIF) ELSE (x109((_M - 1))) ENDIF) ELSE (x109((_M - 1))) ENDIF) ELSE (x83((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x61((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x61((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x61((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x61((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x61((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x61((_M - 1))) ENDIF) ENDIF)); +DEF__162 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x62(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x62((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x62((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x84((_M - 1))) = 1) THEN (IF (((NOT (((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0))) AND (x5((_M - 1)))) <=> TRUE) THEN 2 ELSE 1 ENDIF) ELSE (IF ((x84((_M - 1))) = 2) THEN (IF ((((x33((_M - 1))) = 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) <=> TRUE) THEN 1 ELSE (IF (((((((x33((_M - 1))) = 6) AND ((x9((_M - 1))) = 2)) AND ((x10((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 3 ELSE (IF (((((x33((_M - 1))) < 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) OR ((x5((_M - 1))) AND (((x6((_M - 1))) OR ((x9((_M - 1))) = 1)) OR ((x10((_M - 1))) = 1)))) <=> TRUE) THEN 2 ELSE (x84((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x84((_M - 1))) = 3) THEN (IF (((((NOT ((x9((_M - 1))) = 2)) AND (NOT ((x10((_M - 1))) = 2))) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 2 ELSE (IF ((((((x9((_M - 1))) = 2) AND ((x10((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 3 ELSE (x84((_M - 1))) ENDIF) ENDIF) ELSE (x84((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x62((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x62((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x62((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x62((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x62((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x62((_M - 1))) ENDIF) ENDIF)); +DEF__163 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x63(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x63((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x63((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x63((_M - 1))) = 1) THEN (IF ((((((NOT ((x48((_M - 1))) = 0)) AND (NOT ((x47((_M - 1))) = 0))) AND (NOT ((x39((_M - 1))) = 0))) AND (NOT ((x36((_M - 1))) = 0))) AND ((x31((_M - 1))) < 11)) <=> TRUE) THEN 2 ELSE (IF ((x31((_M - 1))) = 11) THEN 5 ELSE (x63((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x63((_M - 1))) = 2) THEN (IF ((((((x48((_M - 1))) = 2) AND ((x47((_M - 1))) = 2)) AND (NOT ((x39((_M - 1))) = 0))) AND ((x36((_M - 1))) = 2)) <=> TRUE) THEN 4 ELSE (IF ((((((x48((_M - 1))) = 1) AND ((x47((_M - 1))) = 1)) AND ((x39((_M - 1))) = 0)) AND ((x36((_M - 1))) = 1)) <=> TRUE) THEN 3 ELSE (IF (((((((x48((_M - 1))) = 0) OR ((x47((_M - 1))) = 0)) OR ((x39((_M - 1))) = 0)) OR ((x36((_M - 1))) = 0)) OR ((x31((_M - 1))) = 11)) <=> TRUE) THEN 5 ELSE (x63((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x63((_M - 1))) = 3) THEN 5 ELSE (IF ((x63((_M - 1))) = 4) THEN 0 ELSE (IF ((x63((_M - 1))) = 5) THEN 0 ELSE (x63((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x63((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x63((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x63((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x63((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x63((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x63((_M - 1))) ENDIF) ENDIF)); +DEF__164 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x64(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x64((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x64((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x80((_M - 1))) = 1) THEN (x80((_M - 1))) ELSE (IF ((x80((_M - 1))) = 2) THEN (IF ((x35((_M - 1))) = 6) THEN 3 ELSE (IF ((x35((_M - 1))) < 6) THEN 2 ELSE (x116((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x80((_M - 1))) = 3) THEN (x116((_M - 1))) ELSE (x80((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x64((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x64((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x64((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x64((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x64((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x64((_M - 1))) ENDIF) ENDIF)); +DEF__165 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x65(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (IF ((x14((_M - 1))) = 0) THEN 3 ELSE (x65((_M - 1))) ENDIF) ELSE (IF ((x65((_M - 1))) = 2) THEN (IF ((x14((_M - 1))) = 8) THEN 7 ELSE (IF ((x14((_M - 1))) = 6) THEN 3 ELSE (x65((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 3) THEN (IF ((x14((_M - 1))) = 2) THEN 4 ELSE (x65((_M - 1))) ENDIF) ELSE (IF ((x65((_M - 1))) = 4) THEN (IF ((x14((_M - 1))) = 1) THEN 3 ELSE (IF ((x14((_M - 1))) = 3) THEN 6 ELSE (x65((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 5) THEN (IF ((x14((_M - 1))) = 7) THEN 2 ELSE (x65((_M - 1))) ENDIF) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN 2 ELSE (IF ((x14((_M - 1))) = 4) THEN 9 ELSE (x65((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x65((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x65((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x86((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x65((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x65((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN 12 ELSE (IF ((x55((_M - 1))) = 4) THEN 9 ELSE (x65((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (IF ((x14((_M - 1))) = 9) THEN 5 ELSE (IF ((x14((_M - 1))) = 10) THEN 8 ELSE (x65((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (x65((_M - 1))) ELSE (IF ((x57((_M - 1))) = 2) THEN (x65((_M - 1))) ELSE (IF ((x57((_M - 1))) = 3) THEN 10 ELSE (IF ((x57((_M - 1))) = 4) THEN 11 ELSE (x65((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x65((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE 1 ENDIF) ENDIF)); +DEF__166 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x66(_M)) = (IF (_M = _base) THEN FALSE ELSE (x21((_M - 1))) ENDIF)); +DEF__168 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x68(_M)) = (IF (_M = _base) THEN FALSE ELSE (x17((_M - 1))) ENDIF)); +DEF__171 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x71(_M)) = (IF (_M = _base) THEN FALSE ELSE (x22((_M - 1))) ENDIF)); +DEF__173 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x73(_M)) = (IF (_M = _base) THEN FALSE ELSE (x16((_M - 1))) ENDIF)); +% Property(ies) + +P : _nat -> BOOLEAN = LAMBDA(_M : _nat): (x129(_M)); + + + + +% INDUCT : Single property verification. +% INDUCT : MAIN. +% INDUCT : not refinement_pass. +% INDUCT : Checking K = 2. No message received. +% INDUCT : setup step loop - initialize step. +PUSH; +% INDUCT : ;4b +ASSERT (DEF__174( (_n + 0))); +ASSERT (DEF__176( (_n + 0))); +ASSERT (DEF__177( (_n + 0))); +ASSERT (DEF__178( (_n + 0))); +ASSERT (DEF__179( (_n + 0))); +ASSERT (DEF__180( (_n + 0))); +ASSERT (DEF__181( (_n + 0))); +ASSERT (DEF__182( (_n + 0))); +ASSERT (DEF__183( (_n + 0))); +ASSERT (DEF__184( (_n + 0))); +ASSERT (DEF__185( (_n + 0))); +ASSERT (DEF__186( (_n + 0))); +ASSERT (DEF__187( (_n + 0))); +ASSERT (DEF__188( (_n + 0))); +ASSERT (DEF__189( (_n + 0))); +ASSERT (DEF__190( (_n + 0))); +ASSERT (DEF__191( (_n + 0))); +ASSERT (DEF__192( (_n + 0))); +ASSERT (DEF__193( (_n + 0))); +ASSERT (DEF__194( (_n + 0))); +ASSERT (DEF__195( (_n + 0))); +ASSERT (DEF__196( (_n + 0))); +ASSERT (DEF__197( (_n + 0))); +ASSERT (DEF__198( (_n + 0))); +ASSERT (DEF__199( (_n + 0))); +ASSERT (DEF__200( (_n + 0))); +ASSERT (DEF__201( (_n + 0))); +ASSERT (DEF__202( (_n + 0))); +ASSERT (DEF__115( (_n + 0))); +ASSERT (DEF__203( (_n + 0))); +ASSERT (DEF__116( (_n + 0))); +ASSERT (DEF__204( (_n + 0))); +ASSERT (DEF__117( (_n + 0))); +ASSERT (DEF__205( (_n + 0))); +ASSERT (DEF__206( (_n + 0))); +ASSERT (DEF__207( (_n + 0))); +ASSERT (DEF__120( (_n + 0))); +ASSERT (DEF__208( (_n + 0))); +ASSERT (DEF__121( (_n + 0))); +ASSERT (DEF__209( (_n + 0))); +ASSERT (DEF__122( (_n + 0))); +ASSERT (DEF__210( (_n + 0))); +ASSERT (DEF__211( (_n + 0))); +ASSERT (DEF__212( (_n + 0))); +ASSERT (DEF__126( (_n + 0))); +ASSERT (DEF__213( (_n + 0))); +ASSERT (DEF__127( (_n + 0))); +ASSERT (DEF__214( (_n + 0))); +ASSERT (DEF__128( (_n + 0))); +ASSERT (DEF__215( (_n + 0))); +ASSERT (DEF__216( (_n + 0))); +ASSERT (DEF__129( (_n + 0))); +ASSERT (DEF__217( (_n + 0))); +ASSERT (DEF__130( (_n + 0))); +ASSERT (DEF__131( (_n + 0))); +ASSERT (DEF__218( (_n + 0))); +ASSERT (DEF__132( (_n + 0))); +ASSERT (DEF__219( (_n + 0))); +ASSERT (DEF__133( (_n + 0))); +ASSERT (DEF__220( (_n + 0))); +ASSERT (DEF__134( (_n + 0))); +ASSERT (DEF__221( (_n + 0))); +ASSERT (DEF__222( (_n + 0))); +ASSERT (DEF__135( (_n + 0))); +ASSERT (DEF__223( (_n + 0))); +ASSERT (DEF__136( (_n + 0))); +ASSERT (DEF__224( (_n + 0))); +ASSERT (DEF__137( (_n + 0))); +ASSERT (DEF__225( (_n + 0))); +ASSERT (DEF__138( (_n + 0))); +ASSERT (DEF__226( (_n + 0))); +ASSERT (DEF__139( (_n + 0))); +ASSERT (DEF__227( (_n + 0))); +ASSERT (DEF__140( (_n + 0))); +ASSERT (DEF__228( (_n + 0))); +ASSERT (DEF__141( (_n + 0))); +ASSERT (DEF__229( (_n + 0))); +ASSERT (DEF__142( (_n + 0))); +ASSERT (DEF__143( (_n + 0))); +ASSERT (DEF__144( (_n + 0))); +ASSERT (DEF__145( (_n + 0))); +ASSERT (DEF__146( (_n + 0))); +ASSERT (DEF__147( (_n + 0))); +ASSERT (DEF__148( (_n + 0))); +ASSERT (DEF__149( (_n + 0))); +ASSERT (DEF__150( (_n + 0))); +ASSERT (DEF__151( (_n + 0))); +ASSERT (DEF__152( (_n + 0))); +ASSERT (DEF__153( (_n + 0))); +ASSERT (DEF__154( (_n + 0))); +ASSERT (DEF__155( (_n + 0))); +ASSERT (DEF__156( (_n + 0))); +ASSERT (DEF__157( (_n + 0))); +ASSERT (DEF__158( (_n + 0))); +ASSERT (DEF__159( (_n + 0))); +ASSERT (DEF__160( (_n + 0))); +ASSERT (DEF__161( (_n + 0))); +ASSERT (DEF__162( (_n + 0))); +ASSERT (DEF__163( (_n + 0))); +ASSERT (DEF__164( (_n + 0))); +ASSERT (DEF__165( (_n + 0))); +ASSERT (DEF__166( (_n + 0))); +ASSERT (DEF__168( (_n + 0))); +ASSERT (DEF__171( (_n + 0))); +ASSERT (DEF__173( (_n + 0))); +ASSERT (DEF__174( (_n - 1))); +ASSERT (DEF__176( (_n - 1))); +ASSERT (DEF__177( (_n - 1))); +ASSERT (DEF__178( (_n - 1))); +ASSERT (DEF__179( (_n - 1))); +ASSERT (DEF__180( (_n - 1))); +ASSERT (DEF__181( (_n - 1))); +ASSERT (DEF__182( (_n - 1))); +ASSERT (DEF__183( (_n - 1))); +ASSERT (DEF__184( (_n - 1))); +ASSERT (DEF__185( (_n - 1))); +ASSERT (DEF__186( (_n - 1))); +ASSERT (DEF__187( (_n - 1))); +ASSERT (DEF__188( (_n - 1))); +ASSERT (DEF__189( (_n - 1))); +ASSERT (DEF__190( (_n - 1))); +ASSERT (DEF__191( (_n - 1))); +ASSERT (DEF__192( (_n - 1))); +ASSERT (DEF__193( (_n - 1))); +ASSERT (DEF__194( (_n - 1))); +ASSERT (DEF__195( (_n - 1))); +ASSERT (DEF__196( (_n - 1))); +ASSERT (DEF__197( (_n - 1))); +ASSERT (DEF__198( (_n - 1))); +ASSERT (DEF__199( (_n - 1))); +ASSERT (DEF__200( (_n - 1))); +ASSERT (DEF__201( (_n - 1))); +ASSERT (DEF__202( (_n - 1))); +ASSERT (DEF__115( (_n - 1))); +ASSERT (DEF__203( (_n - 1))); +ASSERT (DEF__116( (_n - 1))); +ASSERT (DEF__204( (_n - 1))); +ASSERT (DEF__117( (_n - 1))); +ASSERT (DEF__205( (_n - 1))); +ASSERT (DEF__206( (_n - 1))); +ASSERT (DEF__207( (_n - 1))); +ASSERT (DEF__120( (_n - 1))); +ASSERT (DEF__208( (_n - 1))); +ASSERT (DEF__121( (_n - 1))); +ASSERT (DEF__209( (_n - 1))); +ASSERT (DEF__122( (_n - 1))); +ASSERT (DEF__210( (_n - 1))); +ASSERT (DEF__211( (_n - 1))); +ASSERT (DEF__212( (_n - 1))); +ASSERT (DEF__126( (_n - 1))); +ASSERT (DEF__213( (_n - 1))); +ASSERT (DEF__127( (_n - 1))); +ASSERT (DEF__214( (_n - 1))); +ASSERT (DEF__128( (_n - 1))); +ASSERT (DEF__215( (_n - 1))); +ASSERT (DEF__216( (_n - 1))); +ASSERT (DEF__129( (_n - 1))); +ASSERT (DEF__217( (_n - 1))); +ASSERT (DEF__130( (_n - 1))); +ASSERT (DEF__131( (_n - 1))); +ASSERT (DEF__218( (_n - 1))); +ASSERT (DEF__132( (_n - 1))); +ASSERT (DEF__219( (_n - 1))); +ASSERT (DEF__133( (_n - 1))); +ASSERT (DEF__220( (_n - 1))); +ASSERT (DEF__134( (_n - 1))); +ASSERT (DEF__221( (_n - 1))); +ASSERT (DEF__222( (_n - 1))); +ASSERT (DEF__135( (_n - 1))); +ASSERT (DEF__223( (_n - 1))); +ASSERT (DEF__136( (_n - 1))); +ASSERT (DEF__224( (_n - 1))); +ASSERT (DEF__137( (_n - 1))); +ASSERT (DEF__225( (_n - 1))); +ASSERT (DEF__138( (_n - 1))); +ASSERT (DEF__226( (_n - 1))); +ASSERT (DEF__139( (_n - 1))); +ASSERT (DEF__227( (_n - 1))); +ASSERT (DEF__140( (_n - 1))); +ASSERT (DEF__228( (_n - 1))); +ASSERT (DEF__141( (_n - 1))); +ASSERT (DEF__229( (_n - 1))); +ASSERT (DEF__142( (_n - 1))); +ASSERT (DEF__143( (_n - 1))); +ASSERT (DEF__144( (_n - 1))); +ASSERT (DEF__145( (_n - 1))); +ASSERT (DEF__146( (_n - 1))); +ASSERT (DEF__147( (_n - 1))); +ASSERT (DEF__148( (_n - 1))); +ASSERT (DEF__149( (_n - 1))); +ASSERT (DEF__150( (_n - 1))); +ASSERT (DEF__151( (_n - 1))); +ASSERT (DEF__152( (_n - 1))); +ASSERT (DEF__153( (_n - 1))); +ASSERT (DEF__154( (_n - 1))); +ASSERT (DEF__155( (_n - 1))); +ASSERT (DEF__156( (_n - 1))); +ASSERT (DEF__157( (_n - 1))); +ASSERT (DEF__158( (_n - 1))); +ASSERT (DEF__159( (_n - 1))); +ASSERT (DEF__160( (_n - 1))); +ASSERT (DEF__161( (_n - 1))); +ASSERT (DEF__162( (_n - 1))); +ASSERT (DEF__163( (_n - 1))); +ASSERT (DEF__164( (_n - 1))); +ASSERT (DEF__165( (_n - 1))); +ASSERT (DEF__166( (_n - 1))); +ASSERT (DEF__168( (_n - 1))); +ASSERT (DEF__171( (_n - 1))); +ASSERT (DEF__173( (_n - 1))); +ASSERT (P( (_n - 1))); +ASSERT (NOT (P( _n))); +% PUSH; %safe +ASSERT TRUE; +CHECKSAT; +%ECHO "__DONE__"; +% INDUCT : sat +% INDUCT : __DONE__ +% POP; %safe +% INDUCT : Inductive step is Invalid at K = 2. Continuing search. +POP; +ASSERT (P( (_n - 1))); +ASSERT (P( (_n - 2))); +ASSERT (DEF__174( (_n + 0))); +ASSERT (DEF__176( (_n + 0))); +ASSERT (DEF__177( (_n + 0))); +ASSERT (DEF__178( (_n + 0))); +ASSERT (DEF__179( (_n + 0))); +ASSERT (DEF__180( (_n + 0))); +ASSERT (DEF__181( (_n + 0))); +ASSERT (DEF__182( (_n + 0))); +ASSERT (DEF__183( (_n + 0))); +ASSERT (DEF__184( (_n + 0))); +ASSERT (DEF__185( (_n + 0))); +ASSERT (DEF__186( (_n + 0))); +ASSERT (DEF__187( (_n + 0))); +ASSERT (DEF__188( (_n + 0))); +ASSERT (DEF__189( (_n + 0))); +ASSERT (DEF__190( (_n + 0))); +ASSERT (DEF__191( (_n + 0))); +ASSERT (DEF__192( (_n + 0))); +ASSERT (DEF__193( (_n + 0))); +ASSERT (DEF__194( (_n + 0))); +ASSERT (DEF__195( (_n + 0))); +ASSERT (DEF__196( (_n + 0))); +ASSERT (DEF__197( (_n + 0))); +ASSERT (DEF__198( (_n + 0))); +ASSERT (DEF__199( (_n + 0))); +ASSERT (DEF__200( (_n + 0))); +ASSERT (DEF__201( (_n + 0))); +ASSERT (DEF__202( (_n + 0))); +ASSERT (DEF__115( (_n + 0))); +ASSERT (DEF__203( (_n + 0))); +ASSERT (DEF__116( (_n + 0))); +ASSERT (DEF__204( (_n + 0))); +ASSERT (DEF__117( (_n + 0))); +ASSERT (DEF__205( (_n + 0))); +ASSERT (DEF__206( (_n + 0))); +ASSERT (DEF__207( (_n + 0))); +ASSERT (DEF__120( (_n + 0))); +ASSERT (DEF__208( (_n + 0))); +ASSERT (DEF__121( (_n + 0))); +ASSERT (DEF__209( (_n + 0))); +ASSERT (DEF__122( (_n + 0))); +ASSERT (DEF__210( (_n + 0))); +ASSERT (DEF__211( (_n + 0))); +ASSERT (DEF__212( (_n + 0))); +ASSERT (DEF__126( (_n + 0))); +ASSERT (DEF__213( (_n + 0))); +ASSERT (DEF__127( (_n + 0))); +ASSERT (DEF__214( (_n + 0))); +ASSERT (DEF__128( (_n + 0))); +ASSERT (DEF__215( (_n + 0))); +ASSERT (DEF__216( (_n + 0))); +ASSERT (DEF__129( (_n + 0))); +ASSERT (DEF__217( (_n + 0))); +ASSERT (DEF__130( (_n + 0))); +ASSERT (DEF__131( (_n + 0))); +ASSERT (DEF__218( (_n + 0))); +ASSERT (DEF__132( (_n + 0))); +ASSERT (DEF__219( (_n + 0))); +ASSERT (DEF__133( (_n + 0))); +ASSERT (DEF__220( (_n + 0))); +ASSERT (DEF__134( (_n + 0))); +ASSERT (DEF__221( (_n + 0))); +ASSERT (DEF__222( (_n + 0))); +ASSERT (DEF__135( (_n + 0))); +ASSERT (DEF__223( (_n + 0))); +ASSERT (DEF__136( (_n + 0))); +ASSERT (DEF__224( (_n + 0))); +ASSERT (DEF__137( (_n + 0))); +ASSERT (DEF__225( (_n + 0))); +ASSERT (DEF__138( (_n + 0))); +ASSERT (DEF__226( (_n + 0))); +ASSERT (DEF__139( (_n + 0))); +ASSERT (DEF__227( (_n + 0))); +ASSERT (DEF__140( (_n + 0))); +ASSERT (DEF__228( (_n + 0))); +ASSERT (DEF__141( (_n + 0))); +ASSERT (DEF__229( (_n + 0))); +ASSERT (DEF__142( (_n + 0))); +ASSERT (DEF__143( (_n + 0))); +ASSERT (DEF__144( (_n + 0))); +ASSERT (DEF__145( (_n + 0))); +ASSERT (DEF__146( (_n + 0))); +ASSERT (DEF__147( (_n + 0))); +ASSERT (DEF__148( (_n + 0))); +ASSERT (DEF__149( (_n + 0))); +ASSERT (DEF__150( (_n + 0))); +ASSERT (DEF__151( (_n + 0))); +ASSERT (DEF__152( (_n + 0))); +ASSERT (DEF__153( (_n + 0))); +ASSERT (DEF__154( (_n + 0))); +ASSERT (DEF__155( (_n + 0))); +ASSERT (DEF__156( (_n + 0))); +ASSERT (DEF__157( (_n + 0))); +ASSERT (DEF__158( (_n + 0))); +ASSERT (DEF__159( (_n + 0))); +ASSERT (DEF__160( (_n + 0))); +ASSERT (DEF__161( (_n + 0))); +ASSERT (DEF__162( (_n + 0))); +ASSERT (DEF__163( (_n + 0))); +ASSERT (DEF__164( (_n + 0))); +ASSERT (DEF__165( (_n + 0))); +ASSERT (DEF__166( (_n + 0))); +ASSERT (DEF__168( (_n + 0))); +ASSERT (DEF__171( (_n + 0))); +ASSERT (DEF__173( (_n + 0))); +% INDUCT : not refinement_pass. +% INDUCT : Checking K = 3. No message received. +% INDUCT : setup step loop - initialize step. +PUSH; +% INDUCT : ;4b +ASSERT (DEF__174( (_n - 1))); +ASSERT (DEF__176( (_n - 1))); +ASSERT (DEF__177( (_n - 1))); +ASSERT (DEF__178( (_n - 1))); +ASSERT (DEF__179( (_n - 1))); +ASSERT (DEF__180( (_n - 1))); +ASSERT (DEF__181( (_n - 1))); +ASSERT (DEF__182( (_n - 1))); +ASSERT (DEF__183( (_n - 1))); +ASSERT (DEF__184( (_n - 1))); +ASSERT (DEF__185( (_n - 1))); +ASSERT (DEF__186( (_n - 1))); +ASSERT (DEF__187( (_n - 1))); +ASSERT (DEF__188( (_n - 1))); +ASSERT (DEF__189( (_n - 1))); +ASSERT (DEF__190( (_n - 1))); +ASSERT (DEF__191( (_n - 1))); +ASSERT (DEF__192( (_n - 1))); +ASSERT (DEF__193( (_n - 1))); +ASSERT (DEF__194( (_n - 1))); +ASSERT (DEF__195( (_n - 1))); +ASSERT (DEF__196( (_n - 1))); +ASSERT (DEF__197( (_n - 1))); +ASSERT (DEF__198( (_n - 1))); +ASSERT (DEF__199( (_n - 1))); +ASSERT (DEF__200( (_n - 1))); +ASSERT (DEF__201( (_n - 1))); +ASSERT (DEF__202( (_n - 1))); +ASSERT (DEF__115( (_n - 1))); +ASSERT (DEF__203( (_n - 1))); +ASSERT (DEF__116( (_n - 1))); +ASSERT (DEF__204( (_n - 1))); +ASSERT (DEF__117( (_n - 1))); +ASSERT (DEF__205( (_n - 1))); +ASSERT (DEF__206( (_n - 1))); +ASSERT (DEF__207( (_n - 1))); +ASSERT (DEF__120( (_n - 1))); +ASSERT (DEF__208( (_n - 1))); +ASSERT (DEF__121( (_n - 1))); +ASSERT (DEF__209( (_n - 1))); +ASSERT (DEF__122( (_n - 1))); +ASSERT (DEF__210( (_n - 1))); +ASSERT (DEF__211( (_n - 1))); +ASSERT (DEF__212( (_n - 1))); +ASSERT (DEF__126( (_n - 1))); +ASSERT (DEF__213( (_n - 1))); +ASSERT (DEF__127( (_n - 1))); +ASSERT (DEF__214( (_n - 1))); +ASSERT (DEF__128( (_n - 1))); +ASSERT (DEF__215( (_n - 1))); +ASSERT (DEF__216( (_n - 1))); +ASSERT (DEF__129( (_n - 1))); +ASSERT (DEF__217( (_n - 1))); +ASSERT (DEF__130( (_n - 1))); +ASSERT (DEF__131( (_n - 1))); +ASSERT (DEF__218( (_n - 1))); +ASSERT (DEF__132( (_n - 1))); +ASSERT (DEF__219( (_n - 1))); +ASSERT (DEF__133( (_n - 1))); +ASSERT (DEF__220( (_n - 1))); +ASSERT (DEF__134( (_n - 1))); +ASSERT (DEF__221( (_n - 1))); +ASSERT (DEF__222( (_n - 1))); +ASSERT (DEF__135( (_n - 1))); +ASSERT (DEF__223( (_n - 1))); +ASSERT (DEF__136( (_n - 1))); +ASSERT (DEF__224( (_n - 1))); +ASSERT (DEF__137( (_n - 1))); +ASSERT (DEF__225( (_n - 1))); +ASSERT (DEF__138( (_n - 1))); +ASSERT (DEF__226( (_n - 1))); +ASSERT (DEF__139( (_n - 1))); +ASSERT (DEF__227( (_n - 1))); +ASSERT (DEF__140( (_n - 1))); +ASSERT (DEF__228( (_n - 1))); +ASSERT (DEF__141( (_n - 1))); +ASSERT (DEF__229( (_n - 1))); +ASSERT (DEF__142( (_n - 1))); +ASSERT (DEF__143( (_n - 1))); +ASSERT (DEF__144( (_n - 1))); +ASSERT (DEF__145( (_n - 1))); +ASSERT (DEF__146( (_n - 1))); +ASSERT (DEF__147( (_n - 1))); +ASSERT (DEF__148( (_n - 1))); +ASSERT (DEF__149( (_n - 1))); +ASSERT (DEF__150( (_n - 1))); +ASSERT (DEF__151( (_n - 1))); +ASSERT (DEF__152( (_n - 1))); +ASSERT (DEF__153( (_n - 1))); +ASSERT (DEF__154( (_n - 1))); +ASSERT (DEF__155( (_n - 1))); +ASSERT (DEF__156( (_n - 1))); +ASSERT (DEF__157( (_n - 1))); +ASSERT (DEF__158( (_n - 1))); +ASSERT (DEF__159( (_n - 1))); +ASSERT (DEF__160( (_n - 1))); +ASSERT (DEF__161( (_n - 1))); +ASSERT (DEF__162( (_n - 1))); +ASSERT (DEF__163( (_n - 1))); +ASSERT (DEF__164( (_n - 1))); +ASSERT (DEF__165( (_n - 1))); +ASSERT (DEF__166( (_n - 1))); +ASSERT (DEF__168( (_n - 1))); +ASSERT (DEF__171( (_n - 1))); +ASSERT (DEF__173( (_n - 1))); +ASSERT (DEF__174( (_n - 2))); +ASSERT (DEF__176( (_n - 2))); +ASSERT (DEF__177( (_n - 2))); +ASSERT (DEF__178( (_n - 2))); +ASSERT (DEF__179( (_n - 2))); +ASSERT (DEF__180( (_n - 2))); +ASSERT (DEF__181( (_n - 2))); +ASSERT (DEF__182( (_n - 2))); +ASSERT (DEF__183( (_n - 2))); +ASSERT (DEF__184( (_n - 2))); +ASSERT (DEF__185( (_n - 2))); +ASSERT (DEF__186( (_n - 2))); +ASSERT (DEF__187( (_n - 2))); +ASSERT (DEF__188( (_n - 2))); +ASSERT (DEF__189( (_n - 2))); +ASSERT (DEF__190( (_n - 2))); +ASSERT (DEF__191( (_n - 2))); +ASSERT (DEF__192( (_n - 2))); +ASSERT (DEF__193( (_n - 2))); +ASSERT (DEF__194( (_n - 2))); +ASSERT (DEF__195( (_n - 2))); +ASSERT (DEF__196( (_n - 2))); +ASSERT (DEF__197( (_n - 2))); +ASSERT (DEF__198( (_n - 2))); +ASSERT (DEF__199( (_n - 2))); +ASSERT (DEF__200( (_n - 2))); +ASSERT (DEF__201( (_n - 2))); +ASSERT (DEF__202( (_n - 2))); +ASSERT (DEF__115( (_n - 2))); +ASSERT (DEF__203( (_n - 2))); +ASSERT (DEF__116( (_n - 2))); +ASSERT (DEF__204( (_n - 2))); +ASSERT (DEF__117( (_n - 2))); +ASSERT (DEF__205( (_n - 2))); +ASSERT (DEF__206( (_n - 2))); +ASSERT (DEF__207( (_n - 2))); +ASSERT (DEF__120( (_n - 2))); +ASSERT (DEF__208( (_n - 2))); +ASSERT (DEF__121( (_n - 2))); +ASSERT (DEF__209( (_n - 2))); +ASSERT (DEF__122( (_n - 2))); +ASSERT (DEF__210( (_n - 2))); +ASSERT (DEF__211( (_n - 2))); +ASSERT (DEF__212( (_n - 2))); +ASSERT (DEF__126( (_n - 2))); +ASSERT (DEF__213( (_n - 2))); +ASSERT (DEF__127( (_n - 2))); +ASSERT (DEF__214( (_n - 2))); +ASSERT (DEF__128( (_n - 2))); +ASSERT (DEF__215( (_n - 2))); +ASSERT (DEF__216( (_n - 2))); +ASSERT (DEF__129( (_n - 2))); +ASSERT (DEF__217( (_n - 2))); +ASSERT (DEF__130( (_n - 2))); +ASSERT (DEF__131( (_n - 2))); +ASSERT (DEF__218( (_n - 2))); +ASSERT (DEF__132( (_n - 2))); +ASSERT (DEF__219( (_n - 2))); +ASSERT (DEF__133( (_n - 2))); +ASSERT (DEF__220( (_n - 2))); +ASSERT (DEF__134( (_n - 2))); +ASSERT (DEF__221( (_n - 2))); +ASSERT (DEF__222( (_n - 2))); +ASSERT (DEF__135( (_n - 2))); +ASSERT (DEF__223( (_n - 2))); +ASSERT (DEF__136( (_n - 2))); +ASSERT (DEF__224( (_n - 2))); +ASSERT (DEF__137( (_n - 2))); +ASSERT (DEF__225( (_n - 2))); +ASSERT (DEF__138( (_n - 2))); +ASSERT (DEF__226( (_n - 2))); +ASSERT (DEF__139( (_n - 2))); +ASSERT (DEF__227( (_n - 2))); +ASSERT (DEF__140( (_n - 2))); +ASSERT (DEF__228( (_n - 2))); +ASSERT (DEF__141( (_n - 2))); +ASSERT (DEF__229( (_n - 2))); +ASSERT (DEF__142( (_n - 2))); +ASSERT (DEF__143( (_n - 2))); +ASSERT (DEF__144( (_n - 2))); +ASSERT (DEF__145( (_n - 2))); +ASSERT (DEF__146( (_n - 2))); +ASSERT (DEF__147( (_n - 2))); +ASSERT (DEF__148( (_n - 2))); +ASSERT (DEF__149( (_n - 2))); +ASSERT (DEF__150( (_n - 2))); +ASSERT (DEF__151( (_n - 2))); +ASSERT (DEF__152( (_n - 2))); +ASSERT (DEF__153( (_n - 2))); +ASSERT (DEF__154( (_n - 2))); +ASSERT (DEF__155( (_n - 2))); +ASSERT (DEF__156( (_n - 2))); +ASSERT (DEF__157( (_n - 2))); +ASSERT (DEF__158( (_n - 2))); +ASSERT (DEF__159( (_n - 2))); +ASSERT (DEF__160( (_n - 2))); +ASSERT (DEF__161( (_n - 2))); +ASSERT (DEF__162( (_n - 2))); +ASSERT (DEF__163( (_n - 2))); +ASSERT (DEF__164( (_n - 2))); +ASSERT (DEF__165( (_n - 2))); +ASSERT (DEF__166( (_n - 2))); +ASSERT (DEF__168( (_n - 2))); +ASSERT (DEF__171( (_n - 2))); +ASSERT (DEF__173( (_n - 2))); +ASSERT (NOT (P( _n))); +% PUSH; %safe +ASSERT TRUE; +CHECKSAT; +%ECHO "__DONE__"; +% INDUCT : Abort in 3 step. |