nanoCoP---2.0.THM-Prf.s

%------------------------------------------------------------------------------
% File     : nanoCoP---2.0
% Problem  : SWW474+5 : TPTP v8.1.2. Released v5.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : nanocop.sh %s %d

% Computer : n003.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Fri May 19 12:26:17 EDT 2023

% Result   : Theorem 43.19s 42.73s
% Output   : Proof 43.19s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13  % Problem  : SWW474+5 : TPTP v8.1.2. Released v5.3.0.
% 0.07/0.13  % Command  : nanocop.sh %s %d
% 0.12/0.34  % Computer : n003.cluster.edu
% 0.12/0.34  % Model    : x86_64 x86_64
% 0.12/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34  % Memory   : 8042.1875MB
% 0.12/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit : 300
% 0.12/0.34  % WCLimit  : 300
% 0.12/0.34  % DateTime : Thu May 18 22:49:15 EDT 2023
% 0.12/0.34  % CPUTime  : 
% 43.19/42.73  
% 43.19/42.73  /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 43.19/42.73  Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 43.19/42.73  %-----------------------------------------------------
% 43.19/42.73  ncf(matrix, plain, [(1324 ^ _285294) ^ [] : [hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), hoare_122391849derivs(state), hAPP(fun(pname, bool), fun(hoare_509422987triple(state), bool), hAPP(fun(pname, hoare_509422987triple(state)), fun(fun(pname, bool), fun(hoare_509422987triple(state), bool)), image(pname, hoare_509422987triple(state)), hAPP(fun(pname, com), fun(pname, hoare_509422987triple(state)), hAPP(fun(com, hoare_509422987triple(state)), fun(fun(pname, com), fun(pname, hoare_509422987triple(state))), combb(com, hoare_509422987triple(state), pname), hoare_Mirabelle_MGT), body_1)), hAPP(fun(pname, option(com)), fun(pname, bool), dom(pname, com), body))), hAPP(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool), hAPP(hoare_509422987triple(state), fun(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool)), insert(hoare_509422987triple(state)), hAPP(com, hoare_509422987triple(state), hoare_Mirabelle_MGT, y)), bot_bot(fun(hoare_509422987triple(state), bool)))))], !, (1240 ^ _218455) ^ [_281332, _281334] : [hBOOL(hAPP(bool, bool, hAPP(bool, fun(bool, bool), fconj, _281334), _281332)), -(hBOOL(_281332))], (1176 ^ _218455) ^ [_278627, _278629] : [ti(pname, _278629) = ti(pname, _278627), -(hAPP(pname, com, body_1, _278629) = hAPP(pname, com, body_1, _278627))], (268 ^ _218455) ^ [_228362] : [-(ti(fun(_228362, bool), bot_bot(fun(_228362, bool))) = bot_bot(fun(_228362, bool)))], (1182 ^ _218455) ^ [_278871, _278873] : [-(finite_finite_1(fun(_278873, _278871))), finite_finite_1(_278871), finite_finite_1(_278873)], (1312 ^ _218455) ^ [] : [-(hBOOL(wT_bodies))], (346 ^ _218455) ^ [_231936, _231938, _231940, _231942] : [hBOOL(hAPP(fun(hoare_509422987triple(_231942), bool), bool, hAPP(fun(hoare_509422987triple(_231942), bool), fun(fun(hoare_509422987triple(_231942), bool), bool), hoare_122391849derivs(_231942), _231938), _231936)), hBOOL(hAPP(fun(hoare_509422987triple(_231942), bool), bool, hAPP(fun(hoare_509422987triple(_231942), bool), fun(fun(hoare_509422987triple(_231942), bool), bool), hoare_122391849derivs(_231942), _231940), _231938)), -(hBOOL(hAPP(fun(hoare_509422987triple(_231942), bool), bool, hAPP(fun(hoare_509422987triple(_231942), bool), fun(fun(hoare_509422987triple(_231942), bool), bool), hoare_122391849derivs(_231942), _231940), _231936)))], (937 ^ _218455) ^ [_264225, _264227, _264229, _264231] : [hBOOL(hAPP(fun(_264231, bool), bool, hAPP(fun(_264231, bool), fun(fun(_264231, bool), bool), ord_less_eq(fun(_264231, bool)), _264227), _264225)), -(hBOOL(hAPP(fun(_264231, bool), bool, hAPP(fun(_264231, bool), fun(fun(_264231, bool), bool), ord_less_eq(fun(_264231, bool)), hAPP(fun(_264231, bool), fun(_264231, bool), hAPP(_264231, fun(fun(_264231, bool), fun(_264231, bool)), insert(_264231), _264229), _264227)), hAPP(fun(_264231, bool), fun(_264231, bool), hAPP(_264231, fun(fun(_264231, bool), fun(_264231, bool)), insert(_264231), _264229), _264225))))], (664 ^ _218455) ^ [_248830, _248832, _248834] : [-(hAPP(fun(_248834, bool), fun(_248834, bool), hAPP(_248834, fun(fun(_248834, bool), fun(_248834, bool)), insert(_248834), _248832), hAPP(fun(_248834, bool), fun(_248834, bool), collect(_248834), _248830)) = hAPP(fun(_248834, bool), fun(_248834, bool), collect(_248834), hAPP(fun(_248834, bool), fun(_248834, bool), hAPP(fun(_248834, fun(bool, bool)), fun(fun(_248834, bool), fun(_248834, bool)), combs(_248834, bool, bool), hAPP(fun(_248834, bool), fun(_248834, fun(bool, bool)), hAPP(fun(bool, fun(bool, bool)), fun(fun(_248834, bool), fun(_248834, fun(bool, bool))), combb(bool, fun(bool, bool), _248834), fimplies), hAPP(fun(_248834, bool), fun(_248834, bool), hAPP(fun(bool, bool), fun(fun(_248834, bool), fun(_248834, bool)), combb(bool, bool, _248834), fNot), hAPP(_248834, fun(_248834, bool), hAPP(fun(_248834, fun(_248834, bool)), fun(_248834, fun(_248834, bool)), combc(_248834, _248834, bool), fequal(_248834)), _248832)))), _248830)))], (296 ^ _218455) ^ [_229600, _229602, _229604, _229606] : [-(ti(_229606, hAPP(_229604, _229606, _229602, _229600)) = hAPP(_229604, _229606, _229602, _229600))], (1310 ^ _218455) ^ [] : [-(hBOOL(hoare_1883395792gleton))], (970 ^ _218455) ^ [_266117, _266119, _266121, _266123] : [-(hBOOL(hAPP(fun(_266123, bool), bool, hAPP(_266123, fun(fun(_266123, bool), bool), member(_266123), _266119), _266117))), 973 ^ _218455 : [(980 ^ _218455) ^ [] : [hBOOL(hAPP(fun(_266123, bool), bool, hAPP(fun(_266123, bool), fun(fun(_266123, bool), bool), ord_less_eq(fun(_266123, bool)), _266117), _266121)), -(hBOOL(hAPP(fun(_266123, bool), bool, hAPP(fun(_266123, bool), fun(fun(_266123, bool), bool), ord_less_eq(fun(_266123, bool)), _266117), hAPP(fun(_266123, bool), fun(_266123, bool), hAPP(_266123, fun(fun(_266123, bool), fun(_266123, bool)), insert(_266123), _266119), _266121))))], (974 ^ _218455) ^ [] : [hBOOL(hAPP(fun(_266123, bool), bool, hAPP(fun(_266123, bool), fun(fun(_266123, bool), bool), ord_less_eq(fun(_266123, bool)), _266117), hAPP(fun(_266123, bool), fun(_266123, bool), hAPP(_266123, fun(fun(_266123, bool), fun(_266123, bool)), insert(_266123), _266119), _266121))), -(hBOOL(hAPP(fun(_266123, bool), bool, hAPP(fun(_266123, bool), fun(fun(_266123, bool), bool), ord_less_eq(fun(_266123, bool)), _266117), _266121)))]]], (286 ^ _218455) ^ [] : [-(ti(fun(bool, fun(bool, bool)), fdisj) = fdisj)], (1069 ^ _218455) ^ [_272911, _272913] : [-(hAPP(fun(_272913, bool), fun(_272913, bool), collect(_272913), hAPP(_272913, fun(_272913, bool), hAPP(fun(_272913, fun(_272913, bool)), fun(_272913, fun(_272913, bool)), combc(_272913, _272913, bool), fequal(_272913)), _272911)) = hAPP(fun(_272913, bool), fun(_272913, bool), hAPP(_272913, fun(fun(_272913, bool), fun(_272913, bool)), insert(_272913), _272911), bot_bot(fun(_272913, bool))))], (304 ^ _218455) ^ [_229899] : [hBOOL(_229899), -(hBOOL(ti(bool, _229899)))], (835 ^ _218455) ^ [_259019, _259021, _259023, _259025, _259027] : [-(hAPP(fun(_259027, bool), fun(_259027, bool), hAPP(_259027, fun(fun(_259027, bool), fun(_259027, bool)), insert(_259027), _259025), hAPP(fun(_259027, bool), fun(_259027, bool), hAPP(_259027, fun(fun(_259027, bool), fun(_259027, bool)), insert(_259027), _259023), bot_bot(fun(_259027, bool)))) = hAPP(fun(_259027, bool), fun(_259027, bool), hAPP(_259027, fun(fun(_259027, bool), fun(_259027, bool)), insert(_259027), _259021), hAPP(fun(_259027, bool), fun(_259027, bool), hAPP(_259027, fun(fun(_259027, bool), fun(_259027, bool)), insert(_259027), _259019), bot_bot(fun(_259027, bool))))), 836 ^ _218455 : [(843 ^ _218455) ^ [] : [ti(_259027, _259025) = ti(_259027, _259019), ti(_259027, _259023) = ti(_259027, _259021)], (837 ^ _218455) ^ [] : [ti(_259027, _259025) = ti(_259027, _259021), ti(_259027, _259023) = ti(_259027, _259019)]]], (760 ^ _218455) ^ [_254118, _254120, _254122, _254124, _254126] : [hBOOL(hAPP(fun(_254124, bool), bool, hAPP(_254124, fun(fun(_254124, bool), bool), member(_254124), _254120), _254118)), -(hBOOL(hAPP(fun(_254126, bool), bool, hAPP(_254126, fun(fun(_254126, bool), bool), member(_254126), hAPP(_254124, _254126, _254122, _254120)), hAPP(fun(_254124, bool), fun(_254126, bool), hAPP(fun(_254124, _254126), fun(fun(_254124, bool), fun(_254126, bool)), image(_254124, _254126), _254122), _254118))))], (266 ^ _218455) ^ [] : [-(ti(fun(option(com), com), the(com)) = the(com))], (112 ^ _218455) ^ [_222403, _222405] : [_222405 = _222403, -(finite_finite(_222405) = finite_finite(_222403))], (1153 ^ _218455) ^ [_277400, _277402, _277404, _277406, _277408] : [hBOOL(hAPP(fun(_277406, bool), bool, finite_finite(_277406), _277400)), hBOOL(hAPP(fun(_277406, bool), bool, hAPP(fun(_277406, bool), fun(fun(_277406, bool), bool), ord_less_eq(fun(_277406, bool)), _277400), hAPP(fun(_277408, bool), fun(_277406, bool), hAPP(fun(_277408, _277406), fun(fun(_277408, bool), fun(_277406, bool)), image(_277408, _277406), _277404), _277402))), 1161 ^ _218455 : [(1166 ^ _218455) ^ [] : [-(ti(fun(_277406, bool), _277400) = hAPP(fun(_277408, bool), fun(_277406, bool), hAPP(fun(_277408, _277406), fun(fun(_277408, bool), fun(_277406, bool)), image(_277408, _277406), _277404), 1160 ^ [_277400, _277402, _277404, _277406, _277408]))], (1164 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(_277408, bool), bool, finite_finite(_277408), 1160 ^ [_277400, _277402, _277404, _277406, _277408])))], (1162 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(_277408, bool), bool, hAPP(fun(_277408, bool), fun(fun(_277408, bool), bool), ord_less_eq(fun(_277408, bool)), 1160 ^ [_277400, _277402, _277404, _277406, _277408]), _277402)))]]], (660 ^ _218455) ^ [_248419, _248421, _248423, _248425] : [-(hAPP(fun(_248425, bool), fun(_248425, bool), hAPP(_248425, fun(fun(_248425, bool), fun(_248425, bool)), insert(_248425), _248423), hAPP(fun(_248425, bool), fun(_248425, bool), hAPP(_248425, fun(fun(_248425, bool), fun(_248425, bool)), insert(_248425), _248421), _248419)) = hAPP(fun(_248425, bool), fun(_248425, bool), hAPP(_248425, fun(fun(_248425, bool), fun(_248425, bool)), insert(_248425), _248421), hAPP(fun(_248425, bool), fun(_248425, bool), hAPP(_248425, fun(fun(_248425, bool), fun(_248425, bool)), insert(_248425), _248423), _248419)))], (1300 ^ _218455) ^ [_283586, _283588] : [hBOOL(hAPP(bool, bool, hAPP(bool, fun(bool, bool), fimplies, _283588), _283586)), hBOOL(_283588), -(hBOOL(_283586))], (1057 ^ _218455) ^ [_272111, _272113, _272115] : [hBOOL(hAPP(_272115, bool, _272113, _272111)), -(hAPP(fun(_272115, bool), fun(_272115, bool), collect(_272115), hAPP(fun(_272115, bool), fun(_272115, bool), hAPP(fun(_272115, fun(bool, bool)), fun(fun(_272115, bool), fun(_272115, bool)), combs(_272115, bool, bool), hAPP(fun(_272115, bool), fun(_272115, fun(bool, bool)), hAPP(fun(bool, fun(bool, bool)), fun(fun(_272115, bool), fun(_272115, fun(bool, bool))), combb(bool, fun(bool, bool), _272115), fconj), hAPP(_272115, fun(_272115, bool), fequal(_272115), _272111))), _272113)) = hAPP(fun(_272115, bool), fun(_272115, bool), hAPP(_272115, fun(fun(_272115, bool), fun(_272115, bool)), insert(_272115), _272111), bot_bot(fun(_272115, bool))))], (188 ^ _218455) ^ [_225163, _225165] : [_225165 = _225163, -(insert(_225165) = insert(_225163))], (278 ^ _218455) ^ [] : [-(ti(bool, fFalse) = fFalse)], (52 ^ _218455) ^ [_220273, _220275, _220277, _220279, _220281, _220283] : [-(combc(_220283, _220279, _220275) = combc(_220281, _220277, _220273)), _220283 = _220281, _220279 = _220277, _220275 = _220273], (1170 ^ _218455) ^ [_278433, _278435] : [hAPP(pname, com, body_1, _278435) = hAPP(pname, com, body_1, _278433), -(ti(pname, _278435) = ti(pname, _278433))], (240 ^ _218455) ^ [_227276, _227278] : [-(ti(fun(_227278, fun(_227276, _227278)), combk(_227278, _227276)) = combk(_227278, _227276))], (488 ^ _218455) ^ [_240202, _240204, _240206] : [hBOOL(hAPP(fun(_240206, bool), bool, hAPP(fun(_240206, bool), fun(fun(_240206, bool), bool), ord_less_eq(fun(_240206, bool)), _240204), _240202)), hBOOL(hAPP(fun(_240206, bool), bool, hAPP(fun(_240206, bool), fun(fun(_240206, bool), bool), ord_less_eq(fun(_240206, bool)), _240202), _240204)), -(ti(fun(_240206, bool), _240204) = ti(fun(_240206, bool), _240202))], (1100 ^ _218455) ^ [_274305, _274307, _274309, _274311, _274313] : [hBOOL(hAPP(fun(_274313, bool), bool, hAPP(_274313, fun(fun(_274313, bool), bool), member(_274313), _274309), hAPP(fun(_274311, bool), fun(_274313, bool), hAPP(fun(_274311, _274313), fun(fun(_274311, bool), fun(_274313, bool)), image(_274311, _274313), _274307), _274305))), 1104 ^ _218455 : [(1107 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(_274311, bool), bool, hAPP(_274311, fun(fun(_274311, bool), bool), member(_274311), 1103 ^ [_274305, _274307, _274309, _274311, _274313]), _274305)))], (1105 ^ _218455) ^ [] : [-(ti(_274313, _274309) = hAPP(_274311, _274313, _274307, 1103 ^ [_274305, _274307, _274309, _274311, _274313]))]]], (592 ^ _218455) ^ [_245081, _245083, _245085] : [hBOOL(hAPP(fun(_245085, bool), bool, hAPP(_245085, fun(fun(_245085, bool), bool), member(_245085), _245083), _245081)), -(hAPP(fun(_245085, bool), fun(_245085, bool), hAPP(_245085, fun(fun(_245085, bool), fun(_245085, bool)), insert(_245085), _245083), _245081) = ti(fun(_245085, bool), _245081))], (1222 ^ _218455) ^ [_280612, _280614, _280616, _280618, _280620, _280622] : [-(hAPP(_280622, _280620, hAPP(fun(_280622, _280618), fun(_280622, _280620), hAPP(fun(_280622, fun(_280618, _280620)), fun(fun(_280622, _280618), fun(_280622, _280620)), combs(_280622, _280618, _280620), _280616), _280614), _280612) = hAPP(_280618, _280620, hAPP(_280622, fun(_280618, _280620), _280616, _280612), hAPP(_280622, _280618, _280614, _280612)))], (805 ^ _218455) ^ [_257073, _257075] : [-(hAPP(fun(_257075, bool), fun(_257075, bool), hAPP(fun(_257075, _257075), fun(fun(_257075, bool), fun(_257075, bool)), image(_257075, _257075), combi(_257075)), _257073) = ti(fun(_257075, bool), _257073))], (524 ^ _218455) ^ [_241993, _241995] : [hAPP(fun(_241995, bool), fun(_241995, bool), collect(_241995), _241993) = bot_bot(fun(_241995, bool)), 527 ^ _218455 : [(528 ^ _218455) ^ [_242150] : [hBOOL(hAPP(_241995, bool, _241993, _242150))]]], (238 ^ _218455) ^ [_227174] : [-(ti(fun(_227174, _227174), combi(_227174)) = combi(_227174))], (1029 ^ _218455) ^ [_270067, _270069, _270071, _270073, _270075] : [-(hBOOL(hAPP(fun(_270075, bool), bool, hAPP(fun(_270075, bool), fun(fun(_270075, bool), bool), ord_less_eq(fun(_270075, bool)), _270071), hAPP(fun(_270073, bool), fun(_270075, bool), hAPP(fun(_270073, _270075), fun(fun(_270073, bool), fun(_270075, bool)), image(_270073, _270075), _270069), _270067)))), 1030 ^ _218455 : [(1031 ^ _218455) ^ [_270285] : [hBOOL(hAPP(fun(_270073, bool), bool, hAPP(fun(_270073, bool), fun(fun(_270073, bool), bool), ord_less_eq(fun(_270073, bool)), _270285), _270067)), ti(fun(_270075, bool), _270071) = hAPP(fun(_270073, bool), fun(_270075, bool), hAPP(fun(_270073, _270075), fun(fun(_270073, bool), fun(_270075, bool)), image(_270073, _270075), _270069), _270285)]]], (634 ^ _218455) ^ [_247099, _247101, _247103, _247105] : [635 ^ _218455 : [(638 ^ _218455) ^ [] : [hBOOL(hAPP(_247105, bool, _247101, _247099))], (636 ^ _218455) ^ [] : [ti(_247105, _247103) = ti(_247105, _247099)]], -(hBOOL(hAPP(_247105, bool, hAPP(fun(_247105, bool), fun(_247105, bool), hAPP(_247105, fun(fun(_247105, bool), fun(_247105, bool)), insert(_247105), _247103), _247101), _247099)))], (172 ^ _218455) ^ [_224586, _224588] : [_224588 = _224586, -(option(_224588) = option(_224586))], (136 ^ _218455) ^ [_223275, _223277] : [_223277 = _223275, -(some(_223277) = some(_223275))], (248 ^ _218455) ^ [] : [-(ti(fun(pname, option(com)), body) = body)], (1073 ^ _218455) ^ [_273245, _273247] : [hBOOL(hoare_1883395792gleton), 1079 ^ _218455 : [(1082 ^ _218455) ^ [] : [hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), hoare_122391849derivs(state), _273245), hAPP(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool), hAPP(hoare_509422987triple(state), fun(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool)), insert(hoare_509422987triple(state)), hAPP(com, hoare_509422987triple(state), hoare_Mirabelle_MGT, hAPP(pname, com, body_1, 1078 ^ [_273245, _273247]))), bot_bot(fun(hoare_509422987triple(state), bool)))))], (1080 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(pname, bool), bool, hAPP(pname, fun(fun(pname, bool), bool), member(pname), 1078 ^ [_273245, _273247]), hAPP(fun(pname, option(com)), fun(pname, bool), dom(pname, com), body))))]], hBOOL(hAPP(com, bool, wt, _273247)), -(hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), hoare_122391849derivs(state), _273245), hAPP(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool), hAPP(hoare_509422987triple(state), fun(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool)), insert(hoare_509422987triple(state)), hAPP(com, hoare_509422987triple(state), hoare_Mirabelle_MGT, _273247)), bot_bot(fun(hoare_509422987triple(state), bool))))))], (666 ^ _218455) ^ [_249114, _249116, _249118] : [-(hAPP(fun(_249118, bool), fun(_249118, bool), hAPP(_249118, fun(fun(_249118, bool), fun(_249118, bool)), insert(_249118), _249116), _249114) = hAPP(fun(_249118, bool), fun(_249118, bool), collect(_249118), hAPP(fun(_249118, bool), fun(_249118, bool), hAPP(fun(_249118, fun(bool, bool)), fun(fun(_249118, bool), fun(_249118, bool)), combs(_249118, bool, bool), hAPP(fun(_249118, bool), fun(_249118, fun(bool, bool)), hAPP(fun(bool, fun(bool, bool)), fun(fun(_249118, bool), fun(_249118, fun(bool, bool))), combb(bool, fun(bool, bool), _249118), fdisj), hAPP(_249118, fun(_249118, bool), hAPP(fun(_249118, fun(_249118, bool)), fun(_249118, fun(_249118, bool)), combc(_249118, _249118, bool), fequal(_249118)), _249116))), hAPP(fun(_249118, bool), fun(_249118, bool), hAPP(fun(_249118, fun(fun(_249118, bool), bool)), fun(fun(_249118, bool), fun(_249118, bool)), combc(_249118, fun(_249118, bool), bool), member(_249118)), _249114))))], (738 ^ _218455) ^ [_252964, _252966, _252968] : [-(ti(fun(_252968, bool), _252966) = ti(fun(_252968, bool), _252964)), hBOOL(hAPP(fun(_252968, bool), bool, hAPP(fun(_252968, bool), fun(fun(_252968, bool), bool), ord_less_eq(fun(_252968, bool)), _252966), _252964)), hBOOL(hAPP(fun(_252968, bool), bool, hAPP(fun(_252968, bool), fun(fun(_252968, bool), bool), ord_less_eq(fun(_252968, bool)), _252964), _252966))], (539 ^ _218455) ^ [_242691, _242693] : [bot_bot(fun(_242693, bool)) = hAPP(fun(_242693, bool), fun(_242693, bool), collect(_242693), _242691), 542 ^ _218455 : [(543 ^ _218455) ^ [_242848] : [hBOOL(hAPP(_242693, bool, _242691, _242848))]]], (292 ^ _218455) ^ [_229319, _229321, _229323, _229325] : [-(hAPP(_229325, _229323, ti(fun(_229325, _229323), _229321), _229319) = hAPP(_229325, _229323, _229321, _229319))], (392 ^ _218455) ^ [_234920, _234922] : [-(hBOOL(hAPP(fun(_234922, bool), bool, hAPP(fun(_234922, bool), fun(fun(_234922, bool), bool), ord_less_eq(fun(_234922, bool)), bot_bot(fun(_234922, bool))), _234920)))], (678 ^ _218455) ^ [_250024, _250026, _250028, _250030] : [hBOOL(hAPP(fun(_250030, bool), bool, hAPP(fun(_250030, bool), fun(fun(_250030, bool), bool), ord_less_eq(fun(_250030, bool)), _250026), _250024)), hBOOL(hAPP(fun(_250030, bool), bool, hAPP(fun(_250030, bool), fun(fun(_250030, bool), bool), ord_less_eq(fun(_250030, bool)), _250024), _250028)), -(hBOOL(hAPP(fun(_250030, bool), bool, hAPP(fun(_250030, bool), fun(fun(_250030, bool), bool), ord_less_eq(fun(_250030, bool)), _250026), _250028)))], (40 ^ _218455) ^ [_219781, _219783] : [_219783 = _219781, -(undefined(_219783) = undefined(_219781))], (604 ^ _218455) ^ [_245815, _245817, _245819, _245821] : [-(hBOOL(hAPP(fun(_245821, bool), bool, hAPP(_245821, fun(fun(_245821, bool), bool), member(_245821), _245817), _245815))), -(hBOOL(hAPP(fun(_245821, bool), bool, hAPP(_245821, fun(fun(_245821, bool), bool), member(_245821), _245817), _245819))), 611 ^ _218455 : [(618 ^ _218455) ^ [] : [ti(fun(_245821, bool), _245815) = ti(fun(_245821, bool), _245819), -(hAPP(fun(_245821, bool), fun(_245821, bool), hAPP(_245821, fun(fun(_245821, bool), fun(_245821, bool)), insert(_245821), _245817), _245815) = hAPP(fun(_245821, bool), fun(_245821, bool), hAPP(_245821, fun(fun(_245821, bool), fun(_245821, bool)), insert(_245821), _245817), _245819))], (612 ^ _218455) ^ [] : [hAPP(fun(_245821, bool), fun(_245821, bool), hAPP(_245821, fun(fun(_245821, bool), fun(_245821, bool)), insert(_245821), _245817), _245815) = hAPP(fun(_245821, bool), fun(_245821, bool), hAPP(_245821, fun(fun(_245821, bool), fun(_245821, bool)), insert(_245821), _245817), _245819), -(ti(fun(_245821, bool), _245815) = ti(fun(_245821, bool), _245819))]]], (897 ^ _218455) ^ [_262263, _262265, _262267, _262269] : [ti(fun(_262269, bool), _262263) = bot_bot(fun(_262269, bool)), -(hAPP(fun(_262269, bool), fun(_262267, bool), hAPP(fun(_262269, _262267), fun(fun(_262269, bool), fun(_262267, bool)), image(_262269, _262267), _262265), _262263) = bot_bot(fun(_262267, bool)))], (891 ^ _218455) ^ [_261995, _261997, _261999, _262001] : [hAPP(fun(_262001, bool), fun(_261999, bool), hAPP(fun(_262001, _261999), fun(fun(_262001, bool), fun(_261999, bool)), image(_262001, _261999), _261997), _261995) = bot_bot(fun(_261999, bool)), -(ti(fun(_262001, bool), _261995) = bot_bot(fun(_262001, bool)))], (194 ^ _218455) ^ [_225465, _225467, _225469, _225471, _225473, _225475, _225477, _225479] : [-(hAPP(_225479, _225475, _225471, _225467) = hAPP(_225477, _225473, _225469, _225465)), _225479 = _225477, _225475 = _225473, _225471 = _225469, _225467 = _225465], (652 ^ _218455) ^ [_247958, _247960, _247962, _247964] : [653 ^ _218455 : [(656 ^ _218455) ^ [] : [hBOOL(hAPP(fun(_247964, bool), bool, hAPP(_247964, fun(fun(_247964, bool), bool), member(_247964), _247962), _247958))], (654 ^ _218455) ^ [] : [ti(_247964, _247962) = ti(_247964, _247960)]], -(hBOOL(hAPP(fun(_247964, bool), bool, hAPP(_247964, fun(fun(_247964, bool), bool), member(_247964), _247962), hAPP(fun(_247964, bool), fun(_247964, bool), hAPP(_247964, fun(fun(_247964, bool), fun(_247964, bool)), insert(_247964), _247960), _247958))))], (366 ^ _218455) ^ [_233148, _233150, _233152, _233154] : [hBOOL(hAPP(fun(hoare_509422987triple(_233154), bool), bool, hAPP(fun(hoare_509422987triple(_233154), bool), fun(fun(hoare_509422987triple(_233154), bool), bool), hoare_122391849derivs(_233154), _233152), hAPP(fun(hoare_509422987triple(_233154), bool), fun(hoare_509422987triple(_233154), bool), hAPP(hoare_509422987triple(_233154), fun(fun(hoare_509422987triple(_233154), bool), fun(hoare_509422987triple(_233154), bool)), insert(hoare_509422987triple(_233154)), _233150), _233148))), 369 ^ _218455 : [(372 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(hoare_509422987triple(_233154), bool), bool, hAPP(fun(hoare_509422987triple(_233154), bool), fun(fun(hoare_509422987triple(_233154), bool), bool), hoare_122391849derivs(_233154), _233152), _233148)))], (370 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(hoare_509422987triple(_233154), bool), bool, hAPP(fun(hoare_509422987triple(_233154), bool), fun(fun(hoare_509422987triple(_233154), bool), bool), hoare_122391849derivs(_233154), _233152), hAPP(fun(hoare_509422987triple(_233154), bool), fun(hoare_509422987triple(_233154), bool), hAPP(hoare_509422987triple(_233154), fun(fun(hoare_509422987triple(_233154), bool), fun(hoare_509422987triple(_233154), bool)), insert(hoare_509422987triple(_233154)), _233150), bot_bot(fun(hoare_509422987triple(_233154), bool))))))]]], (290 ^ _218455) ^ [] : [-(ti(fun(bool, fun(bool, bool)), fimplies) = fimplies)], (750 ^ _218455) ^ [_253579, _253581, _253583, _253585, _253587, _253589] : [hBOOL(hAPP(fun(_253587, bool), bool, hAPP(_253587, fun(fun(_253587, bool), bool), member(_253587), _253581), _253579)), ti(_253589, _253585) = hAPP(_253587, _253589, _253583, _253581), -(hBOOL(hAPP(fun(_253589, bool), bool, hAPP(_253589, fun(fun(_253589, bool), bool), member(_253589), _253585), hAPP(fun(_253587, bool), fun(_253589, bool), hAPP(fun(_253587, _253589), fun(fun(_253587, bool), fun(_253589, bool)), image(_253587, _253589), _253583), _253579))))], (730 ^ _218455) ^ [_252591, _252593, _252595] : [ti(fun(_252595, bool), _252593) = ti(fun(_252595, bool), _252591), 733 ^ _218455 : [(736 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(_252595, bool), bool, hAPP(fun(_252595, bool), fun(fun(_252595, bool), bool), ord_less_eq(fun(_252595, bool)), _252591), _252593)))], (734 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(_252595, bool), bool, hAPP(fun(_252595, bool), fun(fun(_252595, bool), bool), ord_less_eq(fun(_252595, bool)), _252593), _252591)))]]], (642 ^ _218455) ^ [_247540, _247542, _247544, _247546] : [hBOOL(hAPP(fun(_247546, bool), bool, hAPP(_247546, fun(fun(_247546, bool), bool), member(_247546), _247544), hAPP(fun(_247546, bool), fun(_247546, bool), hAPP(_247546, fun(fun(_247546, bool), fun(_247546, bool)), insert(_247546), _247542), _247540))), -(ti(_247546, _247544) = ti(_247546, _247542)), -(hBOOL(hAPP(fun(_247546, bool), bool, hAPP(_247546, fun(fun(_247546, bool), bool), member(_247546), _247544), _247540)))], (20 ^ _218455) ^ [_219203, _219205] : [-(finite_finite_1(_219203)), _219205 = _219203, finite_finite_1(_219205)], (158 ^ _218455) ^ [_224126, _224128, _224130, _224132, _224134, _224136] : [-(combb(_224136, _224132, _224128) = combb(_224134, _224130, _224126)), _224136 = _224134, _224132 = _224130, _224128 = _224126], (1063 ^ _218455) ^ [_272519, _272521, _272523] : [-(hBOOL(hAPP(_272523, bool, _272521, _272519))), -(hAPP(fun(_272523, bool), fun(_272523, bool), collect(_272523), hAPP(fun(_272523, bool), fun(_272523, bool), hAPP(fun(_272523, fun(bool, bool)), fun(fun(_272523, bool), fun(_272523, bool)), combs(_272523, bool, bool), hAPP(fun(_272523, bool), fun(_272523, fun(bool, bool)), hAPP(fun(bool, fun(bool, bool)), fun(fun(_272523, bool), fun(_272523, fun(bool, bool))), combb(bool, fun(bool, bool), _272523), fconj), hAPP(_272523, fun(_272523, bool), fequal(_272523), _272519))), _272521)) = bot_bot(fun(_272523, bool)))], (454 ^ _218455) ^ [_238690] : [hBOOL(hoare_1883395792gleton), hBOOL(wT_bodies), hBOOL(hAPP(com, bool, wt, _238690)), -(hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), hoare_122391849derivs(state), bot_bot(fun(hoare_509422987triple(state), bool))), hAPP(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool), hAPP(hoare_509422987triple(state), fun(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool)), insert(hoare_509422987triple(state)), hAPP(com, hoare_509422987triple(state), hoare_Mirabelle_MGT, _238690)), bot_bot(fun(hoare_509422987triple(state), bool))))))], (964 ^ _218455) ^ [_265709, _265711, _265713, _265715] : [hBOOL(hAPP(fun(_265715, bool), bool, hAPP(fun(_265715, bool), fun(fun(_265715, bool), bool), ord_less_eq(fun(_265715, bool)), _265711), _265709)), -(hBOOL(hAPP(fun(_265715, bool), bool, hAPP(fun(_265715, bool), fun(fun(_265715, bool), bool), ord_less_eq(fun(_265715, bool)), _265711), hAPP(fun(_265715, bool), fun(_265715, bool), hAPP(_265715, fun(fun(_265715, bool), fun(_265715, bool)), insert(_265715), _265713), _265709))))], (288 ^ _218455) ^ [_229133] : [-(ti(fun(_229133, fun(_229133, bool)), fequal(_229133)) = fequal(_229133))], (879 ^ _218455) ^ [_261396, _261398] : [hBOOL(hAPP(fun(_261398, bool), bool, hAPP(fun(_261398, bool), fun(fun(_261398, bool), bool), ord_less_eq(fun(_261398, bool)), _261396), bot_bot(fun(_261398, bool)))), -(ti(fun(_261398, bool), _261396) = bot_bot(fun(_261398, bool)))], (1314 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, finite_finite(hoare_509422987triple(state)), fa)))], (1109 ^ _218455) ^ [_274928, _274930, _274932, _274934] : [hBOOL(hAPP(fun(_274934, bool), bool, finite_finite(_274934), _274928)), hBOOL(hAPP(fun(_274934, bool), bool, hAPP(fun(_274934, bool), fun(fun(_274934, bool), bool), ord_less_eq(fun(_274934, bool)), _274928), _274930)), hBOOL(hAPP(fun(_274934, bool), bool, _274932, bot_bot(fun(_274934, bool)))), 1124 ^ _218455 : [(1125 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(_274934, bool), bool, finite_finite(_274934), 1123 ^ [_274928, _274930, _274932, _274934])))], (1129 ^ _218455) ^ [] : [hBOOL(hAPP(fun(_274934, bool), bool, hAPP(_274934, fun(fun(_274934, bool), bool), member(_274934), 1122 ^ [_274928, _274930, _274932, _274934]), 1123 ^ [_274928, _274930, _274932, _274934]))], (1133 ^ _218455) ^ [] : [hBOOL(hAPP(fun(_274934, bool), bool, _274932, hAPP(fun(_274934, bool), fun(_274934, bool), hAPP(_274934, fun(fun(_274934, bool), fun(_274934, bool)), insert(_274934), 1122 ^ [_274928, _274930, _274932, _274934]), 1123 ^ [_274928, _274930, _274932, _274934])))], (1131 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(_274934, bool), bool, _274932, 1123 ^ [_274928, _274930, _274932, _274934])))], (1127 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(_274934, bool), bool, hAPP(_274934, fun(fun(_274934, bool), bool), member(_274934), 1122 ^ [_274928, _274930, _274932, _274934]), _274930)))]], -(hBOOL(hAPP(fun(_274934, bool), bool, _274932, _274928)))], (1020 ^ _218455) ^ [_269409, _269411, _269413, _269415, _269417] : [hBOOL(hAPP(fun(_269417, bool), bool, hAPP(fun(_269417, bool), fun(fun(_269417, bool), bool), ord_less_eq(fun(_269417, bool)), _269413), hAPP(fun(_269415, bool), fun(_269417, bool), hAPP(fun(_269415, _269417), fun(fun(_269415, bool), fun(_269417, bool)), image(_269415, _269417), _269411), _269409))), 1024 ^ _218455 : [(1027 ^ _218455) ^ [] : [-(ti(fun(_269417, bool), _269413) = hAPP(fun(_269415, bool), fun(_269417, bool), hAPP(fun(_269415, _269417), fun(fun(_269415, bool), fun(_269417, bool)), image(_269415, _269417), _269411), 1023 ^ [_269409, _269411, _269413, _269415, _269417]))], (1025 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(_269415, bool), bool, hAPP(fun(_269415, bool), fun(fun(_269415, bool), bool), ord_less_eq(fun(_269415, bool)), 1023 ^ [_269409, _269411, _269413, _269415, _269417]), _269409)))]]], (670 ^ _218455) ^ [_249571, _249573, _249575] : [ti(fun(_249575, bool), _249573) = ti(fun(_249575, bool), _249571), 673 ^ _218455 : [(676 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(_249575, bool), bool, hAPP(fun(_249575, bool), fun(fun(_249575, bool), bool), ord_less_eq(fun(_249575, bool)), _249571), _249573)))], (674 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(_249575, bool), bool, hAPP(fun(_249575, bool), fun(fun(_249575, bool), bool), ord_less_eq(fun(_249575, bool)), _249573), _249571)))]]], (903 ^ _218455) ^ [_262580, _262582, _262584] : [-(hAPP(fun(_262584, bool), fun(_262582, bool), hAPP(fun(_262584, _262582), fun(fun(_262584, bool), fun(_262582, bool)), image(_262584, _262582), _262580), bot_bot(fun(_262584, bool))) = bot_bot(fun(_262582, bool)))], (1320 ^ _218455) ^ [] : [-(hAPP(pname, option(com), body, pn) = hAPP(com, option(com), some(com), y))], (96 ^ _218455) ^ [_221854, _221856, _221858, _221860] : [-(ti(_221860, _221856) = ti(_221858, _221854)), _221860 = _221858, _221856 = _221854], (256 ^ _218455) ^ [] : [-(ti(fun(com, hoare_509422987triple(state)), hoare_Mirabelle_MGT) = hoare_Mirabelle_MGT)], (148 ^ _218455) ^ [_223739, _223741, _223743, _223745] : [-(image(_223745, _223741) = image(_223743, _223739)), _223745 = _223743, _223741 = _223739], (284 ^ _218455) ^ [] : [-(ti(fun(bool, fun(bool, bool)), fconj) = fconj)], (803 ^ _218455) ^ [_256802, _256804, _256806] : [-(hAPP(fun(_256806, bool), fun(_256806, bool), hAPP(_256806, fun(fun(_256806, bool), fun(_256806, bool)), insert(_256806), _256804), _256802) = hAPP(fun(_256806, bool), fun(_256806, bool), collect(_256806), hAPP(fun(_256806, bool), fun(_256806, bool), hAPP(fun(_256806, fun(bool, bool)), fun(fun(_256806, bool), fun(_256806, bool)), combs(_256806, bool, bool), hAPP(fun(_256806, bool), fun(_256806, fun(bool, bool)), hAPP(fun(bool, fun(bool, bool)), fun(fun(_256806, bool), fun(_256806, fun(bool, bool))), combb(bool, fun(bool, bool), _256806), fdisj), hAPP(_256806, fun(_256806, bool), hAPP(fun(_256806, fun(_256806, bool)), fun(_256806, fun(_256806, bool)), combc(_256806, _256806, bool), fequal(_256806)), _256804))), hAPP(fun(_256806, bool), fun(_256806, bool), hAPP(fun(_256806, fun(fun(_256806, bool), bool)), fun(fun(_256806, bool), fun(_256806, bool)), combc(_256806, fun(_256806, bool), bool), member(_256806)), _256802))))], (586 ^ _218455) ^ [_244825] : [finite_finite_1(_244825), 589 ^ _218455 : [(590 ^ _218455) ^ [_244944] : [-(hBOOL(hAPP(fun(_244825, bool), bool, finite_finite(_244825), _244944)))]]], (1294 ^ _218455) ^ [_283358, _283360] : [hBOOL(_283358), -(hBOOL(hAPP(bool, bool, hAPP(bool, fun(bool, bool), fimplies, _283360), _283358)))], (252 ^ _218455) ^ [_227722] : [-(ti(fun(fun(_227722, bool), bool), finite_finite(_227722)) = finite_finite(_227722))], (264 ^ _218455) ^ [_228219] : [-(ti(fun(_228219, option(_228219)), some(_228219)) = some(_228219))], (962 ^ _218455) ^ [_265553, _265555] : [-(hAPP(fun(_265555, bool), fun(_265555, bool), collect(_265555), _265553) = ti(fun(_265555, bool), _265553))], (873 ^ _218455) ^ [_261059, _261061, _261063] : [hBOOL(hAPP(fun(_261063, bool), bool, finite_finite(_261063), _261059)), -(hBOOL(hAPP(fun(_261063, bool), bool, finite_finite(_261063), hAPP(fun(_261063, bool), fun(_261063, bool), hAPP(_261063, fun(fun(_261063, bool), fun(_261063, bool)), insert(_261063), _261061), _261059))))], (956 ^ _218455) ^ [_265302, _265304, _265306] : [hBOOL(hAPP(_265306, bool, _265302, _265304)), -(hBOOL(hAPP(fun(_265306, bool), bool, hAPP(_265306, fun(fun(_265306, bool), bool), member(_265306), _265304), _265302)))], (178 ^ _218455) ^ [_224832, _224834, _224836, _224838] : [-(dom(_224838, _224834) = dom(_224836, _224832)), _224838 = _224836, _224834 = _224832], (262 ^ _218455) ^ [_228119, _228121] : [-(ti(fun(fun(_228121, option(_228119)), fun(_228121, bool)), dom(_228121, _228119)) = dom(_228121, _228119))], (1090 ^ _218455) ^ [_273942, _273944] : [hBOOL(wT_bodies), hAPP(pname, option(com), body, _273944) = hAPP(com, option(com), some(com), _273942), -(hBOOL(hAPP(com, bool, wt, _273942)))], (552 ^ _218455) ^ [_243271, _243273] : [553 ^ _218455 : [(554 ^ _218455) ^ [_243374] : [hBOOL(hAPP(fun(_243273, bool), bool, hAPP(_243273, fun(fun(_243273, bool), bool), member(_243273), _243374), _243271))]], ti(fun(_243273, bool), _243271) = bot_bot(fun(_243273, bool))], (1200 ^ _218455) ^ [_279398, _279400] : [-(ti(_279400, ti(_279400, _279398)) = ti(_279400, _279398))], (698 ^ _218455) ^ [_251006, _251008, _251010, _251012] : [hBOOL(hAPP(fun(_251012, bool), bool, hAPP(_251012, fun(fun(_251012, bool), bool), member(_251012), _251008), _251006)), hBOOL(hAPP(fun(_251012, bool), bool, hAPP(fun(_251012, bool), fun(fun(_251012, bool), bool), ord_less_eq(fun(_251012, bool)), _251006), _251010)), -(hBOOL(hAPP(fun(_251012, bool), bool, hAPP(_251012, fun(fun(_251012, bool), bool), member(_251012), _251008), _251010)))], (10 ^ _218455) ^ [_218890, _218892, _218894] : [-(_218894 = _218890), _218894 = _218892, _218892 = _218890], (1282 ^ _218455) ^ [_282873, _282875, _282877] : [ti(_282877, _282875) = ti(_282877, _282873), -(hBOOL(hAPP(_282877, bool, hAPP(_282877, fun(_282877, bool), fequal(_282877), _282875), _282873)))], (1276 ^ _218455) ^ [_282601, _282603, _282605] : [hBOOL(hAPP(_282605, bool, hAPP(_282605, fun(_282605, bool), fequal(_282605), _282603), _282601)), -(ti(_282605, _282603) = ti(_282605, _282601))], (668 ^ _218455) ^ [_249399, _249401, _249403] : [-(hBOOL(hAPP(fun(_249403, bool), bool, hAPP(_249403, fun(fun(_249403, bool), bool), member(_249403), _249401), hAPP(fun(_249403, bool), fun(_249403, bool), hAPP(_249403, fun(fun(_249403, bool), fun(_249403, bool)), insert(_249403), _249401), _249399))))], (260 ^ _218455) ^ [] : [-(ti(bool, hoare_1883395792gleton) = hoare_1883395792gleton)], (1252 ^ _218455) ^ [_281788, _281790] : [hBOOL(_281788), -(hBOOL(hAPP(bool, bool, hAPP(bool, fun(bool, bool), fdisj, _281790), _281788)))], (394 ^ _218455) ^ [_235074, _235076, _235078] : [hBOOL(hAPP(fun(_235078, bool), bool, finite_finite(_235078), _235074)), -(hBOOL(hAPP(fun(_235078, bool), bool, finite_finite(_235078), hAPP(fun(_235078, bool), fun(_235078, bool), hAPP(_235078, fun(fun(_235078, bool), fun(_235078, bool)), insert(_235078), _235076), _235074))))], (821 ^ _218455) ^ [_258291, _258293, _258295, _258297, _258299] : [hAPP(fun(_258299, bool), fun(_258299, bool), hAPP(_258299, fun(fun(_258299, bool), fun(_258299, bool)), insert(_258299), _258297), hAPP(fun(_258299, bool), fun(_258299, bool), hAPP(_258299, fun(fun(_258299, bool), fun(_258299, bool)), insert(_258299), _258295), bot_bot(fun(_258299, bool)))) = hAPP(fun(_258299, bool), fun(_258299, bool), hAPP(_258299, fun(fun(_258299, bool), fun(_258299, bool)), insert(_258299), _258293), hAPP(fun(_258299, bool), fun(_258299, bool), hAPP(_258299, fun(fun(_258299, bool), fun(_258299, bool)), insert(_258299), _258291), bot_bot(fun(_258299, bool)))), 826 ^ _218455 : [(829 ^ _218455) ^ [] : [-(ti(_258299, _258295) = ti(_258299, _258291))], (827 ^ _218455) ^ [] : [-(ti(_258299, _258297) = ti(_258299, _258293))]], 830 ^ _218455 : [(833 ^ _218455) ^ [] : [-(ti(_258299, _258295) = ti(_258299, _258293))], (831 ^ _218455) ^ [] : [-(ti(_258299, _258297) = ti(_258299, _258291))]]], (276 ^ _218455) ^ [_228771] : [-(ti(fun(_228771, fun(fun(_228771, bool), fun(_228771, bool))), insert(_228771)) = insert(_228771))], (1268 ^ _218455) ^ [] : [hBOOL(fFalse)], (865 ^ _218455) ^ [_260615, _260617, _260619] : [bot_bot(fun(_260619, bool)) = hAPP(fun(_260619, bool), fun(_260619, bool), hAPP(_260619, fun(fun(_260619, bool), fun(_260619, bool)), insert(_260619), _260617), _260615)], (1224 ^ _218455) ^ [_280787, _280789] : [hBOOL(_280787), hBOOL(_280789), -(hBOOL(hAPP(bool, bool, hAPP(bool, fun(bool, bool), fconj, _280787), _280789)))], (1192 ^ _218455) ^ [] : [-(finite_finite_1(bool))], (724 ^ _218455) ^ [_252256, _252258, _252260] : [ti(fun(_252260, bool), _252258) = ti(fun(_252260, bool), _252256), -(hBOOL(hAPP(fun(_252260, bool), bool, hAPP(fun(_252260, bool), fun(fun(_252260, bool), bool), ord_less_eq(fun(_252260, bool)), _252258), _252256)))], (851 ^ _218455) ^ [_259858, _259860, _259862] : [hBOOL(hAPP(fun(_259862, bool), bool, hAPP(_259862, fun(fun(_259862, bool), bool), member(_259862), _259860), hAPP(fun(_259862, bool), fun(_259862, bool), hAPP(_259862, fun(fun(_259862, bool), fun(_259862, bool)), insert(_259862), _259858), bot_bot(fun(_259862, bool))))), -(ti(_259862, _259860) = ti(_259862, _259858))], (994 ^ _218455) ^ [_267397, _267399, _267401, _267403] : [-(hBOOL(hAPP(fun(_267403, bool), bool, hAPP(fun(_267403, bool), fun(fun(_267403, bool), bool), ord_less_eq(fun(_267403, bool)), hAPP(fun(_267403, bool), fun(_267403, bool), hAPP(_267403, fun(fun(_267403, bool), fun(_267403, bool)), insert(_267403), _267401), _267399)), _267397))), hBOOL(hAPP(fun(_267403, bool), bool, hAPP(_267403, fun(fun(_267403, bool), bool), member(_267403), _267401), _267397)), hBOOL(hAPP(fun(_267403, bool), bool, hAPP(fun(_267403, bool), fun(fun(_267403, bool), bool), ord_less_eq(fun(_267403, bool)), _267399), _267397))], (250 ^ _218455) ^ [] : [-(ti(fun(pname, com), body_1) = body_1)], (1045 ^ _218455) ^ [_271178, _271180, _271182] : [hBOOL(hAPP(_271182, bool, _271180, _271178)), -(hAPP(fun(_271182, bool), fun(_271182, bool), collect(_271182), hAPP(fun(_271182, bool), fun(_271182, bool), hAPP(fun(_271182, fun(bool, bool)), fun(fun(_271182, bool), fun(_271182, bool)), combs(_271182, bool, bool), hAPP(fun(_271182, bool), fun(_271182, fun(bool, bool)), hAPP(fun(bool, fun(bool, bool)), fun(fun(_271182, bool), fun(_271182, fun(bool, bool))), combb(bool, fun(bool, bool), _271182), fconj), hAPP(_271182, fun(_271182, bool), hAPP(fun(_271182, fun(_271182, bool)), fun(_271182, fun(_271182, bool)), combc(_271182, _271182, bool), fequal(_271182)), _271178))), _271180)) = hAPP(fun(_271182, bool), fun(_271182, bool), hAPP(_271182, fun(fun(_271182, bool), fun(_271182, bool)), insert(_271182), _271178), bot_bot(fun(_271182, bool))))], (1246 ^ _218455) ^ [_281560, _281562] : [hBOOL(_281560), -(hBOOL(hAPP(bool, bool, hAPP(bool, fun(bool, bool), fdisj, _281560), _281562)))], (374 ^ _218455) ^ [_233793, _233795] : [hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), hoare_122391849derivs(state), hAPP(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool), hAPP(hoare_509422987triple(state), fun(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool)), insert(hoare_509422987triple(state)), hAPP(com, hoare_509422987triple(state), hoare_Mirabelle_MGT, hAPP(pname, com, body_1, _233795))), _233793)), hAPP(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool), hAPP(hoare_509422987triple(state), fun(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool)), insert(hoare_509422987triple(state)), hAPP(com, hoare_509422987triple(state), hoare_Mirabelle_MGT, hAPP(option(com), com, the(com), hAPP(pname, option(com), body, _233795)))), bot_bot(fun(hoare_509422987triple(state), bool))))), -(hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), hoare_122391849derivs(state), _233793), hAPP(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool), hAPP(hoare_509422987triple(state), fun(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool)), insert(hoare_509422987triple(state)), hAPP(com, hoare_509422987triple(state), hoare_Mirabelle_MGT, hAPP(pname, com, body_1, _233795))), bot_bot(fun(hoare_509422987triple(state), bool))))))], (254 ^ _218455) ^ [_227813] : [-(ti(_227813, undefined(_227813)) = undefined(_227813))], (986 ^ _218455) ^ [_266946, _266948, _266950, _266952] : [hBOOL(hAPP(fun(_266952, bool), bool, hAPP(fun(_266952, bool), fun(fun(_266952, bool), bool), ord_less_eq(fun(_266952, bool)), hAPP(fun(_266952, bool), fun(_266952, bool), hAPP(_266952, fun(fun(_266952, bool), fun(_266952, bool)), insert(_266952), _266950), _266948)), _266946)), 989 ^ _218455 : [(992 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(_266952, bool), bool, hAPP(fun(_266952, bool), fun(fun(_266952, bool), bool), ord_less_eq(fun(_266952, bool)), _266948), _266946)))], (990 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(_266952, bool), bool, hAPP(_266952, fun(fun(_266952, bool), bool), member(_266952), _266950), _266946)))]]], (662 ^ _218455) ^ [_248639, _248641, _248643] : [-(hAPP(fun(_248643, bool), fun(_248643, bool), hAPP(_248643, fun(fun(_248643, bool), fun(_248643, bool)), insert(_248643), _248641), hAPP(fun(_248643, bool), fun(_248643, bool), hAPP(_248643, fun(fun(_248643, bool), fun(_248643, bool)), insert(_248643), _248641), _248639)) = hAPP(fun(_248643, bool), fun(_248643, bool), hAPP(_248643, fun(fun(_248643, bool), fun(_248643, bool)), insert(_248643), _248641), _248639))], (410 ^ _218455) ^ [_236080, _236082, _236084, _236086] : [ti(fun(_236084, bool), _236080) = bot_bot(fun(_236084, bool)), -(hAPP(fun(_236084, bool), fun(_236086, bool), hAPP(fun(_236084, _236086), fun(fun(_236084, bool), fun(_236086, bool)), image(_236084, _236086), hAPP(_236086, fun(_236084, _236086), combk(_236086, _236084), _236082)), _236080) = bot_bot(fun(_236086, bool)))], (228 ^ _218455) ^ [_226627, _226629] : [_226629 = _226627, -(hoare_509422987triple(_226629) = hoare_509422987triple(_226627))], (530 ^ _218455) ^ [_242222, _242224] : [-(hBOOL(hAPP(_242224, bool, _242222, 531 ^ [_242222, _242224]))), -(hAPP(fun(_242224, bool), fun(_242224, bool), collect(_242224), _242222) = bot_bot(fun(_242224, bool)))], (386 ^ _218455) ^ [_234615, _234617, _234619, _234621] : [hBOOL(hAPP(fun(_234619, bool), bool, finite_finite(_234619), _234615)), -(hBOOL(hAPP(fun(_234621, bool), bool, finite_finite(_234621), hAPP(fun(_234619, bool), fun(_234621, bool), hAPP(fun(_234619, _234621), fun(fun(_234619, bool), fun(_234621, bool)), image(_234619, _234621), _234617), _234615))))], (857 ^ _218455) ^ [_260142, _260144, _260146] : [ti(_260146, _260144) = ti(_260146, _260142), -(hBOOL(hAPP(fun(_260146, bool), bool, hAPP(_260146, fun(fun(_260146, bool), bool), member(_260146), _260144), hAPP(fun(_260146, bool), fun(_260146, bool), hAPP(_260146, fun(fun(_260146, bool), fun(_260146, bool)), insert(_260146), _260142), bot_bot(fun(_260146, bool))))))], (580 ^ _218455) ^ [_244597] : [finite_finite_1(_244597), 583 ^ _218455 : [(584 ^ _218455) ^ [_244716] : [-(hBOOL(hAPP(fun(_244597, bool), bool, finite_finite(_244597), _244716)))]]], (218 ^ _218455) ^ [_226316, _226318, _226320, _226322] : [-(fun(_226322, _226318) = fun(_226320, _226316)), _226322 = _226320, _226318 = _226316], (244 ^ _218455) ^ [] : [-(ti(fun(com, bool), wt) = wt)], (508 ^ _218455) ^ [_241174, _241176, _241178, _241180, _241182, _241184] : [ti(_241184, _241178) = hAPP(_241182, _241184, _241176, _241174), hBOOL(hAPP(fun(_241182, bool), bool, hAPP(_241182, fun(fun(_241182, bool), bool), member(_241182), _241174), _241180)), -(hBOOL(hAPP(fun(_241184, bool), bool, hAPP(_241184, fun(fun(_241184, bool), bool), member(_241184), _241178), hAPP(fun(_241182, bool), fun(_241184, bool), hAPP(fun(_241182, _241184), fun(fun(_241182, bool), fun(_241184, bool)), image(_241182, _241184), _241176), _241180))))], (766 ^ _218455) ^ [_254569, _254571, _254573, _254575, _254577] : [hBOOL(hAPP(fun(_254577, bool), bool, hAPP(_254577, fun(fun(_254577, bool), bool), member(_254577), _254573), hAPP(fun(_254575, bool), fun(_254577, bool), hAPP(fun(_254575, _254577), fun(fun(_254575, bool), fun(_254577, bool)), image(_254575, _254577), _254571), _254569))), 770 ^ _218455 : [(773 ^ _218455) ^ [] : [-(ti(_254577, _254573) = hAPP(_254575, _254577, _254571, 769 ^ [_254569, _254571, _254573, _254575, _254577]))], (771 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(_254575, bool), bool, hAPP(_254575, fun(fun(_254575, bool), bool), member(_254575), 769 ^ [_254569, _254571, _254573, _254575, _254577]), _254569)))]]], (1168 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(pname, bool), bool, finite_finite(pname), hAPP(fun(pname, option(com)), fun(pname, bool), dom(pname, com), body))))], (118 ^ _218455) ^ [_222621, _222623] : [_222623 = _222621, -(member(_222623) = member(_222621))], (316 ^ _218455) ^ [] : [-(ti(com, y) = y)], (444 ^ _218455) ^ [_238180, _238182, _238184] : [hBOOL(hAPP(fun(_238184, bool), bool, hAPP(fun(_238184, bool), fun(fun(_238184, bool), bool), ord_less_eq(fun(_238184, bool)), _238182), hAPP(fun(_238184, bool), fun(_238184, bool), hAPP(_238184, fun(fun(_238184, bool), fun(_238184, bool)), insert(_238184), _238180), bot_bot(fun(_238184, bool))))), -(ti(fun(_238184, bool), _238182) = bot_bot(fun(_238184, bool))), -(ti(fun(_238184, bool), _238182) = hAPP(fun(_238184, bool), fun(_238184, bool), hAPP(_238184, fun(fun(_238184, bool), fun(_238184, bool)), insert(_238184), _238180), bot_bot(fun(_238184, bool))))], (416 ^ _218455) ^ [_236370, _236372, _236374, _236376] : [-(ti(fun(_236374, bool), _236370) = bot_bot(fun(_236374, bool))), -(hAPP(fun(_236374, bool), fun(_236376, bool), hAPP(fun(_236374, _236376), fun(fun(_236374, bool), fun(_236376, bool)), image(_236374, _236376), hAPP(_236376, fun(_236374, _236376), combk(_236376, _236374), _236372)), _236370) = hAPP(fun(_236376, bool), fun(_236376, bool), hAPP(_236376, fun(fun(_236376, bool), fun(_236376, bool)), insert(_236376), _236372), bot_bot(fun(_236376, bool))))], (572 ^ _218455) ^ [_244207, _244209] : [ti(fun(_244209, bool), _244207) = bot_bot(fun(_244209, bool)), 575 ^ _218455 : [(576 ^ _218455) ^ [_244366] : [hBOOL(hAPP(fun(_244209, bool), bool, hAPP(_244209, fun(fun(_244209, bool), bool), member(_244209), _244366), _244207))]]], (927 ^ _218455) ^ [_263800, _263802, _263804] : [hBOOL(hAPP(fun(_263804, bool), bool, finite_finite(_263804), _263800)), hBOOL(hAPP(fun(_263804, bool), bool, hAPP(fun(_263804, bool), fun(fun(_263804, bool), bool), ord_less_eq(fun(_263804, bool)), _263802), _263800)), -(hBOOL(hAPP(fun(_263804, bool), bool, finite_finite(_263804), _263802)))], (1220 ^ _218455) ^ [_280439, _280441, _280443, _280445] : [-(hAPP(_280445, _280443, hAPP(_280443, fun(_280445, _280443), combk(_280443, _280445), _280441), _280439) = ti(_280443, _280441))], (66 ^ _218455) ^ [_220733, _220735] : [_220735 = _220733, -(combi(_220735) = combi(_220733))], (1270 ^ _218455) ^ [_282370] : [-(ti(bool, _282370) = fTrue), -(ti(bool, _282370) = fFalse)], (258 ^ _218455) ^ [_227951] : [-(ti(fun(fun(hoare_509422987triple(_227951), bool), fun(fun(hoare_509422987triple(_227951), bool), bool)), hoare_122391849derivs(_227951)) = hoare_122391849derivs(_227951))], (310 ^ _218455) ^ [_230078] : [-(ti(fun(_230078, fun(fun(_230078, bool), bool)), member(_230078)) = member(_230078))], (298 ^ _218455) ^ [_229741] : [hBOOL(ti(bool, _229741)), -(hBOOL(_229741))], (468 ^ _218455) ^ [_239082, _239084] : [hBOOL(hAPP(fun(_239084, bool), bool, hAPP(_239084, fun(fun(_239084, bool), bool), member(_239084), _239082), bot_bot(fun(_239084, bool))))], (807 ^ _218455) ^ [_257262, _257264, _257266, _257268, _257270, _257272] : [-(hAPP(fun(_257272, bool), fun(_257270, bool), hAPP(fun(_257272, _257270), fun(fun(_257272, bool), fun(_257270, bool)), image(_257272, _257270), _257266), hAPP(fun(_257268, bool), fun(_257272, bool), hAPP(fun(_257268, _257272), fun(fun(_257268, bool), fun(_257272, bool)), image(_257268, _257272), _257264), _257262)) = hAPP(fun(_257268, bool), fun(_257270, bool), hAPP(fun(_257268, _257270), fun(fun(_257268, bool), fun(_257270, bool)), image(_257268, _257270), hAPP(fun(_257268, _257272), fun(_257268, _257270), hAPP(fun(_257272, _257270), fun(fun(_257268, _257272), fun(_257268, _257270)), combb(_257272, _257270, _257268), _257266), _257264)), _257262))], (1006 ^ _218455) ^ [_268121, _268123, _268125, _268127, _268129] : [hBOOL(hAPP(fun(_268127, bool), bool, hAPP(_268127, fun(fun(_268127, bool), bool), member(_268127), _268123), _268121)), -(hAPP(fun(_268129, bool), fun(_268129, bool), hAPP(_268129, fun(fun(_268129, bool), fun(_268129, bool)), insert(_268129), hAPP(_268127, _268129, _268125, _268123)), hAPP(fun(_268127, bool), fun(_268129, bool), hAPP(fun(_268127, _268129), fun(fun(_268127, bool), fun(_268129, bool)), image(_268127, _268129), _268125), _268121)) = hAPP(fun(_268127, bool), fun(_268129, bool), hAPP(fun(_268127, _268129), fun(fun(_268127, bool), fun(_268129, bool)), image(_268127, _268129), _268125), _268121))], (246 ^ _218455) ^ [] : [-(ti(bool, wT_bodies) = wT_bodies)], (1318 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), ord_less_eq(fun(hoare_509422987triple(state), bool)), fa), hAPP(fun(pname, bool), fun(hoare_509422987triple(state), bool), hAPP(fun(pname, hoare_509422987triple(state)), fun(fun(pname, bool), fun(hoare_509422987triple(state), bool)), image(pname, hoare_509422987triple(state)), hAPP(fun(pname, com), fun(pname, hoare_509422987triple(state)), hAPP(fun(com, hoare_509422987triple(state)), fun(fun(pname, com), fun(pname, hoare_509422987triple(state))), combb(com, hoare_509422987triple(state), pname), hoare_Mirabelle_MGT), hAPP(fun(pname, option(com)), fun(pname, com), hAPP(fun(option(com), com), fun(fun(pname, option(com)), fun(pname, com)), combb(option(com), com, pname), the(com)), body))), hAPP(fun(pname, option(com)), fun(pname, bool), dom(pname, com), body)))))], (1288 ^ _218455) ^ [_283131, _283133] : [-(hBOOL(_283131)), -(hBOOL(hAPP(bool, bool, hAPP(bool, fun(bool, bool), fimplies, _283131), _283133)))], (1258 ^ _218455) ^ [_282016, _282018] : [hBOOL(hAPP(bool, bool, hAPP(bool, fun(bool, bool), fdisj, _282018), _282016)), -(hBOOL(_282018)), -(hBOOL(_282016))], (72 ^ _218455) ^ [_220979, _220981, _220983, _220985] : [-(combk(_220985, _220981) = combk(_220983, _220979)), _220985 = _220983, _220981 = _220979], (106 ^ _218455) ^ [_222185, _222187] : [_222187 = _222185, -(fequal(_222187) = fequal(_222185))], (578 ^ _218455) ^ [_244475] : [-(bot_bot(fun(_244475, bool)) = hAPP(fun(_244475, bool), fun(_244475, bool), collect(_244475), hAPP(bool, fun(_244475, bool), combk(bool, _244475), fFalse)))], (748 ^ _218455) ^ [_253388, _253390] : [-(hBOOL(hAPP(fun(_253390, bool), bool, hAPP(fun(_253390, bool), fun(fun(_253390, bool), bool), ord_less_eq(fun(_253390, bool)), _253388), _253388)))], (518 ^ _218455) ^ [_241685, _241687, _241689] : [ti(fun(_241689, bool), _241685) = bot_bot(fun(_241689, bool)), hBOOL(hAPP(fun(_241689, bool), bool, hAPP(_241689, fun(fun(_241689, bool), bool), member(_241689), _241687), _241685))], (242 ^ _218455) ^ [_227399, _227401, _227403] : [-(ti(fun(fun(_227403, fun(_227401, _227399)), fun(fun(_227403, _227401), fun(_227403, _227399))), combs(_227403, _227401, _227399)) = combs(_227403, _227401, _227399))], (809 ^ _218455) ^ [_257518, _257520, _257522] : [hAPP(fun(_257522, bool), fun(_257522, bool), hAPP(_257522, fun(fun(_257522, bool), fun(_257522, bool)), insert(_257522), _257520), bot_bot(fun(_257522, bool))) = hAPP(fun(_257522, bool), fun(_257522, bool), hAPP(_257522, fun(fun(_257522, bool), fun(_257522, bool)), insert(_257522), _257518), bot_bot(fun(_257522, bool))), -(ti(_257522, _257520) = ti(_257522, _257518))], (4 ^ _218455) ^ [_218686, _218688] : [_218688 = _218686, -(_218686 = _218688)], (565 ^ _218455) ^ [_243901, _243903] : [-(hBOOL(hAPP(fun(_243903, bool), bool, hAPP(_243903, fun(fun(_243903, bool), bool), member(_243903), 566 ^ [_243901, _243903]), _243901))), -(ti(fun(_243903, bool), _243901) = bot_bot(fun(_243903, bool)))], (142 ^ _218455) ^ [_223493, _223495] : [_223495 = _223493, -(hoare_122391849derivs(_223495) = hoare_122391849derivs(_223493))], (708 ^ _218455) ^ [_251485, _251487, _251489, _251491] : [hBOOL(hAPP(fun(_251491, bool), bool, hAPP(fun(_251491, bool), fun(fun(_251491, bool), bool), ord_less_eq(fun(_251491, bool)), _251487), _251485)), hBOOL(hAPP(fun(_251491, bool), bool, hAPP(_251491, fun(fun(_251491, bool), bool), member(_251491), _251489), _251487)), -(hBOOL(hAPP(fun(_251491, bool), bool, hAPP(_251491, fun(fun(_251491, bool), bool), member(_251491), _251489), _251485)))], (1004 ^ _218455) ^ [_267915, _267917, _267919] : [-(hBOOL(hAPP(fun(_267919, bool), bool, hAPP(fun(_267919, bool), fun(fun(_267919, bool), bool), ord_less_eq(fun(_267919, bool)), _267917), hAPP(fun(_267919, bool), fun(_267919, bool), hAPP(_267919, fun(fun(_267919, bool), fun(_267919, bool)), insert(_267919), _267915), _267917))))], (598 ^ _218455) ^ [_245431, _245433, _245435, _245437] : [hBOOL(hAPP(fun(_245437, bool), bool, hAPP(_245437, fun(fun(_245437, bool), bool), member(_245437), _245433), _245431)), -(hBOOL(hAPP(fun(_245437, bool), bool, hAPP(_245437, fun(fun(_245437, bool), bool), member(_245437), _245433), hAPP(fun(_245437, bool), fun(_245437, bool), hAPP(_245437, fun(fun(_245437, bool), fun(_245437, bool)), insert(_245437), _245435), _245431))))], (815 ^ _218455) ^ [_257888, _257890, _257892] : [hBOOL(hAPP(fun(_257892, bool), bool, hAPP(_257892, fun(fun(_257892, bool), bool), member(_257892), _257890), hAPP(fun(_257892, bool), fun(_257892, bool), hAPP(_257892, fun(fun(_257892, bool), fun(_257892, bool)), insert(_257892), _257888), bot_bot(fun(_257892, bool))))), -(ti(_257892, _257890) = ti(_257892, _257888))], (1208 ^ _218455) ^ [_279701] : [-(hBOOL(_279701)), -(hBOOL(hAPP(bool, bool, fNot, _279701)))], (1071 ^ _218455) ^ [_273081, _273083] : [-(hAPP(fun(_273083, bool), fun(_273083, bool), collect(_273083), hAPP(_273083, fun(_273083, bool), fequal(_273083), _273081)) = hAPP(fun(_273083, bool), fun(_273083, bool), hAPP(_273083, fun(fun(_273083, bool), fun(_273083, bool)), insert(_273083), _273081), bot_bot(fun(_273083, bool))))], (1051 ^ _218455) ^ [_271628, _271630, _271632] : [-(hBOOL(hAPP(_271632, bool, _271630, _271628))), -(hAPP(fun(_271632, bool), fun(_271632, bool), collect(_271632), hAPP(fun(_271632, bool), fun(_271632, bool), hAPP(fun(_271632, fun(bool, bool)), fun(fun(_271632, bool), fun(_271632, bool)), combs(_271632, bool, bool), hAPP(fun(_271632, bool), fun(_271632, fun(bool, bool)), hAPP(fun(bool, fun(bool, bool)), fun(fun(_271632, bool), fun(_271632, fun(bool, bool))), combb(bool, fun(bool, bool), _271632), fconj), hAPP(_271632, fun(_271632, bool), hAPP(fun(_271632, fun(_271632, bool)), fun(_271632, fun(_271632, bool)), combc(_271632, _271632, bool), fequal(_271632)), _271628))), _271630)) = bot_bot(fun(_271632, bool)))], (318 ^ _218455) ^ [_230345, _230347] : [-(hBOOL(hAPP(fun(hoare_509422987triple(_230347), bool), bool, hAPP(fun(hoare_509422987triple(_230347), bool), fun(fun(hoare_509422987triple(_230347), bool), bool), hoare_122391849derivs(_230347), _230345), bot_bot(fun(hoare_509422987triple(_230347), bool)))))], (905 ^ _218455) ^ [_262789, _262791, _262793, _262795] : [bot_bot(fun(_262795, bool)) = hAPP(fun(_262793, bool), fun(_262795, bool), hAPP(fun(_262793, _262795), fun(fun(_262793, bool), fun(_262795, bool)), image(_262793, _262795), _262791), _262789), -(ti(fun(_262793, bool), _262789) = bot_bot(fun(_262793, bool)))], (478 ^ _218455) ^ [_239720, _239722, _239724, _239726] : [hBOOL(hAPP(fun(_239726, bool), bool, hAPP(_239726, fun(fun(_239726, bool), bool), member(_239726), _239724), hAPP(fun(_239726, bool), fun(_239726, bool), hAPP(_239726, fun(fun(_239726, bool), fun(_239726, bool)), insert(_239726), _239722), _239720))), -(ti(_239726, _239724) = ti(_239726, _239722)), -(hBOOL(hAPP(fun(_239726, bool), bool, hAPP(_239726, fun(fun(_239726, bool), bool), member(_239726), _239724), _239720)))], (775 ^ _218455) ^ [_255110, _255112, _255114, _255116, _255118] : [-(hBOOL(hAPP(fun(_255118, bool), bool, hAPP(_255118, fun(fun(_255118, bool), bool), member(_255118), _255114), hAPP(fun(_255116, bool), fun(_255118, bool), hAPP(fun(_255116, _255118), fun(fun(_255116, bool), fun(_255118, bool)), image(_255116, _255118), _255112), _255110)))), 776 ^ _218455 : [(777 ^ _218455) ^ [_255287] : [hBOOL(hAPP(fun(_255116, bool), bool, hAPP(_255116, fun(fun(_255116, bool), bool), member(_255116), _255287), _255110)), ti(_255118, _255114) = hAPP(_255116, _255118, _255112, _255287)]]], (1234 ^ _218455) ^ [_281104, _281106] : [hBOOL(hAPP(bool, bool, hAPP(bool, fun(bool, bool), fconj, _281106), _281104)), -(hBOOL(_281106))], (688 ^ _218455) ^ [_250527, _250529, _250531, _250533] : [hBOOL(hAPP(fun(_250533, bool), bool, hAPP(fun(_250533, bool), fun(fun(_250533, bool), bool), ord_less_eq(fun(_250533, bool)), _250529), _250527)), hBOOL(hAPP(fun(_250533, bool), bool, hAPP(_250533, fun(fun(_250533, bool), bool), member(_250533), _250531), _250529)), -(hBOOL(hAPP(fun(_250533, bool), bool, hAPP(_250533, fun(fun(_250533, bool), bool), member(_250533), _250531), _250527)))], (30 ^ _218455) ^ [_219478, _219480] : [-(hBOOL(_219478)), _219480 = _219478, hBOOL(_219480)], (124 ^ _218455) ^ [_222839, _222841] : [_222841 = _222839, -(ord_less_eq(_222841) = ord_less_eq(_222839))], (1012 ^ _218455) ^ [_268604, _268606, _268608, _268610, _268612] : [-(hAPP(fun(_268612, bool), fun(_268610, bool), hAPP(fun(_268612, _268610), fun(fun(_268612, bool), fun(_268610, bool)), image(_268612, _268610), _268608), hAPP(fun(_268612, bool), fun(_268612, bool), hAPP(_268612, fun(fun(_268612, bool), fun(_268612, bool)), insert(_268612), _268606), _268604)) = hAPP(fun(_268610, bool), fun(_268610, bool), hAPP(_268610, fun(fun(_268610, bool), fun(_268610, bool)), insert(_268610), hAPP(_268612, _268610, _268608, _268606)), hAPP(fun(_268612, bool), fun(_268610, bool), hAPP(fun(_268612, _268610), fun(fun(_268612, bool), fun(_268610, bool)), image(_268612, _268610), _268608), _268604)))], (624 ^ _218455) ^ [_246745, _246747, _246749, _246751] : [hBOOL(hAPP(_246751, bool, hAPP(fun(_246751, bool), fun(_246751, bool), hAPP(_246751, fun(fun(_246751, bool), fun(_246751, bool)), insert(_246751), _246749), _246747), _246745)), -(ti(_246751, _246749) = ti(_246751, _246745)), -(hBOOL(hAPP(_246751, bool, _246747, _246745)))], (234 ^ _218455) ^ [_226930, _226932, _226934] : [-(ti(fun(fun(_226934, _226932), fun(fun(_226930, _226934), fun(_226930, _226932))), combb(_226934, _226932, _226930)) = combb(_226934, _226932, _226930))], (380 ^ _218455) ^ [_234169, _234171] : [hBOOL(hAPP(fun(_234171, bool), bool, finite_finite(_234171), _234169)), -(hBOOL(hAPP(fun(fun(_234171, bool), bool), bool, finite_finite(fun(_234171, bool)), hAPP(fun(fun(_234171, bool), bool), fun(fun(_234171, bool), bool), collect(fun(_234171, bool)), hAPP(fun(_234171, bool), fun(fun(_234171, bool), bool), hAPP(fun(fun(_234171, bool), fun(fun(_234171, bool), bool)), fun(fun(_234171, bool), fun(fun(_234171, bool), bool)), combc(fun(_234171, bool), fun(_234171, bool), bool), ord_less_eq(fun(_234171, bool))), _234169)))))], (950 ^ _218455) ^ [_265086, _265088, _265090] : [hBOOL(hAPP(fun(_265090, bool), bool, hAPP(_265090, fun(fun(_265090, bool), bool), member(_265090), _265088), _265086)), -(hBOOL(hAPP(_265090, bool, _265086, _265088)))], (356 ^ _218455) ^ [_232457, _232459, _232461, _232463] : [hBOOL(hAPP(fun(hoare_509422987triple(_232463), bool), bool, hAPP(fun(hoare_509422987triple(_232463), bool), fun(fun(hoare_509422987triple(_232463), bool), bool), hoare_122391849derivs(_232463), _232459), hAPP(fun(hoare_509422987triple(_232463), bool), fun(hoare_509422987triple(_232463), bool), hAPP(hoare_509422987triple(_232463), fun(fun(hoare_509422987triple(_232463), bool), fun(hoare_509422987triple(_232463), bool)), insert(hoare_509422987triple(_232463)), _232457), bot_bot(fun(hoare_509422987triple(_232463), bool))))), hBOOL(hAPP(fun(hoare_509422987triple(_232463), bool), bool, hAPP(fun(hoare_509422987triple(_232463), bool), fun(fun(hoare_509422987triple(_232463), bool), bool), hoare_122391849derivs(_232463), _232459), _232461)), -(hBOOL(hAPP(fun(hoare_509422987triple(_232463), bool), bool, hAPP(fun(hoare_509422987triple(_232463), bool), fun(fun(hoare_509422987triple(_232463), bool), bool), hoare_122391849derivs(_232463), _232459), hAPP(fun(hoare_509422987triple(_232463), bool), fun(hoare_509422987triple(_232463), bool), hAPP(hoare_509422987triple(_232463), fun(fun(hoare_509422987triple(_232463), bool), fun(hoare_509422987triple(_232463), bool)), insert(hoare_509422987triple(_232463)), _232457), _232461))))], (885 ^ _218455) ^ [_261642, _261644] : [ti(fun(_261644, bool), _261642) = bot_bot(fun(_261644, bool)), -(hBOOL(hAPP(fun(_261644, bool), bool, hAPP(fun(_261644, bool), fun(fun(_261644, bool), bool), ord_less_eq(fun(_261644, bool)), _261642), bot_bot(fun(_261644, bool)))))], (718 ^ _218455) ^ [_251950, _251952, _251954] : [ti(fun(_251954, bool), _251952) = ti(fun(_251954, bool), _251950), -(hBOOL(hAPP(fun(_251954, bool), bool, hAPP(fun(_251954, bool), fun(fun(_251954, bool), bool), ord_less_eq(fun(_251954, bool)), _251950), _251952)))], (1137 ^ _218455) ^ [_276492] : [hBOOL(hAPP(com, bool, wt, hAPP(pname, com, body_1, _276492))), -(hAPP(pname, option(com), body, _276492) = hAPP(com, option(com), some(com), 1140 ^ [_276492]))], (867 ^ _218455) ^ [_260801, _260803, _260805] : [hBOOL(hAPP(fun(_260805, bool), bool, finite_finite(_260805), hAPP(fun(_260805, bool), fun(_260805, bool), hAPP(_260805, fun(fun(_260805, bool), fun(_260805, bool)), insert(_260805), _260803), _260801))), -(hBOOL(hAPP(fun(_260805, bool), bool, finite_finite(_260805), _260801)))], (422 ^ _218455) ^ [_236809, _236811, _236813, _236815, _236817] : [hBOOL(hAPP(fun(_236815, bool), bool, hAPP(_236815, fun(fun(_236815, bool), bool), member(_236815), _236811), _236809)), -(hAPP(fun(_236815, bool), fun(_236817, bool), hAPP(fun(_236815, _236817), fun(fun(_236815, bool), fun(_236817, bool)), image(_236815, _236817), hAPP(_236817, fun(_236815, _236817), combk(_236817, _236815), _236813)), _236809) = hAPP(fun(_236817, bool), fun(_236817, bool), hAPP(_236817, fun(fun(_236817, bool), fun(_236817, bool)), insert(_236817), _236813), bot_bot(fun(_236817, bool))))], (336 ^ _218455) ^ [_231405, _231407, _231409, _231411] : [hBOOL(hAPP(fun(hoare_509422987triple(_231411), bool), bool, hAPP(fun(hoare_509422987triple(_231411), bool), fun(fun(hoare_509422987triple(_231411), bool), bool), hoare_122391849derivs(_231411), _231407), _231405)), hBOOL(hAPP(fun(hoare_509422987triple(_231411), bool), bool, hAPP(fun(hoare_509422987triple(_231411), bool), fun(fun(hoare_509422987triple(_231411), bool), bool), ord_less_eq(fun(hoare_509422987triple(_231411), bool)), _231407), _231409)), -(hBOOL(hAPP(fun(hoare_509422987triple(_231411), bool), bool, hAPP(fun(hoare_509422987triple(_231411), bool), fun(fun(hoare_509422987triple(_231411), bool), bool), hoare_122391849derivs(_231411), _231409), _231405)))], (130 ^ _218455) ^ [_223057, _223059] : [_223059 = _223057, -(the(_223059) = the(_223057))], (236 ^ _218455) ^ [_227066, _227068, _227070] : [-(ti(fun(fun(_227070, fun(_227068, _227066)), fun(_227068, fun(_227070, _227066))), combc(_227070, _227068, _227066)) = combc(_227070, _227068, _227066))], (537 ^ _218455) ^ [_242528, _242530] : [hBOOL(hAPP(fun(_242530, bool), bool, hAPP(_242530, fun(fun(_242530, bool), bool), member(_242530), _242528), bot_bot(fun(_242530, bool))))], (558 ^ _218455) ^ [_243518, _243520] : [-(ti(fun(_243520, bool), _243518) = bot_bot(fun(_243520, bool))), -(hBOOL(hAPP(fun(_243520, bool), bool, hAPP(_243520, fun(fun(_243520, bool), bool), member(_243520), 561 ^ [_243518, _243520]), _243518)))], (863 ^ _218455) ^ [_260474, _260476, _260478] : [hAPP(fun(_260478, bool), fun(_260478, bool), hAPP(_260478, fun(fun(_260478, bool), fun(_260478, bool)), insert(_260478), _260476), _260474) = bot_bot(fun(_260478, bool))], (280 ^ _218455) ^ [] : [-(ti(fun(bool, bool), fNot) = fNot)], (434 ^ _218455) ^ [_237687, _237689, _237691, _237693, _237695] : [hBOOL(hAPP(fun(_237693, bool), bool, finite_finite(_237693), _237687)), hBOOL(hAPP(fun(_237695, bool), bool, hAPP(fun(_237695, bool), fun(fun(_237695, bool), bool), ord_less_eq(fun(_237695, bool)), _237691), hAPP(fun(_237693, bool), fun(_237695, bool), hAPP(fun(_237693, _237695), fun(fun(_237693, bool), fun(_237695, bool)), image(_237693, _237695), _237689), _237687))), -(hBOOL(hAPP(fun(_237695, bool), bool, finite_finite(_237695), _237691)))], (545 ^ _218455) ^ [_242920, _242922] : [-(hBOOL(hAPP(_242922, bool, _242920, 546 ^ [_242920, _242922]))), -(bot_bot(fun(_242922, bool)) = hAPP(fun(_242922, bool), fun(_242922, bool), collect(_242922), _242920))], (1014 ^ _218455) ^ [_268882, _268884, _268886, _268888, _268890] : [hBOOL(hAPP(fun(_268888, bool), bool, hAPP(fun(_268888, bool), fun(fun(_268888, bool), bool), ord_less_eq(fun(_268888, bool)), _268884), _268882)), -(hBOOL(hAPP(fun(_268890, bool), bool, hAPP(fun(_268890, bool), fun(fun(_268890, bool), bool), ord_less_eq(fun(_268890, bool)), hAPP(fun(_268888, bool), fun(_268890, bool), hAPP(fun(_268888, _268890), fun(fun(_268888, bool), fun(_268890, bool)), image(_268888, _268890), _268886), _268884)), hAPP(fun(_268888, bool), fun(_268890, bool), hAPP(fun(_268888, _268890), fun(fun(_268888, bool), fun(_268890, bool)), image(_268888, _268890), _268886), _268882))))], (1216 ^ _218455) ^ [_280158, _280160, _280162, _280164, _280166, _280168] : [-(hAPP(_280168, _280166, hAPP(_280164, fun(_280168, _280166), hAPP(fun(_280168, fun(_280164, _280166)), fun(_280164, fun(_280168, _280166)), combc(_280168, _280164, _280166), _280162), _280160), _280158) = hAPP(_280164, _280166, hAPP(_280168, fun(_280164, _280166), _280162, _280158), _280160))], (1316 ^ _218455) ^ [] : [hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(hoare_509422987triple(state), fun(fun(hoare_509422987triple(state), bool), bool), member(hoare_509422987triple(state)), hAPP(com, hoare_509422987triple(state), hoare_Mirabelle_MGT, y)), fa))], (793 ^ _218455) ^ [_256238, _256240, _256242] : [-(hBOOL(hAPP(fun(_256242, bool), bool, finite_finite(_256242), hAPP(fun(_256242, bool), fun(_256242, bool), collect(_256242), hAPP(fun(_256242, bool), fun(_256242, bool), hAPP(fun(_256242, fun(bool, bool)), fun(fun(_256242, bool), fun(_256242, bool)), combs(_256242, bool, bool), hAPP(fun(_256242, bool), fun(_256242, fun(bool, bool)), hAPP(fun(bool, fun(bool, bool)), fun(fun(_256242, bool), fun(_256242, fun(bool, bool))), combb(bool, fun(bool, bool), _256242), fdisj), _256240)), _256238))))), hBOOL(hAPP(fun(_256242, bool), bool, finite_finite(_256242), hAPP(fun(_256242, bool), fun(_256242, bool), collect(_256242), _256240))), hBOOL(hAPP(fun(_256242, bool), bool, finite_finite(_256242), hAPP(fun(_256242, bool), fun(_256242, bool), collect(_256242), _256238)))], (1214 ^ _218455) ^ [_279953, _279955, _279957, _279959, _279961, _279963] : [-(hAPP(_279963, _279961, hAPP(fun(_279963, _279959), fun(_279963, _279961), hAPP(fun(_279959, _279961), fun(fun(_279963, _279959), fun(_279963, _279961)), combb(_279959, _279961, _279963), _279957), _279955), _279953) = hAPP(_279959, _279961, _279957, hAPP(_279963, _279959, _279955, _279953)))], (1144 ^ _218455) ^ [_276815, _276817, _276819] : [1146 ^ _218455 : [(1149 ^ _218455) ^ [] : [hBOOL(hAPP(fun(_276819, bool), bool, hAPP(_276819, fun(fun(_276819, bool), bool), member(_276819), 1145 ^ [_276815, _276817, _276819]), _276817))], (1147 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(_276819, bool), bool, hAPP(_276819, fun(fun(_276819, bool), bool), member(_276819), 1145 ^ [_276815, _276817, _276819]), _276815)))]], -(hBOOL(hAPP(fun(_276819, bool), bool, hAPP(fun(_276819, bool), fun(fun(_276819, bool), bool), ord_less_eq(fun(_276819, bool)), _276815), _276817)))], (270 ^ _218455) ^ [_228456] : [-(ti(fun(fun(_228456, bool), fun(fun(_228456, bool), bool)), ord_less_eq(fun(_228456, bool))) = ord_less_eq(fun(_228456, bool)))], (312 ^ _218455) ^ [] : [-(ti(fun(hoare_509422987triple(state), bool), fa) = fa)], (326 ^ _218455) ^ [_230874, _230876, _230878, _230880] : [hBOOL(hAPP(fun(hoare_509422987triple(_230880), bool), bool, hAPP(fun(hoare_509422987triple(_230880), bool), fun(fun(hoare_509422987triple(_230880), bool), bool), hoare_122391849derivs(_230880), _230876), _230874)), hBOOL(hAPP(fun(hoare_509422987triple(_230880), bool), bool, hAPP(fun(hoare_509422987triple(_230880), bool), fun(fun(hoare_509422987triple(_230880), bool), bool), ord_less_eq(fun(hoare_509422987triple(_230880), bool)), _230878), _230874)), -(hBOOL(hAPP(fun(hoare_509422987triple(_230880), bool), bool, hAPP(fun(hoare_509422987triple(_230880), bool), fun(fun(hoare_509422987triple(_230880), bool), bool), hoare_122391849derivs(_230880), _230876), _230878)))], (1218 ^ _218455) ^ [_280307, _280309] : [-(hAPP(_280309, _280309, combi(_280309), _280307) = ti(_280309, _280307))], (294 ^ _218455) ^ [_229461, _229463, _229465, _229467] : [-(hAPP(_229467, _229465, _229463, ti(_229467, _229461)) = hAPP(_229467, _229465, _229463, _229461))], (943 ^ _218455) ^ [_264687, _264689, _264691, _264693] : [hAPP(_264693, _264691, _264689, 944 ^ [_264687, _264689, _264691, _264693]) = hAPP(_264693, _264691, _264687, 944 ^ [_264687, _264689, _264691, _264693]), -(ti(fun(_264693, _264691), _264689) = ti(fun(_264693, _264691), _264687))], (785 ^ _218455) ^ [_255739, _255741, _255743] : [hBOOL(hAPP(fun(_255743, bool), bool, finite_finite(_255743), hAPP(fun(_255743, bool), fun(_255743, bool), collect(_255743), hAPP(fun(_255743, bool), fun(_255743, bool), hAPP(fun(_255743, fun(bool, bool)), fun(fun(_255743, bool), fun(_255743, bool)), combs(_255743, bool, bool), hAPP(fun(_255743, bool), fun(_255743, fun(bool, bool)), hAPP(fun(bool, fun(bool, bool)), fun(fun(_255743, bool), fun(_255743, fun(bool, bool))), combb(bool, fun(bool, bool), _255743), fdisj), _255741)), _255739)))), 788 ^ _218455 : [(791 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(_255743, bool), bool, finite_finite(_255743), hAPP(fun(_255743, bool), fun(_255743, bool), collect(_255743), _255739))))], (789 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(_255743, bool), bool, finite_finite(_255743), hAPP(fun(_255743, bool), fun(_255743, bool), collect(_255743), _255741))))]]], (1202 ^ _218455) ^ [_279502] : [hBOOL(hAPP(bool, bool, fNot, _279502)), hBOOL(_279502)], (400 ^ _218455) ^ [_235351] : [-(hBOOL(hAPP(fun(_235351, bool), bool, finite_finite(_235351), bot_bot(fun(_235351, bool)))))], (272 ^ _218455) ^ [_228559] : [-(ti(fun(fun(_228559, bool), fun(_228559, bool)), collect(_228559)) = collect(_228559))], (428 ^ _218455) ^ [_237267, _237269, _237271, _237273, _237275] : [hAPP(_237275, option(_237273), _237271, _237269) = hAPP(_237273, option(_237273), some(_237273), _237267), -(hAPP(fun(_237275, bool), fun(_237275, bool), hAPP(_237275, fun(fun(_237275, bool), fun(_237275, bool)), insert(_237275), _237269), hAPP(fun(_237275, option(_237273)), fun(_237275, bool), dom(_237275, _237273), _237271)) = hAPP(fun(_237275, option(_237273)), fun(_237275, bool), dom(_237275, _237273), _237271))], (470 ^ _218455) ^ [_239244, _239246, _239248, _239250] : [471 ^ _218455 : [(474 ^ _218455) ^ [] : [ti(_239250, _239246) = ti(_239250, _239248)], (472 ^ _218455) ^ [] : [hBOOL(hAPP(fun(_239250, bool), bool, hAPP(_239250, fun(fun(_239250, bool), bool), member(_239250), _239246), _239244))]], -(hBOOL(hAPP(fun(_239250, bool), bool, hAPP(_239250, fun(fun(_239250, bool), bool), member(_239250), _239246), hAPP(fun(_239250, bool), fun(_239250, bool), hAPP(_239250, fun(fun(_239250, bool), fun(_239250, bool)), insert(_239250), _239248), _239244))))], (282 ^ _218455) ^ [] : [-(ti(bool, fTrue) = fTrue)], (402 ^ _218455) ^ [_235486, _235488, _235490] : [403 ^ _218455 : [(406 ^ _218455) ^ [] : [hBOOL(hAPP(fun(_235490, bool), bool, finite_finite(_235490), hAPP(fun(_235490, bool), fun(_235490, bool), collect(_235490), _235488)))], (404 ^ _218455) ^ [] : [hBOOL(hAPP(fun(_235490, bool), bool, finite_finite(_235490), hAPP(fun(_235490, bool), fun(_235490, bool), collect(_235490), _235486)))]], -(hBOOL(hAPP(fun(_235490, bool), bool, finite_finite(_235490), hAPP(fun(_235490, bool), fun(_235490, bool), collect(_235490), hAPP(fun(_235490, bool), fun(_235490, bool), hAPP(fun(_235490, fun(bool, bool)), fun(fun(_235490, bool), fun(_235490, bool)), combs(_235490, bool, bool), hAPP(fun(_235490, bool), fun(_235490, fun(bool, bool)), hAPP(fun(bool, fun(bool, bool)), fun(fun(_235490, bool), fun(_235490, fun(bool, bool))), combb(bool, fun(bool, bool), _235490), fconj), _235486)), _235488)))))], (1322 ^ _218455) ^ [] : [-(hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), hoare_122391849derivs(state), hAPP(fun(pname, bool), fun(hoare_509422987triple(state), bool), hAPP(fun(pname, hoare_509422987triple(state)), fun(fun(pname, bool), fun(hoare_509422987triple(state), bool)), image(pname, hoare_509422987triple(state)), hAPP(fun(pname, com), fun(pname, hoare_509422987triple(state)), hAPP(fun(com, hoare_509422987triple(state)), fun(fun(pname, com), fun(pname, hoare_509422987triple(state))), combb(com, hoare_509422987triple(state), pname), hoare_Mirabelle_MGT), body_1)), hAPP(fun(pname, option(com)), fun(pname, bool), dom(pname, com), body))), fa)))], (917 ^ _218455) ^ [_263389, _263391, _263393] : [hBOOL(hAPP(fun(_263393, bool), bool, hAPP(fun(_263393, bool), fun(fun(_263393, bool), bool), ord_less_eq(fun(_263393, bool)), _263391), _263389)), hBOOL(hAPP(fun(_263393, bool), bool, finite_finite(_263393), _263389)), -(hBOOL(hAPP(fun(_263393, bool), bool, finite_finite(_263393), _263391)))], (314 ^ _218455) ^ [] : [-(ti(pname, pn) = pn)], (1194 ^ _218455) ^ [_279209] : [finite_finite_1(_279209), -(finite_finite_1(option(_279209)))], (2 ^ _218455) ^ [_218579] : [-(_218579 = _218579)], (498 ^ _218455) ^ [_240667, _240669, _240671, _240673] : [hBOOL(hAPP(fun(_240673, bool), bool, hAPP(fun(_240673, bool), fun(fun(_240673, bool), bool), ord_less_eq(fun(_240673, bool)), _240669), _240667)), hBOOL(hAPP(fun(_240673, bool), bool, hAPP(_240673, fun(fun(_240673, bool), bool), member(_240673), _240671), _240669)), -(hBOOL(hAPP(fun(_240673, bool), bool, hAPP(_240673, fun(fun(_240673, bool), bool), member(_240673), _240671), _240667)))], (82 ^ _218455) ^ [_221366, _221368, _221370, _221372, _221374, _221376] : [-(combs(_221376, _221372, _221368) = combs(_221374, _221370, _221366)), _221376 = _221374, _221372 = _221370, _221368 = _221366], (320 ^ _218455) ^ [_230504, _230506, _230508] : [hBOOL(hAPP(fun(hoare_509422987triple(_230508), bool), bool, hAPP(fun(hoare_509422987triple(_230508), bool), fun(fun(hoare_509422987triple(_230508), bool), bool), ord_less_eq(fun(hoare_509422987triple(_230508), bool)), _230506), _230504)), -(hBOOL(hAPP(fun(hoare_509422987triple(_230508), bool), bool, hAPP(fun(hoare_509422987triple(_230508), bool), fun(fun(hoare_509422987triple(_230508), bool), bool), hoare_122391849derivs(_230508), _230504), _230506)))], (1039 ^ _218455) ^ [_270812, _270814, _270816, _270818, _270820] : [hAPP(_270820, option(_270818), _270816, _270814) = hAPP(_270818, option(_270818), some(_270818), _270812), -(hBOOL(hAPP(fun(_270820, bool), bool, hAPP(_270820, fun(fun(_270820, bool), bool), member(_270820), _270814), hAPP(fun(_270820, option(_270818)), fun(_270820, bool), dom(_270820, _270818), _270816))))], (212 ^ _218455) ^ [_226070, _226072] : [_226072 = _226070, -(bot_bot(_226072) = bot_bot(_226070))], (46 ^ _218455) ^ [_219999, _220001] : [_220001 = _219999, -(collect(_220001) = collect(_219999))], (911 ^ _218455) ^ [_263057, _263059, _263061, _263063] : [ti(fun(_263061, bool), _263057) = bot_bot(fun(_263061, bool)), -(bot_bot(fun(_263063, bool)) = hAPP(fun(_263061, bool), fun(_263063, bool), hAPP(fun(_263061, _263063), fun(fun(_263061, bool), fun(_263063, bool)), image(_263061, _263063), _263059), _263057))], (274 ^ _218455) ^ [_228667, _228669] : [-(ti(fun(fun(_228669, _228667), fun(fun(_228669, bool), fun(_228667, bool))), image(_228669, _228667)) = image(_228669, _228667))]], input).
% 43.19/42.73  ncf('1',plain,[hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), hoare_122391849derivs(state), hAPP(fun(pname, bool), fun(hoare_509422987triple(state), bool), hAPP(fun(pname, hoare_509422987triple(state)), fun(fun(pname, bool), fun(hoare_509422987triple(state), bool)), image(pname, hoare_509422987triple(state)), hAPP(fun(pname, com), fun(pname, hoare_509422987triple(state)), hAPP(fun(com, hoare_509422987triple(state)), fun(fun(pname, com), fun(pname, hoare_509422987triple(state))), combb(com, hoare_509422987triple(state), pname), hoare_Mirabelle_MGT), body_1)), hAPP(fun(pname, option(com)), fun(pname, bool), dom(pname, com), body))), hAPP(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool), hAPP(hoare_509422987triple(state), fun(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool)), insert(hoare_509422987triple(state)), hAPP(com, hoare_509422987triple(state), hoare_Mirabelle_MGT, y)), bot_bot(fun(hoare_509422987triple(state), bool)))))],start(1324 ^ 0)).
% 43.19/42.73  ncf('1.1',plain,[-(hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), hoare_122391849derivs(state), hAPP(fun(pname, bool), fun(hoare_509422987triple(state), bool), hAPP(fun(pname, hoare_509422987triple(state)), fun(fun(pname, bool), fun(hoare_509422987triple(state), bool)), image(pname, hoare_509422987triple(state)), hAPP(fun(pname, com), fun(pname, hoare_509422987triple(state)), hAPP(fun(com, hoare_509422987triple(state)), fun(fun(pname, com), fun(pname, hoare_509422987triple(state))), combb(com, hoare_509422987triple(state), pname), hoare_Mirabelle_MGT), body_1)), hAPP(fun(pname, option(com)), fun(pname, bool), dom(pname, com), body))), hAPP(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool), hAPP(hoare_509422987triple(state), fun(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool)), insert(hoare_509422987triple(state)), hAPP(com, hoare_509422987triple(state), hoare_Mirabelle_MGT, y)), bot_bot(fun(hoare_509422987triple(state), bool)))))), hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), hoare_122391849derivs(state), bot_bot(fun(hoare_509422987triple(state), bool))), hAPP(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool), hAPP(hoare_509422987triple(state), fun(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool)), insert(hoare_509422987triple(state)), hAPP(com, hoare_509422987triple(state), hoare_Mirabelle_MGT, y)), bot_bot(fun(hoare_509422987triple(state), bool))))), hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), hoare_122391849derivs(state), hAPP(fun(pname, bool), fun(hoare_509422987triple(state), bool), hAPP(fun(pname, hoare_509422987triple(state)), fun(fun(pname, bool), fun(hoare_509422987triple(state), bool)), image(pname, hoare_509422987triple(state)), hAPP(fun(pname, com), fun(pname, hoare_509422987triple(state)), hAPP(fun(com, hoare_509422987triple(state)), fun(fun(pname, com), fun(pname, hoare_509422987triple(state))), combb(com, hoare_509422987triple(state), pname), hoare_Mirabelle_MGT), body_1)), hAPP(fun(pname, option(com)), fun(pname, bool), dom(pname, com), body))), bot_bot(fun(hoare_509422987triple(state), bool))))],extension(346 ^ 1,bind([[_231936, _231938, _231940, _231942], [hAPP(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool), hAPP(hoare_509422987triple(state), fun(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool)), insert(hoare_509422987triple(state)), hAPP(com, hoare_509422987triple(state), hoare_Mirabelle_MGT, y)), bot_bot(fun(hoare_509422987triple(state), bool))), bot_bot(fun(hoare_509422987triple(state), bool)), hAPP(fun(pname, bool), fun(hoare_509422987triple(state), bool), hAPP(fun(pname, hoare_509422987triple(state)), fun(fun(pname, bool), fun(hoare_509422987triple(state), bool)), image(pname, hoare_509422987triple(state)), hAPP(fun(pname, com), fun(pname, hoare_509422987triple(state)), hAPP(fun(com, hoare_509422987triple(state)), fun(fun(pname, com), fun(pname, hoare_509422987triple(state))), combb(com, hoare_509422987triple(state), pname), hoare_Mirabelle_MGT), body_1)), hAPP(fun(pname, option(com)), fun(pname, bool), dom(pname, com), body)), state]]))).
% 43.19/42.73  ncf('1.1.1',plain,[-(hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), hoare_122391849derivs(state), bot_bot(fun(hoare_509422987triple(state), bool))), hAPP(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool), hAPP(hoare_509422987triple(state), fun(fun(hoare_509422987triple(state), bool), fun(hoare_509422987triple(state), bool)), insert(hoare_509422987triple(state)), hAPP(com, hoare_509422987triple(state), hoare_Mirabelle_MGT, y)), bot_bot(fun(hoare_509422987triple(state), bool)))))), hBOOL(hoare_1883395792gleton), hBOOL(wT_bodies), hBOOL(hAPP(com, bool, wt, y))],extension(454 ^ 2,bind([[_238690], [y]]))).
% 43.19/42.73  ncf('1.1.1.1',plain,[-(hBOOL(hoare_1883395792gleton))],extension(1310 ^ 3)).
% 43.19/42.73  ncf('1.1.1.2',plain,[-(hBOOL(wT_bodies))],extension(1312 ^ 3)).
% 43.19/42.73  ncf('1.1.1.3',plain,[-(hBOOL(hAPP(com, bool, wt, y))), hBOOL(wT_bodies), hAPP(pname, option(com), body, pn) = hAPP(com, option(com), some(com), y)],extension(1090 ^ 3,bind([[_273942, _273944], [y, pn]]))).
% 43.19/42.73  ncf('1.1.1.3.1',plain,[-(hBOOL(wT_bodies))],lemmata('[1, 1].x')).
% 43.19/42.73  ncf('1.1.1.3.2',plain,[-(hAPP(pname, option(com), body, pn) = hAPP(com, option(com), some(com), y))],extension(1320 ^ 4)).
% 43.19/42.73  ncf('1.1.2',plain,[-(hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), hoare_122391849derivs(state), hAPP(fun(pname, bool), fun(hoare_509422987triple(state), bool), hAPP(fun(pname, hoare_509422987triple(state)), fun(fun(pname, bool), fun(hoare_509422987triple(state), bool)), image(pname, hoare_509422987triple(state)), hAPP(fun(pname, com), fun(pname, hoare_509422987triple(state)), hAPP(fun(com, hoare_509422987triple(state)), fun(fun(pname, com), fun(pname, hoare_509422987triple(state))), combb(com, hoare_509422987triple(state), pname), hoare_Mirabelle_MGT), body_1)), hAPP(fun(pname, option(com)), fun(pname, bool), dom(pname, com), body))), bot_bot(fun(hoare_509422987triple(state), bool))))), hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), hoare_122391849derivs(state), bot_bot(fun(hoare_509422987triple(state), bool))), bot_bot(fun(hoare_509422987triple(state), bool)))), hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), hoare_122391849derivs(state), hAPP(fun(pname, bool), fun(hoare_509422987triple(state), bool), hAPP(fun(pname, hoare_509422987triple(state)), fun(fun(pname, bool), fun(hoare_509422987triple(state), bool)), image(pname, hoare_509422987triple(state)), hAPP(fun(pname, com), fun(pname, hoare_509422987triple(state)), hAPP(fun(com, hoare_509422987triple(state)), fun(fun(pname, com), fun(pname, hoare_509422987triple(state))), combb(com, hoare_509422987triple(state), pname), hoare_Mirabelle_MGT), body_1)), hAPP(fun(pname, option(com)), fun(pname, bool), dom(pname, com), body))), bot_bot(fun(hoare_509422987triple(state), bool))))],extension(346 ^ 2,bind([[_231936, _231938, _231940, _231942], [bot_bot(fun(hoare_509422987triple(state), bool)), bot_bot(fun(hoare_509422987triple(state), bool)), hAPP(fun(pname, bool), fun(hoare_509422987triple(state), bool), hAPP(fun(pname, hoare_509422987triple(state)), fun(fun(pname, bool), fun(hoare_509422987triple(state), bool)), image(pname, hoare_509422987triple(state)), hAPP(fun(pname, com), fun(pname, hoare_509422987triple(state)), hAPP(fun(com, hoare_509422987triple(state)), fun(fun(pname, com), fun(pname, hoare_509422987triple(state))), combb(com, hoare_509422987triple(state), pname), hoare_Mirabelle_MGT), body_1)), hAPP(fun(pname, option(com)), fun(pname, bool), dom(pname, com), body)), state]]))).
% 43.19/42.73  ncf('1.1.2.1',plain,[-(hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), hoare_122391849derivs(state), bot_bot(fun(hoare_509422987triple(state), bool))), bot_bot(fun(hoare_509422987triple(state), bool)))))],extension(318 ^ 3,bind([[_230345, _230347], [bot_bot(fun(hoare_509422987triple(state), bool)), state]]))).
% 43.19/42.73  ncf('1.1.2.2',plain,[-(hBOOL(hAPP(fun(hoare_509422987triple(state), bool), bool, hAPP(fun(hoare_509422987triple(state), bool), fun(fun(hoare_509422987triple(state), bool), bool), hoare_122391849derivs(state), hAPP(fun(pname, bool), fun(hoare_509422987triple(state), bool), hAPP(fun(pname, hoare_509422987triple(state)), fun(fun(pname, bool), fun(hoare_509422987triple(state), bool)), image(pname, hoare_509422987triple(state)), hAPP(fun(pname, com), fun(pname, hoare_509422987triple(state)), hAPP(fun(com, hoare_509422987triple(state)), fun(fun(pname, com), fun(pname, hoare_509422987triple(state))), combb(com, hoare_509422987triple(state), pname), hoare_Mirabelle_MGT), body_1)), hAPP(fun(pname, option(com)), fun(pname, bool), dom(pname, com), body))), bot_bot(fun(hoare_509422987triple(state), bool)))))],extension(318 ^ 3,bind([[_230345, _230347], [hAPP(fun(pname, bool), fun(hoare_509422987triple(state), bool), hAPP(fun(pname, hoare_509422987triple(state)), fun(fun(pname, bool), fun(hoare_509422987triple(state), bool)), image(pname, hoare_509422987triple(state)), hAPP(fun(pname, com), fun(pname, hoare_509422987triple(state)), hAPP(fun(com, hoare_509422987triple(state)), fun(fun(pname, com), fun(pname, hoare_509422987triple(state))), combb(com, hoare_509422987triple(state), pname), hoare_Mirabelle_MGT), body_1)), hAPP(fun(pname, option(com)), fun(pname, bool), dom(pname, com), body)), state]]))).
% 43.19/42.73  %-----------------------------------------------------
% 43.19/42.73  End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------