%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWV893-1 : TPTP v8.1.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n004.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 : Wed Jul 27 13:21:44 EDT 2022 % Result : Unknown 47.84s 47.95s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV893-1 : TPTP v8.1.0. Released v4.1.0. % 0.03/0.13 % Command : otter-tptp-script %s % 0.13/0.34 % Computer : n004.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Jul 27 05:38:51 EDT 2022 % 0.13/0.35 % CPUTime : % 47.45/47.53 ----- Otter 3.3f, August 2004 ----- % 47.45/47.53 The process was started by sandbox2 on n004.cluster.edu, % 47.45/47.53 Wed Jul 27 05:38:51 2022 % 47.45/47.53 The command was "./otter". The process ID is 25012. % 47.45/47.53 % 47.45/47.53 set(prolog_style_variables). % 47.45/47.53 set(auto). % 47.45/47.53 dependent: set(auto1). % 47.45/47.53 dependent: set(process_input). % 47.45/47.53 dependent: clear(print_kept). % 47.45/47.53 dependent: clear(print_new_demod). % 47.45/47.53 dependent: clear(print_back_demod). % 47.45/47.53 dependent: clear(print_back_sub). % 47.45/47.53 dependent: set(control_memory). % 47.45/47.53 dependent: assign(max_mem, 12000). % 47.45/47.53 dependent: assign(pick_given_ratio, 4). % 47.45/47.53 dependent: assign(stats_level, 1). % 47.45/47.53 dependent: assign(max_seconds, 10800). % 47.45/47.53 clear(print_given). % 47.45/47.53 % 47.45/47.53 list(usable). % 47.45/47.53 0 [] A=A. % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(V_A,c_HOL_Ominus__class_Ominus(V_B,V_A,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))=V_B| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),V_C,tc_fun(T_a,tc_bool))| -c_lesse_quals(V_A,c_Lattices_Oupper__semilattice__class_Osup(V_B,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(V_A,c_Lattices_Oupper__semilattice__class_Osup(V_B,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))| -c_lesse_quals(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),V_C,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(c_HOL_Ominus__class_Ominus(c_Set_Oimage(V_f,V_A,T_b,T_a),c_Set_Oimage(V_f,V_B,T_b,T_a),tc_fun(T_a,tc_bool)),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_b,tc_bool)),T_b,T_a),tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_HOL_Ominus__class_Ominus(V_A,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,V_B,T_a),tc_fun(T_a,tc_bool))=c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,V_B,T_a),tc_fun(T_a,tc_bool))=c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Set_Oinsert(V_a,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a)=c_Set_Oinsert(V_a,V_A,T_a). % 47.45/47.53 0 [] c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,V_B,T_a),tc_fun(T_a,tc_bool)),T_a)| -c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a). % 47.45/47.53 0 [] c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)| -c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,V_B,T_a),tc_fun(T_a,tc_bool)),T_a). % 47.45/47.53 0 [] c_HOL_Ominus__class_Ominus(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool))=c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))| -c_in(V_x,V_B,T_a). % 47.45/47.53 0 [] c_HOL_Ominus__class_Ominus(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool))=c_Set_Oinsert(V_x,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)|c_in(V_x,V_B,T_a). % 47.45/47.53 0 [] -class_OrderedGroup_Opordered__ab__group__add(T_a)|c_HOL_Ominus__class_Ominus(V_x,V_y,T_a)!=c_HOL_Ominus__class_Ominus(V_x_H,V_y_H,T_a)|c_lesse_quals(V_y,V_x,T_a)| -c_lesse_quals(V_y_H,V_x_H,T_a). % 47.45/47.53 0 [] -class_OrderedGroup_Opordered__ab__group__add(T_a)|c_HOL_Ominus__class_Ominus(V_x,V_y,T_a)!=c_HOL_Ominus__class_Ominus(V_x_H,V_y_H,T_a)|c_lesse_quals(V_y_H,V_x_H,T_a)| -c_lesse_quals(V_y,V_x,T_a). % 47.45/47.53 0 [] c_HOL_Ominus__class_Ominus(V_B,c_HOL_Ominus__class_Ominus(V_C,V_A,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))=V_A| -c_lesse_quals(V_B,V_C,tc_fun(T_a,tc_bool))| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),c_HOL_Ominus__class_Ominus(V_C,V_D,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))| -c_lesse_quals(V_D,V_B,tc_fun(T_a,tc_bool))| -c_lesse_quals(V_A,V_C,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_HOL_Ominus__class_Ominus(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_HOL_Ominus__class_Ominus(V_A,V_A,tc_fun(T_a,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_HOL_Ominus__class_Ominus(V_A,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))=V_A. % 47.45/47.53 0 [] -c_in(V_c,V_B,T_a)| -c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a). % 47.45/47.53 0 [] c_in(V_c,V_A,T_a)| -c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a). % 47.45/47.53 0 [] c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)| -c_Finite__Set_Ofinite(V_A,T_a)| -c_Finite__Set_Ofinite(V_B,T_a). % 47.45/47.53 0 [] c_Finite__Set_Ofinite(V_A,T_a)| -c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)| -c_Finite__Set_Ofinite(V_B,T_a). % 47.45/47.53 0 [] c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)| -c_Finite__Set_Ofinite(V_A,T_a). % 47.45/47.53 0 [] c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool))=c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] -class_OrderedGroup_Oab__group__add(T_a)|c_HOL_Ominus__class_Ominus(V_xa,V_y,T_a)!=c_HOL_Ominus__class_Ominus(V_x,V_x,T_a)|V_xa=V_y. % 47.45/47.53 0 [] -class_OrderedGroup_Oab__group__add(T_a)|c_HOL_Ominus__class_Ominus(V_x,V_x,T_a)!=c_HOL_Ominus__class_Ominus(V_x_H,V_y_H,T_a)|V_x_H=V_y_H. % 47.45/47.53 0 [] c_lesse_quals(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Hoare__Mirabelle_Ohoare__valids(V_G,V_ts,T_a)| -c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a). % 47.45/47.53 0 [] c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)|c_in(V_c,V_B,T_a)| -c_in(V_c,V_A,T_a). % 47.45/47.53 0 [] c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)|c_in(V_c,V_B,T_a)| -c_in(V_c,V_A,T_a). % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(c_HOL_Ominus__class_Ominus(V_B,V_A,tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(V_B,V_A,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(V_A,c_HOL_Ominus__class_Ominus(V_B,V_A,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_HOL_Ominus__class_Ominus(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_C,tc_fun(T_a,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(c_HOL_Ominus__class_Ominus(V_A,V_C,tc_fun(T_a,tc_bool)),c_HOL_Ominus__class_Ominus(V_B,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Set_Oinsert(V_a,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a)=V_A| -c_in(V_a,V_A,T_a). % 47.45/47.53 0 [] c_HOL_Ominus__class_Ominus(c_Set_Oinsert(V_x,V_A,T_a),c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool))=V_A|c_in(V_x,V_A,T_a). % 47.45/47.53 0 [] c_lesse_quals(V_A,c_Set_Oinsert(V_x,V_B,T_a),tc_fun(T_a,tc_bool))| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool))| -c_lesse_quals(c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] hAPP(V_f,V_x)!=c_Option_Ooption_ONone(T_a)|c_HOL_Ominus__class_Ominus(c_Map_Odom(V_f,T_b,T_a),c_Set_Oinsert(V_x,V_A,T_b),tc_fun(T_b,tc_bool))=c_HOL_Ominus__class_Ominus(c_Map_Odom(V_f,T_b,T_a),V_A,tc_fun(T_b,tc_bool)). % 47.45/47.53 0 [] c_Com_Ocom_OCall(V_vname,V_pname,V_fun)!=c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H)|V_fun=V_fun_H. % 47.45/47.53 0 [] c_Com_Ocom_OCall(V_vname,V_pname,V_fun)!=c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H)|V_pname=V_pname_H. % 47.45/47.53 0 [] c_Com_Ocom_OCall(V_vname,V_pname,V_fun)!=c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H)|V_vname=V_vname_H. % 47.45/47.53 0 [] c_Com_Ocom_Ocom__rec(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,c_Com_Ocom_OSemi(V_com1,V_com2),T_a)=hAPP(hAPP(hAPP(hAPP(V_f4,V_com1),V_com2),c_Com_Ocom_Ocom__rec(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,V_com1,T_a)),c_Com_Ocom_Ocom__rec(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,V_com2,T_a)). % 47.45/47.53 0 [] c_Com_Ocom_OWhile(V_fun_H,V_com_H)!=c_Com_Ocom_OSKIP. % 47.45/47.53 0 [] c_Com_Ocom_OWhile(V_fun_H,V_com_H)!=c_Com_Ocom_OLocal(V_loc,V_fun,V_com). % 47.45/47.53 0 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OWhile(V_b,V_c)),V_s),V_s))|hBOOL(hAPP(V_b,V_s)). % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(V_a,V_B,T_a),V_C,tc_fun(T_a,tc_bool))=c_Set_Oinsert(V_a,c_Lattices_Oupper__semilattice__class_Osup(V_B,V_C,tc_fun(T_a,tc_bool)),T_a). % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(V_A,c_Set_Oinsert(V_a,V_B,T_a),tc_fun(T_a,tc_bool))=c_Set_Oinsert(V_a,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),T_a). % 47.45/47.53 0 [] c_lesse_quals(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] -class_Orderings_Obot(T_a)|c_lesse_quals(c_Orderings_Obot__class_Obot(T_a),V_x,T_a). % 47.45/47.53 0 [] c_Com_Ocom_OSemi(V_com1,V_com2)!=c_Com_Ocom_OSemi(V_com1_H,V_com2_H)|V_com2=V_com2_H. % 47.45/47.53 0 [] c_Com_Ocom_OSemi(V_com1,V_com2)!=c_Com_Ocom_OSemi(V_com1_H,V_com2_H)|V_com1=V_com1_H. % 47.45/47.53 0 [] c_Com_Ocom_OSemi(V_com1,V_com2)!=c_Com_Ocom_OWhile(V_fun_H,V_com_H). % 47.45/47.53 0 [] -class_Lattices_Obounded__lattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Orderings_Otop__class_Otop(T_a),T_a)=c_Orderings_Otop__class_Otop(T_a). % 47.45/47.53 0 [] -class_Lattices_Obounded__lattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Otop__class_Otop(T_a),V_x,T_a)=c_Orderings_Otop__class_Otop(T_a). % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool))=c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(V_A,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))=c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Com_Ocom_OSemi(V_com1,V_com2)!=c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H). % 47.45/47.53 0 [] c_Set_Oinsert(V_a,V_A,T_a)!=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Com_Ocom_OSemi(V_com1_H,V_com2_H)!=c_Com_Ocom_OLocal(V_loc,V_fun,V_com). % 47.45/47.53 0 [] c_Set_Oinsert(V_x,c_Set_Oinsert(V_x,V_A,T_a),T_a)=c_Set_Oinsert(V_x,V_A,T_a). % 47.45/47.53 0 [] c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H)!=c_Com_Ocom_OAss(V_vname,V_fun). % 47.45/47.53 0 [] hBOOL(hAPP(V_A,V_x))|V_y=V_x| -hBOOL(hAPP(c_Set_Oinsert(V_y,V_A,T_a),V_x)). % 47.45/47.53 0 [] c_Com_Ocom_OCond(V_fun,V_com1,V_com2)!=c_Com_Ocom_OWhile(V_fun_H,V_com_H). % 47.45/47.53 0 [] c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H)!=c_Com_Ocom_OLocal(V_loc,V_fun,V_com). % 47.45/47.53 0 [] c_lesse_quals(V_B,c_Set_Oinsert(V_a,V_B,T_a),tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Finite__Set_Ofinite(V_A,T_a)| -c_Finite__Set_Ofinite(c_Set_Oinsert(V_a,V_A,T_a),T_a). % 47.45/47.53 0 [] c_Finite__Set_Ofinite(c_Set_Oinsert(V_a,V_A,T_a),T_a)| -c_Finite__Set_Ofinite(V_A,T_a). % 47.45/47.53 0 [] c_Finite__Set_Ofinite(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a). % 47.45/47.53 0 [] c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_P,hAPP(c_Com_Ocom_OBODY,V_pn),V_Q,T_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(T_a)),T_a)| -c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_P,hAPP(c_Com_Ocom_OBODY,V_pn),V_Q,T_a),V_G,tc_Hoare__Mirabelle_Otriple(T_a)),c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_P,c_Option_Othe(hAPP(c_Com_Obody,V_pn),tc_Com_Ocom),V_Q,T_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(T_a)),T_a). % 47.45/47.53 0 [] c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H)!=c_Com_Ocom_OSemi(V_com1,V_com2). % 47.45/47.53 0 [] c_Com_Ocom_OCond(V_fun,V_com1,V_com2)!=c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H)|V_com2=V_com2_H. % 47.45/47.53 0 [] c_Com_Ocom_OCond(V_fun,V_com1,V_com2)!=c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H)|V_com1=V_com1_H. % 47.45/47.53 0 [] c_Com_Ocom_OCond(V_fun,V_com1,V_com2)!=c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H)|V_fun=V_fun_H. % 47.45/47.53 0 [] c_Finite__Set_Ofinite(c_Lattices_Oupper__semilattice__class_Osup(V_F,V_G,tc_fun(T_a,tc_bool)),T_a)| -c_Finite__Set_Ofinite(V_G,T_a)| -c_Finite__Set_Ofinite(V_F,T_a). % 47.45/47.53 0 [] c_Finite__Set_Ofinite(c_Lattices_Oupper__semilattice__class_Osup(V_F,V_G,tc_fun(T_a,tc_bool)),T_a)| -c_Finite__Set_Ofinite(V_G,T_a)| -c_Finite__Set_Ofinite(V_F,T_a). % 47.45/47.53 0 [] c_in(V_x,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),T_a). % 47.45/47.53 0 [] c_Option_Ooption_OSome(V_a_H,T_a)!=c_Option_Ooption_ONone(T_a). % 47.45/47.53 0 [] c_Option_Ooption_OSome(V_xa,T_a)!=c_Option_Ooption_ONone(T_a). % 47.45/47.53 0 [] c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H)!=c_Com_Ocom_OCond(V_fun,V_com1,V_com2). % 47.45/47.53 0 [] c_Option_Ooption_OSome(V_a,T_a)!=c_Option_Ooption_OSome(V_a_H,T_a)|V_a=V_a_H. % 47.45/47.53 0 [] hAPP(c_Fun_Ocomp(V_f,V_g,T_b,T_a,T_c),V_x)=hAPP(V_f,hAPP(V_g,V_x)). % 47.45/47.53 0 [] hAPP(V_a,hAPP(V_b,V_v))=hAPP(c_Fun_Ocomp(V_a,V_b,T_c,T_b,T_a),V_v). % 47.45/47.53 0 [] hAPP(V_m,V_a)!=c_Option_Ooption_OSome(V_b,T_a)|c_in(V_a,c_Map_Odom(V_m,T_b,T_a),T_b). % 47.45/47.53 0 [] c_Com_Ocom_OAss(V_vname,V_fun)!=c_Com_Ocom_OWhile(V_fun_H,V_com_H). % 47.45/47.53 0 [] c_Com_Ocom_OAss(V_vname,V_fun)!=c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H). % 47.45/47.53 0 [] hBOOL(hAPP(V_B,V_x))|hBOOL(hAPP(V_A,V_x))| -hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_x)). % 47.45/47.53 0 [] hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_x))| -hBOOL(hAPP(V_B,V_x)). % 47.45/47.53 0 [] hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_x))| -hBOOL(hAPP(V_A,V_x)). % 47.45/47.53 0 [] c_Com_Ocom_Ocom__case(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,c_Com_Ocom_OSKIP,T_a)=V_f1. % 47.45/47.53 0 [] c_in(V_c,V_B,T_a)|c_in(V_c,V_A,T_a)| -c_in(V_c,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),T_a). % 47.45/47.53 0 [] c_Com_Ocom_OLocal(V_loc,V_fun,V_com)!=c_Com_Ocom_OWhile(V_fun_H,V_com_H). % 47.45/47.53 0 [] hAPP(V_m,V_a)!=c_Option_Ooption_ONone(T_b)| -c_in(V_a,c_Map_Odom(V_m,T_a,T_b),T_a). % 47.45/47.53 0 [] c_in(V_a,c_Map_Odom(V_m,T_a,T_b),T_a)|hAPP(V_m,V_a)=c_Option_Ooption_ONone(T_b). % 47.45/47.53 0 [] c_Finite__Set_Ofinite(V_F,T_a)| -c_Finite__Set_Ofinite(c_Lattices_Oupper__semilattice__class_Osup(V_F,V_G,tc_fun(T_a,tc_bool)),T_a). % 47.45/47.53 0 [] c_Finite__Set_Ofinite(V_G,T_a)| -c_Finite__Set_Ofinite(c_Lattices_Oupper__semilattice__class_Osup(V_F,V_G,tc_fun(T_a,tc_bool)),T_a). % 47.45/47.53 0 [] -class_Lattices_Obounded__lattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Orderings_Obot__class_Obot(T_a),T_a)=V_x. % 47.45/47.53 0 [] -class_Lattices_Obounded__lattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(T_a),V_x,T_a)=V_x. % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool))=V_B. % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(V_A,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))=V_A. % 47.45/47.53 0 [] c_Com_Ocom_OAss(V_vname,V_fun)!=c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H). % 47.45/47.53 0 [] c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_P,c_Com_Ocom_OSemi(V_c,V_d),V_R,T_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(T_a)),T_a)| -c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_Q,V_d,V_R,T_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(T_a)),T_a)| -c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,T_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(T_a)),T_a). % 47.45/47.53 0 [] c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),T_a). % 47.45/47.53 0 [] c_Com_Ocom_OSKIP!=c_Com_Ocom_OWhile(V_fun_H,V_com_H). % 47.45/47.53 0 [] -hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)). % 47.45/47.53 0 [] c_Set_Oimage(c_COMBK(V_c,T_a,T_b),V_A,T_b,T_a)=c_Set_Oinsert(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)|V_A=c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)). % 47.45/47.53 0 [] c_Com_Ocom_OSKIP!=c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H). % 47.45/47.53 0 [] c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool))!=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),V_x)). % 47.45/47.53 0 [] c_Set_Oimage(V_f,V_x,T_a,T_b)=c_Set_Oimage(V_g,V_x,T_a,T_b)|c_in(c_ATP__Linkup_Osko__Set__Ximage__cong__1__1(V_x,V_f,V_g,T_a,T_b),V_x,T_a). % 47.45/47.53 0 [] c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,tc_Com_Ostate),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)| -c_Hoare__Mirabelle_Ohoare__valids(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,tc_Com_Ostate),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)| -c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,V_c),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate). % 47.45/47.53 0 [] hAPP(V_f,c_Map_Osko__Map__Xfinite__map__freshness__1__1(V_f,T_a,T_b))=c_Option_Ooption_ONone(T_b)|c_Finite__Set_Ofinite(c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),T_a)| -c_Finite__Set_Ofinite(c_Map_Odom(V_f,T_a,T_b),T_a). % 47.45/47.53 0 [] c_lesse_quals(c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool))| -c_in(V_x,V_A,T_a)| -c_lesse_quals(V_A,c_Set_Oinsert(V_x,V_B,T_a),tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(V_A,c_Set_Oinsert(V_x,V_B,T_a),tc_fun(T_a,tc_bool))| -c_in(V_x,V_A,T_a)| -c_lesse_quals(c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(V_A,c_Set_Oinsert(V_x,V_B,T_a),tc_fun(T_a,tc_bool))| -c_in(V_x,V_A,T_a)| -c_lesse_quals(c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Com_Ocom_Ocom__rec(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,c_Com_Ocom_OLocal(V_loc,V_fun,V_com),T_a)=hAPP(hAPP(hAPP(hAPP(V_f3,V_loc),V_fun),V_com),c_Com_Ocom_Ocom__rec(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,V_com,T_a)). % 47.45/47.53 0 [] c_Com_Ocom_OAss(V_vname,V_fun)!=c_Com_Ocom_OSemi(V_com1_H,V_com2_H). % 47.45/47.53 0 [] c_Com_Ocom_Ocom__rec(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,c_Com_Ocom_OSKIP,T_a)=V_f1. % 47.45/47.53 0 [] c_lesse_quals(V_A,c_Set_Oinsert(V_b,V_B,T_a),tc_fun(T_a,tc_bool))| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool))| -c_lesse_quals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Com_Ocom_OLocal(V_loc,V_fun,V_com)!=c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H). % 47.45/47.53 0 [] c_Com_Ocom_OCond(V_fun,V_com1,V_com2)!=c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H). % 47.45/47.53 0 [] c_Finite__Set_Ofinite(V_B,T_b)| -c_lesse_quals(V_B,c_Set_Oimage(V_f,V_A,T_a,T_b),tc_fun(T_b,tc_bool))| -c_Finite__Set_Ofinite(V_A,T_a). % 47.45/47.53 0 [] c_in(hAPP(V_f,V_x),V_B,T_a)| -c_in(V_x,V_A,T_b)| -c_lesse_quals(c_Set_Oimage(V_f,V_A,T_b,T_a),V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Set_Oimage(c_COMBK(V_c,T_b,T_a),V_A,T_a,T_b)=c_Set_Oinsert(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b)| -c_in(V_x,V_A,T_a). % 47.45/47.53 0 [] V_b=V_a| -c_in(V_b,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a). % 47.45/47.53 0 [] c_Fun_Ocomp(V_f,c_Fun_Oid(T_a),T_a,T_b,T_a)=V_f. % 47.45/47.53 0 [] c_Fun_Ocomp(c_Fun_Oid(T_b),V_g,T_b,T_b,T_a)=V_g. % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(V_A,V_A,tc_fun(T_a,tc_bool))=V_A. % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(V_x,V_x,T_a)=V_x. % 47.45/47.53 0 [] c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H)!=c_Com_Ocom_OSemi(V_com1,V_com2). % 47.45/47.53 0 [] c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_P,hAPP(c_Com_Ocom_OBODY,V_pn),V_Q,T_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(T_a)),T_a)| -c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_P,c_Option_Othe(hAPP(c_Com_Obody,V_pn),tc_Com_Ocom),V_Q,T_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(T_a)),T_a). % 47.45/47.53 0 [] c_in(V_x,c_Set_Oinsert(V_x,V_A,T_a),T_a). % 47.45/47.53 0 [] c_in(V_a,c_Set_Oinsert(V_a,V_B,T_a),T_a). % 47.45/47.53 0 [] c_in(V_x,c_Set_Oinsert(V_x,V_B,T_a),T_a). % 47.45/47.53 0 [] c_Com_Ocom_Ocom__case(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,c_Com_Ocom_OCall(V_vname,V_pname,V_fun),T_a)=hAPP(hAPP(hAPP(V_f8,V_vname),V_pname),V_fun). % 47.45/47.53 0 [] c_Set_Oinsert(V_x,c_Set_Oinsert(V_y,V_A,T_a),T_a)=c_Set_Oinsert(V_y,c_Set_Oinsert(V_x,V_A,T_a),T_a). % 47.45/47.53 0 [] c_in(V_x,V_S,T_a)| -hBOOL(hAPP(V_S,V_x)). % 47.45/47.53 0 [] hBOOL(hAPP(V_S,V_x))| -c_in(V_x,V_S,T_a). % 47.45/47.53 0 [] hAPP(c_COMBI(T_a),V_P)=V_P. % 47.45/47.53 0 [] hAPP(c_COMBK(V_P,T_a,T_b),V_Q)=V_P. % 47.45/47.53 0 [] c_Com_Ocom_Ocom__case(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,c_Com_Ocom_OAss(V_vname,V_fun),T_a)=hAPP(hAPP(V_f2,V_vname),V_fun). % 47.45/47.53 0 [] c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,c_Orderings_Otop__class_Otop(tc_fun(T_b,tc_bool)),T_b,T_a),T_a). % 47.45/47.53 0 [] c_Option_Ooption_ONone(T_a)!=c_Option_Ooption_OSome(V_y,T_a). % 47.45/47.53 0 [] c_Option_Ooption_ONone(T_a)!=c_Option_Ooption_OSome(V_a_H,T_a). % 47.45/47.53 0 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OWhile(V_b,V_c)),V_s0),V_s2))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OWhile(V_b,V_c)),V_s1),V_s2))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c),V_s0),V_s1))| -hBOOL(hAPP(V_b,V_s0)). % 47.45/47.53 0 [] c_Set_Oinsert(V_xa,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)=c_Set_Oinsert(V_x,c_Set_Oinsert(V_xa,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a). % 47.45/47.53 0 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OCond(V_b,V_c0,V_c1)),V_s),V_s1))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c0),V_s),V_s1))| -hBOOL(hAPP(V_b,V_s)). % 47.45/47.53 0 [] -hBOOL(hAPP(V_b,V_s))|hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c1),V_s),V_t))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OCond(V_b,V_c1,V_c2)),V_s),V_t)). % 47.45/47.53 0 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSemi(V_c0,V_c1)),V_s0),V_s2))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c1),V_s1),V_s2))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c0),V_s0),V_s1)). % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(V_A,c_Lattices_Oupper__semilattice__class_Osup(V_B,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(V_B,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_C,tc_fun(T_a,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(V_A,c_Lattices_Oupper__semilattice__class_Osup(V_B,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),V_z,T_a)=c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_y,V_z,T_a),T_a). % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_y,V_z,T_a),T_a)=c_Lattices_Oupper__semilattice__class_Osup(V_y,c_Lattices_Oupper__semilattice__class_Osup(V_x,V_z,T_a),T_a). % 47.45/47.53 0 [] -class_Lattices_Olattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_y,V_z,T_a),T_a)=c_Lattices_Oupper__semilattice__class_Osup(V_y,c_Lattices_Oupper__semilattice__class_Osup(V_x,V_z,T_a),T_a). % 47.45/47.53 0 [] -class_Lattices_Olattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),V_z,T_a)=c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_y,V_z,T_a),T_a). % 47.45/47.53 0 [] c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_C,tc_fun(T_a,tc_bool))| -c_lesse_quals(V_B,V_C,tc_fun(T_a,tc_bool))| -c_lesse_quals(V_A,V_C,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(V_B,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(V_A,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_C,tc_fun(T_a,tc_bool))| -c_lesse_quals(V_B,V_C,tc_fun(T_a,tc_bool))| -c_lesse_quals(V_A,V_C,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(V_a,V_b,T_a),V_x,T_a)| -c_lesse_quals(V_b,V_x,T_a)| -c_lesse_quals(V_a,V_x,T_a). % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_lesse_quals(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),T_a). % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_lesse_quals(V_y,c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),T_a). % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(V_y,V_z,T_a),V_x,T_a)| -c_lesse_quals(V_z,V_x,T_a)| -c_lesse_quals(V_y,V_x,T_a). % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),V_z,T_a)| -c_lesse_quals(V_y,V_z,T_a)| -c_lesse_quals(V_x,V_z,T_a). % 47.45/47.53 0 [] -class_Lattices_Olattice(T_a)|c_lesse_quals(V_y,c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),T_a). % 47.45/47.53 0 [] -class_Lattices_Olattice(T_a)|c_lesse_quals(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),T_a). % 47.45/47.53 0 [] hAPP(V_f,V_x)!=c_Option_Ooption_OSome(V_y,T_a)|c_Set_Oinsert(V_x,c_Map_Odom(V_f,T_b,T_a),T_b)=c_Map_Odom(V_f,T_b,T_a). % 47.45/47.53 0 [] c_Com_Ocom_OSKIP!=c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H). % 47.45/47.53 0 [] c_Com_Ocom_OAss(V_vname,V_fun)!=c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H). % 47.45/47.53 0 [] c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)!=c_Set_Oinsert(V_b,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)|V_a=V_b. % 47.45/47.53 0 [] -hBOOL(hAPP(V_P,V_x))| -c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a). % 47.45/47.53 0 [] c_Set_Oimage(c_COMBK(V_c,T_a,T_b),c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a)=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Set_Oinsert(V_x,V_xa,T_a)!=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))|c_in(V_x,V_xa,T_a). % 47.45/47.53 0 [] c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(V_t,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(T_a)),T_a)| -c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(V_t,V_ts,tc_Hoare__Mirabelle_Otriple(T_a)),T_a). % 47.45/47.53 0 [] c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H)!=c_Com_Ocom_OLocal(V_loc,V_fun,V_com). % 47.45/47.53 0 [] c_in(V_x,V_B,T_a)| -c_lesse_quals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H)!=c_Com_Ocom_OWhile(V_fun,V_com). % 47.45/47.53 0 [] hBOOL(hAPP(c_Set_Oinsert(V_y,V_A,T_a),V_x))| -hBOOL(hAPP(V_A,V_x)). % 47.45/47.53 0 [] c_Set_Oinsert(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_a,T_b),T_b)=c_Set_Oimage(V_f,V_A,T_a,T_b)| -c_in(V_x,V_A,T_a). % 47.45/47.53 0 [] c_lesse_quals(V_A,c_Set_Oinsert(V_x,V_B,T_a),tc_fun(T_a,tc_bool))| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool))|c_in(V_x,V_A,T_a). % 47.45/47.53 0 [] c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool))|c_in(V_x,V_A,T_a)| -c_lesse_quals(V_A,c_Set_Oinsert(V_x,V_B,T_a),tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(V_A,c_Set_Oinsert(V_x,V_B,T_a),tc_fun(T_a,tc_bool))| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool))|c_in(V_x,V_A,T_a). % 47.45/47.53 0 [] c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool))| -c_lesse_quals(V_A,c_Set_Oinsert(V_x,V_B,T_a),tc_fun(T_a,tc_bool))|c_in(V_x,V_A,T_a). % 47.45/47.53 0 [] c_Set_Oinsert(V_x,V_A,T_a)!=c_Set_Oinsert(V_x,V_B,T_a)|c_in(V_x,V_B,T_a)|c_in(V_x,V_A,T_a)|V_A=V_B. % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool))!=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))|V_B=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool))!=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))|V_A=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] -class_Lattices_Obounded__lattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,T_a)!=c_Orderings_Obot__class_Obot(T_a)|V_A=c_Orderings_Obot__class_Obot(T_a). % 47.45/47.53 0 [] -class_Lattices_Obounded__lattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,T_a)!=c_Orderings_Obot__class_Obot(T_a)|V_B=c_Orderings_Obot__class_Obot(T_a). % 47.45/47.53 0 [] c_Fun_Ocomp(V_a,V_b,T_c,T_b,T_a)!=c_Fun_Ocomp(c_Fun_Oid(T_b),V_c,T_b,T_b,T_a)|hAPP(V_a,hAPP(V_b,V_v))=hAPP(V_c,V_v). % 47.45/47.53 0 [] c_Com_Ocom_Ocom__case(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,c_Com_Ocom_OSemi(V_com1,V_com2),T_a)=hAPP(hAPP(V_f4,V_com1),V_com2). % 47.45/47.53 0 [] c_Com_Ocom_OLocal(V_loc,V_fun,V_com)!=c_Com_Ocom_OSemi(V_com1_H,V_com2_H). % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(V_B,V_A,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a)=c_Lattices_Oupper__semilattice__class_Osup(V_y,V_x,T_a). % 47.45/47.53 0 [] -class_Lattices_Olattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a)=c_Lattices_Oupper__semilattice__class_Osup(V_y,V_x,T_a). % 47.45/47.53 0 [] c_Com_Ocom_OWhile(V_fun,V_com)!=c_Com_Ocom_OWhile(V_fun_H,V_com_H)|V_fun=V_fun_H. % 47.45/47.53 0 [] c_Com_Ocom_OWhile(V_fun,V_com)!=c_Com_Ocom_OWhile(V_fun_H,V_com_H)|V_com=V_com_H. % 47.45/47.53 0 [] c_Com_Ocom_Ocom__rec(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,c_Com_Ocom_OCall(V_vname,V_pname,V_fun),T_a)=hAPP(hAPP(hAPP(V_f8,V_vname),V_pname),V_fun). % 47.45/47.53 0 [] c_Set_Oinsert(V_a,V_A,T_a)=V_A| -c_in(V_a,V_A,T_a). % 47.45/47.53 0 [] c_Set_Oinsert(V_a,V_A,T_a)=c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),V_A,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(V_A,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),T_a)=c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a). % 47.45/47.53 0 [] -class_Lattices_Olattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),T_a)=c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a). % 47.45/47.53 0 [] c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H)!=c_Com_Ocom_OSKIP. % 47.45/47.53 0 [] c_Com_Ocom_OWhile(V_fun_H,V_com_H)!=c_Com_Ocom_OCond(V_fun,V_com1,V_com2). % 47.45/47.53 0 [] -class_Finite__Set_Ofinite_Ofinite(T_a)|c_Finite__Set_Ofinite(V_A,T_a). % 47.45/47.53 0 [] hAPP(c_Hoare__Mirabelle_OMGT,V_c)=c_Hoare__Mirabelle_Otriple_Otriple(c_fe_qual(tc_Com_Ostate),V_c,c_Natural_Oevalc(V_c),tc_Com_Ostate). % 47.45/47.53 0 [] c_Com_Ocom_OSemi(V_com1,V_com2)!=c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H). % 47.45/47.53 0 [] c_Com_Ocom_Ocom__rec(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,c_Com_Ocom_OAss(V_vname,V_fun),T_a)=hAPP(hAPP(V_f2,V_vname),V_fun). % 47.45/47.53 0 [] c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H)!=c_Com_Ocom_OAss(V_vname,V_fun). % 47.45/47.53 0 [] c_Com_Ocom_Ocom__rec(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,c_Com_Ocom_OWhile(V_fun,V_com),T_a)=hAPP(hAPP(hAPP(V_f6,V_fun),V_com),c_Com_Ocom_Ocom__rec(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,V_com,T_a)). % 47.45/47.53 0 [] hAPP(c_Fun_Oid(T_a),V_x)=V_x. % 47.45/47.53 0 [] c_Com_Ocom_Ocom__rec(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,c_Com_Ocom_OCond(V_fun,V_com1,V_com2),T_a)=hAPP(hAPP(hAPP(hAPP(hAPP(V_f5,V_fun),V_com1),V_com2),c_Com_Ocom_Ocom__rec(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,V_com1,T_a)),c_Com_Ocom_Ocom__rec(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,V_com2,T_a)). % 47.45/47.53 0 [] V_t=V_s| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),V_s),V_t)). % 47.45/47.53 0 [] -class_HOL_Oord(T_b)|c_lesse_quals(hAPP(V_f,V_x),hAPP(V_g,V_x),T_b)| -c_lesse_quals(V_f,V_g,tc_fun(T_a,T_b)). % 47.45/47.53 0 [] c_in(V_a,V_A,T_a)|V_a=V_b| -c_in(V_a,c_Set_Oinsert(V_b,V_A,T_a),T_a). % 47.45/47.53 0 [] c_Com_Ocom_OWhile(V_fun,V_com)!=c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H). % 47.45/47.53 0 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),V_s),V_s)). % 47.45/47.53 0 [] c_Com_Ocom_OSemi(V_com1_H,V_com2_H)!=c_Com_Ocom_OAss(V_vname,V_fun). % 47.45/47.53 0 [] V_A=V_B| -c_lesse_quals(V_B,V_A,tc_fun(T_a,tc_bool))| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] V_u=V_t| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c),V_s),V_u))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c),V_s),V_t)). % 47.45/47.53 0 [] V_A=V_B| -c_lesse_quals(V_B,V_A,tc_fun(T_a,tc_bool))| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] -class_Orderings_Oorder(T_a)|V_x=V_y| -c_lesse_quals(V_y,V_x,T_a)| -c_lesse_quals(V_x,V_y,T_a). % 47.45/47.53 0 [] -class_Orderings_Oorder(T_a)|V_x=V_y| -c_lesse_quals(V_y,V_x,T_a)| -c_lesse_quals(V_x,V_y,T_a). % 47.45/47.53 0 [] -class_Orderings_Oorder(T_a)|V_x=V_y| -c_lesse_quals(V_x,V_y,T_a)| -c_lesse_quals(V_y,V_x,T_a). % 47.45/47.53 0 [] c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H)!=c_Com_Ocom_OSKIP. % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a)=V_x| -c_lesse_quals(V_y,V_x,T_a). % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a)!=V_y|c_lesse_quals(V_x,V_y,T_a). % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a)=V_y| -c_lesse_quals(V_x,V_y,T_a). % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool))=V_B| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool))=V_A| -c_lesse_quals(V_B,V_A,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool))!=V_B|c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Set_Oinsert(V_a,c_Set_Oinsert(V_b,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)!=c_Set_Oinsert(V_c,c_Set_Oinsert(V_d,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)|V_a=V_d|V_a=V_c. % 47.45/47.53 0 [] c_Set_Oinsert(V_a,c_Set_Oinsert(V_b,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)!=c_Set_Oinsert(V_c,c_Set_Oinsert(V_d,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)|V_b=V_c|V_a=V_c. % 47.45/47.53 0 [] c_Set_Oinsert(V_a,c_Set_Oinsert(V_b,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)!=c_Set_Oinsert(V_c,c_Set_Oinsert(V_d,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)|V_a=V_d|V_b=V_d. % 47.45/47.53 0 [] c_Set_Oinsert(V_a,c_Set_Oinsert(V_b,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)!=c_Set_Oinsert(V_c,c_Set_Oinsert(V_d,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)|V_b=V_c|V_b=V_d. % 47.45/47.53 0 [] c_Fun_Obij__betw(c_Fun_Ocomp(V_g,V_f,T_b,T_c,T_a),V_A,V_C,T_a,T_c)| -c_Fun_Obij__betw(V_g,V_B,V_C,T_b,T_c)| -c_Fun_Obij__betw(V_f,V_A,V_B,T_a,T_b). % 47.45/47.53 0 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c2),V_s),V_t))|hBOOL(hAPP(V_b,V_s))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OCond(V_b,V_c1,V_c2)),V_s),V_t)). % 47.45/47.53 0 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OCond(V_b,V_c0,V_c1)),V_s),V_s1))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c1),V_s),V_s1))|hBOOL(hAPP(V_b,V_s)). % 47.45/47.53 0 [] c_Com_Ocom_OSKIP!=c_Com_Ocom_OAss(V_vname_H,V_fun_H). % 47.45/47.53 0 [] c_Hoare__Mirabelle_Otriple_Otriple(V_fun1,V_com,V_fun2,T_a)!=c_Hoare__Mirabelle_Otriple_Otriple(V_fun1_H,V_com_H,V_fun2_H,T_a)|V_fun1=V_fun1_H. % 47.45/47.53 0 [] c_Hoare__Mirabelle_Otriple_Otriple(V_fun1,V_com,V_fun2,T_a)!=c_Hoare__Mirabelle_Otriple_Otriple(V_fun1_H,V_com_H,V_fun2_H,T_a)|V_com=V_com_H. % 47.45/47.53 0 [] c_Hoare__Mirabelle_Otriple_Otriple(V_fun1,V_com,V_fun2,T_a)!=c_Hoare__Mirabelle_Otriple_Otriple(V_fun1_H,V_com_H,V_fun2_H,T_a)|V_fun2=V_fun2_H. % 47.45/47.53 0 [] V_A=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))| -c_lesse_quals(V_A,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Com_Ocom_OWhile(V_fun_H,V_com_H)!=c_Com_Ocom_OAss(V_vname,V_fun). % 47.45/47.53 0 [] c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))!=c_Set_Oinsert(V_a,V_A,T_a). % 47.45/47.53 0 [] c_Com_Ocom_Ocom__case(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,c_Com_Ocom_OLocal(V_loc,V_fun,V_com),T_a)=hAPP(hAPP(hAPP(V_f3,V_loc),V_fun),V_com). % 47.45/47.53 0 [] c_Com_Ocom_Ocom__case(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,c_Com_Ocom_OWhile(V_fun,V_com),T_a)=hAPP(hAPP(V_f6,V_fun),V_com). % 47.45/47.53 0 [] -c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a). % 47.45/47.53 0 [] -c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a). % 47.45/47.53 0 [] hBOOL(hAPP(V_P,V_x))| -c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a). % 47.45/47.53 0 [] -c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a). % 47.45/47.53 0 [] c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a)| -c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_G_H,T_a)| -c_Hoare__Mirabelle_Ohoare__derivs(V_G_H,V_ts,T_a). % 47.45/47.53 0 [] c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),c_Lattices_Oupper__semilattice__class_Osup(V_C,V_D,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))| -c_lesse_quals(V_B,V_D,tc_fun(T_a,tc_bool))| -c_lesse_quals(V_A,V_C,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(V_A,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] -class_Orderings_Otop(T_a)|c_lesse_quals(V_x,c_Orderings_Otop__class_Otop(T_a),T_a). % 47.45/47.53 0 [] c_Fun_Ocomp(V_f,c_Fun_Ocomp(V_g,V_h,T_d,T_c,T_a),T_c,T_b,T_a)=c_Fun_Ocomp(c_Fun_Ocomp(V_f,V_g,T_c,T_b,T_d),V_h,T_d,T_b,T_a). % 47.45/47.53 0 [] c_Com_Ocom_OAss(V_vname,V_fun)!=c_Com_Ocom_OAss(V_vname_H,V_fun_H)|V_fun=V_fun_H. % 47.45/47.53 0 [] c_Com_Ocom_OAss(V_vname,V_fun)!=c_Com_Ocom_OAss(V_vname_H,V_fun_H)|V_vname=V_vname_H. % 47.45/47.53 0 [] c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H)!=c_Com_Ocom_OAss(V_vname,V_fun). % 47.45/47.53 0 [] c_Com_Ocom_OSemi(V_com1_H,V_com2_H)!=c_Com_Ocom_OSKIP. % 47.45/47.53 0 [] c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_P,c_Com_Ocom_OSKIP,V_P,T_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(T_a)),T_a). % 47.45/47.53 0 [] hBOOL(hAPP(c_Set_Oinsert(V_x,V_A,T_a),V_x)). % 47.45/47.53 0 [] c_lesse_quals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool))| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool))| -c_in(V_x,V_B,T_a). % 47.45/47.53 0 [] c_Com_Ocom_OLocal(V_loc,V_fun,V_com)!=c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H)|V_com=V_com_H. % 47.45/47.53 0 [] c_Com_Ocom_OLocal(V_loc,V_fun,V_com)!=c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H)|V_fun=V_fun_H. % 47.45/47.53 0 [] c_Com_Ocom_OLocal(V_loc,V_fun,V_com)!=c_Com_Ocom_OLocal(V_loc_H,V_fun_H,V_com_H)|V_loc=V_loc_H. % 47.45/47.53 0 [] c_Com_Ocom_OSKIP!=c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H). % 47.45/47.53 0 [] c_Com_Ocom_OWhile(V_fun_H,V_com_H)!=c_Com_Ocom_OSemi(V_com1,V_com2). % 47.45/47.53 0 [] -class_Finite__Set_Ofinite_Ofinite(T_a)|c_Finite__Set_Ofinite(c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),T_a). % 47.45/47.53 0 [] c_in(V_c,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)| -c_in(V_c,V_B,T_a). % 47.45/47.53 0 [] c_in(V_c,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)| -c_in(V_c,V_A,T_a). % 47.45/47.53 0 [] hBOOL(hAPP(V_b,V_s))|V_t=V_s| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OWhile(V_b,V_c)),V_s),V_t)). % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_lesse_quals(V_y,V_z,T_a)| -c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),V_z,T_a). % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_lesse_quals(V_x,V_z,T_a)| -c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),V_z,T_a). % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_lesse_quals(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_a,V_b,T_a),T_a)| -c_lesse_quals(V_x,V_b,T_a). % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_lesse_quals(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_a,V_b,T_a),T_a)| -c_lesse_quals(V_x,V_a,T_a). % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_lesse_quals(V_b,V_x,T_a)| -c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(V_a,V_b,T_a),V_x,T_a). % 47.45/47.53 0 [] -class_Lattices_Oupper__semilattice(T_a)|c_lesse_quals(V_a,V_x,T_a)| -c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(V_a,V_b,T_a),V_x,T_a). % 47.45/47.53 0 [] c_lesse_quals(V_A,V_C,tc_fun(T_a,tc_bool))| -c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_C,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(V_B,V_C,tc_fun(T_a,tc_bool))| -c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_C,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] -class_Orderings_Oorder(T_a)|c_lesse_quals(V_z,V_x,T_a)| -c_lesse_quals(V_z,V_y,T_a)| -c_lesse_quals(V_y,V_x,T_a). % 47.45/47.53 0 [] -class_Orderings_Opreorder(T_a)|c_lesse_quals(V_x,V_z,T_a)| -c_lesse_quals(V_y,V_z,T_a)| -c_lesse_quals(V_x,V_y,T_a). % 47.45/47.53 0 [] c_in(V_x,V_B,T_a)| -c_in(V_x,V_A,T_a)| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_in(V_c,V_B,T_a)| -c_in(V_c,V_A,T_a)| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(V_x,V_x,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_in(V_x,V_B,T_a)| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool))| -c_in(V_x,V_A,T_a). % 47.45/47.53 0 [] c_in(V_t,V_B,T_a)| -c_in(V_t,V_A,T_a)| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(V_A,V_A,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(V_A,V_C,tc_fun(T_a,tc_bool))| -c_lesse_quals(V_B,V_C,tc_fun(T_a,tc_bool))| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] hBOOL(hAPP(V_Q,V_x))| -hBOOL(hAPP(V_P,V_x))| -c_lesse_quals(V_P,V_Q,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] -class_Orderings_Oorder(T_a)|c_lesse_quals(V_x,V_x,T_a). % 47.45/47.53 0 [] -class_Orderings_Opreorder(T_a)|c_lesse_quals(V_x,V_x,T_a). % 47.45/47.53 0 [] c_Finite__Set_Ofinite(V_A,T_a)| -c_Finite__Set_Ofinite(V_B,T_a)| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] hBOOL(hAPP(V_Q,V_x))| -c_lesse_quals(V_P,V_Q,tc_fun(T_a,tc_bool))| -hBOOL(hAPP(V_P,V_x)). % 47.45/47.53 0 [] c_Finite__Set_Ofinite(V_A,T_a)| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool))| -c_Finite__Set_Ofinite(V_B,T_a). % 47.45/47.53 0 [] c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H)!=c_Com_Ocom_OSKIP. % 47.45/47.53 0 [] c_in(V_a,c_Set_Oinsert(V_b,V_B,T_a),T_a)| -c_in(V_a,V_B,T_a). % 47.45/47.53 0 [] c_in(V_a,c_Set_Oinsert(V_b,V_A,T_a),T_a)| -c_in(V_a,V_A,T_a). % 47.45/47.53 0 [] c_in(V_x,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a). % 47.45/47.53 0 [] c_Com_Ocom_Ocom__case(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,c_Com_Ocom_OCond(V_fun,V_com1,V_com2),T_a)=hAPP(hAPP(hAPP(V_f5,V_fun),V_com1),V_com2). % 47.45/47.53 0 [] c_Fun_Ocomp(V_a,V_b,T_c,T_b,T_a)!=c_Fun_Ocomp(V_c,V_d,T_d,T_b,T_a)|hAPP(V_a,hAPP(V_b,V_v))=hAPP(V_c,hAPP(V_d,V_v)). % 47.45/47.53 0 [] hAPP(V_f,hAPP(V_g,V_x))!=hAPP(V_f_H,hAPP(V_g_H,V_x_H))|hAPP(c_Fun_Ocomp(V_f,V_g,T_b,T_a,T_c),V_x)=hAPP(c_Fun_Ocomp(V_f_H,V_g_H,T_d,T_a,T_e),V_x_H). % 47.45/47.53 0 [] V_A=c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)|V_A=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))| -c_lesse_quals(V_A,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a)| -c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(V_t,V_ts,tc_Hoare__Mirabelle_Otriple(T_a)),T_a). % 47.45/47.53 0 [] c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(V_t,V_ts,tc_Hoare__Mirabelle_Otriple(T_a)),T_a)| -c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a)| -c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(V_t,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(T_a)),T_a). % 47.45/47.53 0 [] c_Com_Ocom_OAss(V_vname_H,V_fun_H)!=c_Com_Ocom_OSKIP. % 47.45/47.53 0 [] c_lesse_quals(c_Set_Oinsert(V_a,V_C,T_a),c_Set_Oinsert(V_a,V_D,T_a),tc_fun(T_a,tc_bool))| -c_lesse_quals(V_C,V_D,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_Option_Othe(c_Option_Ooption_OSome(V_x,T_a),T_a)=V_x. % 47.45/47.53 0 [] c_Com_Ocom_OLocal(V_loc,V_fun,V_com)!=c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H). % 47.45/47.53 0 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c2),V_s),V_t))|hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c1),V_s),V_t))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OCond(V_b,V_c1,V_c2)),V_s),V_t)). % 47.45/47.53 0 [] c_Com_Ocom_OSKIP!=c_Com_Ocom_OSemi(V_com1_H,V_com2_H). % 47.45/47.53 0 [] -class_Orderings_Olinorder(T_a)|c_lesse_quals(V_y,V_x,T_a)|c_lesse_quals(V_x,V_y,T_a). % 47.45/47.53 0 [] hBOOL(hAPP(c_Com_OWT,V_c1))| -hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OCond(V_b,V_c1,V_c2))). % 47.45/47.53 0 [] hBOOL(hAPP(c_Com_OWT,V_c2))| -hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OCond(V_b,V_c1,V_c2))). % 47.45/47.53 0 [] c_Set_Oimage(V_f,c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_b,tc_bool)),T_b,T_a)=c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(V_f,V_A,T_b,T_a),c_Set_Oimage(V_f,V_B,T_b,T_a),tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] -c_lesse_quals(V_x,V_A,tc_fun(T_b,tc_bool))|c_lesse_quals(c_Set_Oimage(V_f,V_x,T_b,T_a),c_Set_Oimage(V_f,V_A,T_b,T_a),tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] c_lesse_quals(c_Set_Oimage(V_f,V_A,T_a,T_b),c_Set_Oimage(V_f,V_B,T_a,T_b),tc_fun(T_b,tc_bool))| -c_lesse_quals(V_A,V_B,tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] hAPP(V_f,c_ATP__Linkup_Osko__Set__Ximage__cong__1__1(V_x,V_f,V_g,T_a,T_b))!=hAPP(V_g,c_ATP__Linkup_Osko__Set__Ximage__cong__1__1(V_x,V_f,V_g,T_a,T_b))|c_Set_Oimage(V_f,V_x,T_a,T_b)=c_Set_Oimage(V_g,V_x,T_a,T_b). % 47.45/47.53 0 [] hBOOL(hAPP(c_Com_OWT,hAPP(c_Com_Ocom_OBODY,V_pn)))|hAPP(c_Com_Obody,V_pn)=c_Option_Ooption_ONone(tc_Com_Ocom). % 47.45/47.53 0 [] hAPP(c_Com_Ocom_OBODY,V_pname_H)!=c_Com_Ocom_OSKIP. % 47.45/47.53 0 [] c_Com_Ocom_OWhile(V_fun,V_com)!=hAPP(c_Com_Ocom_OBODY,V_pname_H). % 47.45/47.53 0 [] c_Com_Ocom_Ocom__rec(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,hAPP(c_Com_Ocom_OBODY,V_pname),T_a)=hAPP(V_f7,V_pname). % 47.45/47.53 0 [] c_Set_Oimage(V_f,V_A,T_b,T_a)!=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))|V_A=c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)). % 47.45/47.53 0 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(hAPP(c_Com_Ocom_OBODY,V_pn)),V_s0),V_s1))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Option_Othe(hAPP(c_Com_Obody,V_pn),tc_Com_Ocom)),V_s0),V_s1)). % 47.45/47.53 0 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Option_Othe(hAPP(c_Com_Obody,V_P),tc_Com_Ocom)),V_s),V_s1))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(hAPP(c_Com_Ocom_OBODY,V_P)),V_s),V_s1)). % 47.45/47.53 0 [] c_Set_Oimage(c_Fun_Ocomp(V_f,V_g,T_c,T_a,T_b),V_r,T_b,T_a)=c_Set_Oimage(V_f,c_Set_Oimage(V_g,V_r,T_b,T_c),T_c,T_a). % 47.45/47.53 0 [] c_Set_Oimage(V_f,V_A,T_a,T_b)=V_B| -c_Fun_Obij__betw(V_f,V_A,V_B,T_a,T_b). % 47.45/47.53 0 [] hAPP(c_Com_Obody,V_pn)!=c_Option_Ooption_OSome(V_b,tc_Com_Ocom)| -c_Com_OWT__bodies|hBOOL(hAPP(c_Com_OWT,V_b)). % 47.45/47.53 0 [] hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OSemi(V_c0,V_c1)))| -hBOOL(hAPP(c_Com_OWT,V_c1))| -hBOOL(hAPP(c_Com_OWT,V_c0)). % 47.45/47.53 0 [] c_Set_Oimage(V_f,c_Set_Oimage(V_g,V_A,T_c,T_b),T_b,T_a)=c_Set_Oimage(c_COMBB(V_f,V_g,T_b,T_a,T_c),V_A,T_c,T_a). % 47.45/47.53 0 [] c_Set_Oimage(V_f,c_Set_Oinsert(V_a,V_B,T_b),T_b,T_a)=c_Set_Oinsert(hAPP(V_f,V_a),c_Set_Oimage(V_f,V_B,T_b,T_a),T_a). % 47.45/47.53 0 [] hBOOL(hAPP(c_Com_OWT,V_c1))| -hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OSemi(V_c1,V_c2))). % 47.45/47.53 0 [] hBOOL(hAPP(c_Com_OWT,V_c2))| -hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OSemi(V_c1,V_c2))). % 47.45/47.53 0 [] c_Finite__Set_Ofinite(c_Set_Oimage(V_h,V_F,T_a,T_b),T_b)| -c_Finite__Set_Ofinite(V_F,T_a). % 47.45/47.53 0 [] c_Com_OWT__bodies| -c_split(c_COMBK(c_Com_OWT,tc_fun(tc_Com_Ocom,tc_bool),tc_Com_Opname),c_Com_Osko__Com__XWT__bodies__def__1__1,tc_Com_Opname,tc_Com_Ocom,tc_bool). % 47.45/47.53 0 [] hAPP(c_Com_Ocom_OBODY,V_pname_H)!=c_Com_Ocom_OCond(V_fun,V_com1,V_com2). % 47.45/47.53 0 [] c_Com_Ocom_OCond(V_fun,V_com1,V_com2)!=hAPP(c_Com_Ocom_OBODY,V_pname_H). % 47.45/47.53 0 [] c_Set_Oimage(c_COMBB(V_f,V_g,T_c,T_a,T_b),c_Orderings_Otop__class_Otop(tc_fun(T_b,tc_bool)),T_b,T_a)=c_Set_Oimage(V_f,c_Set_Oimage(V_g,c_Orderings_Otop__class_Otop(tc_fun(T_b,tc_bool)),T_b,T_c),T_c,T_a). % 47.45/47.53 0 [] hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OCond(V_b,V_c0,V_c1)))| -hBOOL(hAPP(c_Com_OWT,V_c1))| -hBOOL(hAPP(c_Com_OWT,V_c0)). % 47.45/47.53 0 [] c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,V_c),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)| -hBOOL(hAPP(c_Com_OWT,V_c))| -c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_sko__Hoare__Mirabelle__XMGF__lemma1__1(V_G))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)| -c_Hoare__Mirabelle_Ostate__not__singleton. % 47.45/47.53 0 [] c_Hoare__Mirabelle_Ostate__not__singleton|V_x=V_xa. % 47.45/47.53 0 [] v_sko__Hoare__Mirabelle__Xsingle__stateE__1(V_t)!=V_t| -c_Hoare__Mirabelle_Ostate__not__singleton. % 47.45/47.53 0 [] hAPP(c_Com_Ocom_OBODY,V_pname_H)!=c_Com_Ocom_OAss(V_vname,V_fun). % 47.45/47.53 0 [] c_Com_Ocom_OAss(V_vname,V_fun)!=hAPP(c_Com_Ocom_OBODY,V_pname_H). % 47.45/47.53 0 [] c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))!=c_Set_Oimage(V_f,V_A,T_b,T_a)|V_A=c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)). % 47.45/47.53 0 [] hAPP(c_Com_Ocom_OBODY,V_pname_H)!=c_Com_Ocom_OLocal(V_loc,V_fun,V_com). % 47.45/47.53 0 [] hAPP(c_Com_Ocom_OBODY,V_pname_H)!=c_Com_Ocom_OWhile(V_fun,V_com). % 47.45/47.53 0 [] hAPP(c_Com_Obody,V_P)=c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(V_P),tc_Com_Ocom)| -hBOOL(hAPP(c_Com_OWT,hAPP(c_Com_Ocom_OBODY,V_P))). % 47.45/47.53 0 [] c_Com_OWT__bodies| -c_split(c_COMBK(c_Com_OWT,tc_fun(tc_Com_Ocom,tc_bool),tc_Com_Opname),c_Com_Osko__Com__XWT__bodies__def__raw__1__1,tc_Com_Opname,tc_Com_Ocom,tc_bool). % 47.45/47.53 0 [] c_Set_Oimage(c_COMBI(T_a),V_Y,T_a,T_a)=V_Y. % 47.45/47.53 0 [] c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,V_pn)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)| -c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,V_pn)),V_G,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,c_Option_Othe(hAPP(c_Com_Obody,V_pn),tc_Com_Ocom)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate). % 47.45/47.53 0 [] c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H)!=hAPP(c_Com_Ocom_OBODY,V_pname). % 47.45/47.53 0 [] c_Finite__Set_Ofinite(c_Set_Oimage(c_COMBB(V_f,V_g,T_a,T_c,T_b),c_Orderings_Otop__class_Otop(tc_fun(T_b,tc_bool)),T_b,T_c),T_c)| -c_Finite__Set_Ofinite(c_Set_Oimage(V_g,c_Orderings_Otop__class_Otop(tc_fun(T_b,tc_bool)),T_b,T_a),T_a). % 47.45/47.53 0 [] hAPP(c_Com_Ocom_OBODY,V_pname_H)!=c_Com_Ocom_OSemi(V_com1,V_com2). % 47.45/47.53 0 [] hAPP(c_COMBB(V_P,V_Q,T_b,T_a,T_c),V_R)=hAPP(V_P,hAPP(V_Q,V_R)). % 47.45/47.53 0 [] c_Com_Ocom_OSemi(V_com1,V_com2)!=hAPP(c_Com_Ocom_OBODY,V_pname_H). % 47.45/47.53 0 [] hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OSKIP)). % 47.45/47.53 0 [] c_Set_Oimage(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a)=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 47.45/47.53 0 [] hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OAss(V_X,V_a))). % 47.45/47.53 0 [] hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OCall(V_X,V_pn,V_a)))| -hBOOL(hAPP(c_Com_OWT,hAPP(c_Com_Ocom_OBODY,V_pn))). % 47.45/47.53 0 [] hBOOL(hAPP(c_Com_OWT,hAPP(c_Com_Ocom_OBODY,V_P)))| -hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OCall(V_X,V_P,V_a))). % 47.45/47.53 0 [] hAPP(c_Hoare__Mirabelle_OMGT,v_c)=c_Hoare__Mirabelle_Otriple_Otriple(c_fe_qual(tc_Com_Ostate),v_c,c_Natural_Oevalc(v_c),tc_Com_Ostate). % 47.45/47.53 0 [] c_Com_Ocom_OLocal(V_loc,V_fun,V_com)!=hAPP(c_Com_Ocom_OBODY,V_pname_H). % 47.45/47.53 0 [] hAPP(c_Com_Ocom_OBODY,V_pname)!=c_Com_Ocom_OCall(V_vname_H,V_pname_H,V_fun_H). % 47.45/47.53 0 [] c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,V_c),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)| -hBOOL(hAPP(c_Com_OWT,V_c))|c_in(v_sko__Hoare__Mirabelle__XMGF__lemma1__1(V_G),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)| -c_Hoare__Mirabelle_Ostate__not__singleton. % 47.45/47.53 0 [] c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname). % 47.45/47.53 0 [] c_Set_Oimage(c_Fun_Oid(T_a),V_Y,T_a,T_a)=V_Y. % 47.45/47.53 0 [] hAPP(c_Com_Ocom_OBODY,V_pname)!=hAPP(c_Com_Ocom_OBODY,V_pname_H)|V_pname=V_pname_H. % 47.45/47.53 0 [] hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OWhile(V_b,V_c)))| -hBOOL(hAPP(c_Com_OWT,V_c)). % 47.45/47.53 0 [] hBOOL(hAPP(c_Com_OWT,V_c))| -hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OWhile(V_b,V_c))). % 47.45/47.53 0 [] c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))=c_Set_Oimage(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a). % 47.45/47.53 0 [] hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OLocal(V_Y,V_a,V_c)))| -hBOOL(hAPP(c_Com_OWT,V_c)). % 47.45/47.53 0 [] hBOOL(hAPP(c_Com_OWT,V_c))| -hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OLocal(V_Y,V_a,V_c))). % 47.45/47.53 0 [] c_Com_Ocom_Ocom__case(V_f1,V_f2,V_f3,V_f4,V_f5,V_f6,V_f7,V_f8,hAPP(c_Com_Ocom_OBODY,V_pname),T_a)=hAPP(V_f7,V_pname). % 47.45/47.53 0 [] c_Com_Ocom_OSKIP!=hAPP(c_Com_Ocom_OBODY,V_pname_H). % 47.45/47.53 0 [] -c_in(V_x,V_A,T_aa)|c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_aa,T_a),T_a). % 47.45/47.53 0 [] -c_in(V_x,V_A,T_b)|c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_b,T_a),T_a). % 47.45/47.53 0 [] c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_b,T_a),T_a)| -c_in(V_x,V_A,T_b). % 47.45/47.53 0 [] c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_a,T_b),T_b)| -c_in(V_x,V_A,T_a). % 47.45/47.53 0 [] c_Hoare__Mirabelle_Ostate__not__singleton. % 47.45/47.53 0 [] c_Com_OWT__bodies. % 47.45/47.53 0 [] hBOOL(hAPP(c_Com_OWT,v_c)). % 47.45/47.53 0 [] v_uG!=c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)). % 47.45/47.53 0 [] class_Lattices_Oupper__semilattice(tc_fun(T_2,T_1))| -class_Lattices_Olattice(T_1). % 47.45/47.53 0 [] class_Lattices_Obounded__lattice(tc_fun(T_2,T_1))| -class_Lattices_Obounded__lattice(T_1). % 47.45/47.53 0 [] class_Finite__Set_Ofinite_Ofinite(tc_fun(T_2,T_1))| -class_Finite__Set_Ofinite_Ofinite(T_1)| -class_Finite__Set_Ofinite_Ofinite(T_2). % 47.45/47.53 0 [] class_Orderings_Opreorder(tc_fun(T_2,T_1))| -class_Orderings_Opreorder(T_1). % 47.45/47.53 0 [] class_Lattices_Olattice(tc_fun(T_2,T_1))| -class_Lattices_Olattice(T_1). % 47.45/47.53 0 [] class_Orderings_Oorder(tc_fun(T_2,T_1))| -class_Orderings_Oorder(T_1). % 47.45/47.53 0 [] class_Orderings_Otop(tc_fun(T_2,T_1))| -class_Orderings_Otop(T_1). % 47.45/47.53 0 [] class_Orderings_Obot(tc_fun(T_2,T_1))| -class_Orderings_Obot(T_1). % 47.45/47.53 0 [] class_HOL_Oord(tc_fun(T_2,T_1))| -class_HOL_Oord(T_1). % 47.45/47.53 0 [] class_Lattices_Oupper__semilattice(tc_nat). % 47.45/47.53 0 [] class_Orderings_Opreorder(tc_nat). % 47.45/47.53 0 [] class_Orderings_Olinorder(tc_nat). % 47.45/47.53 0 [] class_Lattices_Olattice(tc_nat). % 47.45/47.53 0 [] class_Orderings_Oorder(tc_nat). % 47.45/47.53 0 [] class_Orderings_Obot(tc_nat). % 47.45/47.53 0 [] class_HOL_Oord(tc_nat). % 47.45/47.53 0 [] class_Lattices_Oupper__semilattice(tc_bool). % 47.45/47.53 0 [] class_Lattices_Obounded__lattice(tc_bool). % 47.45/47.53 0 [] class_Finite__Set_Ofinite_Ofinite(tc_bool). % 47.45/47.53 0 [] class_Orderings_Opreorder(tc_bool). % 47.45/47.53 0 [] class_Lattices_Olattice(tc_bool). % 47.45/47.53 0 [] class_Orderings_Oorder(tc_bool). % 47.45/47.53 0 [] class_Orderings_Otop(tc_bool). % 47.45/47.53 0 [] class_Orderings_Obot(tc_bool). % 47.45/47.53 0 [] class_HOL_Oord(tc_bool). % 47.45/47.53 0 [] class_Finite__Set_Ofinite_Ofinite(tc_Option_Ooption(T_1))| -class_Finite__Set_Ofinite_Ofinite(T_1). % 47.45/47.53 0 [] c_COMBC(V_P,V_Q,V_R,T_b,T_c,T_a)=hAPP(hAPP(V_P,V_R),V_Q). % 47.45/47.53 0 [] hAPP(c_COMBB(V_P,V_Q,T_b,T_a,T_c),V_R)=hAPP(V_P,hAPP(V_Q,V_R)). % 47.45/47.53 0 [] hBOOL(hAPP(hAPP(c_fe_qual(T_a),V_x),V_x)). % 47.45/47.53 0 [] V_X=V_Y| -hBOOL(hAPP(hAPP(c_fe_qual(T_a),V_X),V_Y)). % 47.45/47.53 end_of_list. % 47.45/47.53 % 47.45/47.53 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=4. % 47.45/47.53 % 47.45/47.53 This ia a non-Horn set with equality. The strategy will be % 47.45/47.53 Knuth-Bendix, ordered hyper_res, factoring, and unit % 47.45/47.53 deletion, with positive clauses in sos and nonpositive % 47.45/47.53 clauses in usable. % 47.45/47.53 % 47.45/47.53 dependent: set(knuth_bendix). % 47.45/47.53 dependent: set(anl_eq). % 47.45/47.53 dependent: set(para_from). % 47.45/47.53 dependent: set(para_into). % 47.45/47.53 dependent: clear(para_from_right). % 47.45/47.53 dependent: clear(para_into_right). % 47.45/47.53 dependent: set(para_from_vars). % 47.45/47.53 dependent: set(eq_units_both_ways). % 47.45/47.53 dependent: set(dynamic_demod_all). % 47.45/47.53 dependent: set(dynamic_demod). % 47.45/47.53 dependent: set(order_eq). % 47.45/47.53 dependent: set(back_demod). % 47.45/47.53 dependent: set(lrpo). % 47.45/47.53 dependent: set(hyper_res). % 47.45/47.53 dependent: set(unit_deletion). % 47.45/47.53 dependent: set(factor). % 47.45/47.53 % 47.45/47.53 ------------> process usable: % 47.45/47.53 ** KEPT (pick-wt=19): 1 [] c_Lattices_Oupper__semilattice__class_Osup(A,c_HOL_Ominus__class_Ominus(B,A,tc_fun(C,tc_bool)),tc_fun(C,tc_bool))=B| -c_lesse_quals(A,B,tc_fun(C,tc_bool)). % 47.45/47.53 ** KEPT (pick-wt=22): 2 [] c_lesse_quals(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),D,tc_fun(C,tc_bool))| -c_lesse_quals(A,c_Lattices_Oupper__semilattice__class_Osup(B,D,tc_fun(C,tc_bool)),tc_fun(C,tc_bool)). % 47.45/47.53 ** KEPT (pick-wt=22): 3 [] c_lesse_quals(A,c_Lattices_Oupper__semilattice__class_Osup(B,C,tc_fun(D,tc_bool)),tc_fun(D,tc_bool))| -c_lesse_quals(c_HOL_Ominus__class_Ominus(A,B,tc_fun(D,tc_bool)),C,tc_fun(D,tc_bool)). % 47.45/47.53 ** KEPT (pick-wt=19): 4 [] c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool)),D)| -c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(A,C,tc_fun(D,tc_bool)),D). % 47.45/47.53 ** KEPT (pick-wt=19): 5 [] c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),C)| -c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(D,B,C),tc_fun(C,tc_bool)),C). % 47.45/47.53 ** KEPT (pick-wt=20): 6 [] c_HOL_Ominus__class_Ominus(c_Set_Oinsert(A,B,C),D,tc_fun(C,tc_bool))=c_HOL_Ominus__class_Ominus(B,D,tc_fun(C,tc_bool))| -c_in(A,D,C). % 47.45/47.53 ** KEPT (pick-wt=19): 7 [] -class_OrderedGroup_Opordered__ab__group__add(A)|c_HOL_Ominus__class_Ominus(B,C,A)!=c_HOL_Ominus__class_Ominus(D,E,A)|c_lesse_quals(C,B,A)| -c_lesse_quals(E,D,A). % 47.45/47.53 ** KEPT (pick-wt=19): 8 [] -class_OrderedGroup_Opordered__ab__group__add(A)|c_HOL_Ominus__class_Ominus(B,C,A)!=c_HOL_Ominus__class_Ominus(D,E,A)|c_lesse_quals(E,D,A)| -c_lesse_quals(C,B,A). % 47.45/47.53 ** KEPT (pick-wt=25): 9 [] c_HOL_Ominus__class_Ominus(A,c_HOL_Ominus__class_Ominus(B,C,tc_fun(D,tc_bool)),tc_fun(D,tc_bool))=C| -c_lesse_quals(A,B,tc_fun(D,tc_bool))| -c_lesse_quals(C,A,tc_fun(D,tc_bool)). % 47.45/47.53 ** KEPT (pick-wt=28): 10 [] c_lesse_quals(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),c_HOL_Ominus__class_Ominus(D,E,tc_fun(C,tc_bool)),tc_fun(C,tc_bool))| -c_lesse_quals(E,B,tc_fun(C,tc_bool))| -c_lesse_quals(A,D,tc_fun(C,tc_bool)). % 47.45/47.53 ** KEPT (pick-wt=13): 11 [] -c_in(A,B,C)| -c_in(A,c_HOL_Ominus__class_Ominus(D,B,tc_fun(C,tc_bool)),C). % 47.45/47.53 ** KEPT (pick-wt=13): 12 [] c_in(A,B,C)| -c_in(A,c_HOL_Ominus__class_Ominus(B,D,tc_fun(C,tc_bool)),C). % 47.45/47.53 ** KEPT (pick-wt=14): 13 [] c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),C)| -c_Finite__Set_Ofinite(A,C)| -c_Finite__Set_Ofinite(B,C). % 47.45/47.53 ** KEPT (pick-wt=14): 14 [] c_Finite__Set_Ofinite(A,B)| -c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(A,C,tc_fun(B,tc_bool)),B)| -c_Finite__Set_Ofinite(C,B). % 47.45/47.53 ** KEPT (pick-wt=11): 15 [] c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),C)| -c_Finite__Set_Ofinite(A,C). % 47.45/47.53 ** KEPT (pick-wt=14): 16 [] -class_OrderedGroup_Oab__group__add(A)|c_HOL_Ominus__class_Ominus(B,C,A)!=c_HOL_Ominus__class_Ominus(D,D,A)|B=C. % 47.45/47.53 ** KEPT (pick-wt=14): 17 [] -class_OrderedGroup_Oab__group__add(A)|c_HOL_Ominus__class_Ominus(B,B,A)!=c_HOL_Ominus__class_Ominus(C,D,A)|C=D. % 47.45/47.53 ** KEPT (pick-wt=8): 18 [] c_Hoare__Mirabelle_Ohoare__valids(A,B,C)| -c_Hoare__Mirabelle_Ohoare__derivs(A,B,C). % 47.45/47.53 ** KEPT (pick-wt=17): 19 [] c_in(A,c_HOL_Ominus__class_Ominus(B,C,tc_fun(D,tc_bool)),D)|c_in(A,C,D)| -c_in(A,B,D). % 47.45/47.53 Following clause subsumed by 19 during input processing: 0 [] c_in(A,c_HOL_Ominus__class_Ominus(B,C,tc_fun(D,tc_bool)),D)|c_in(A,C,D)| -c_in(A,B,D). % 47.45/47.53 ** KEPT (pick-wt=21): 20 [] c_Set_Oinsert(A,c_HOL_Ominus__class_Ominus(B,c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),tc_fun(C,tc_bool)),C)=B| -c_in(A,B,C). % 47.45/47.53 ** KEPT (pick-wt=32): 21 [] c_lesse_quals(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))| -c_lesse_quals(A,C,tc_fun(D,tc_bool))| -c_lesse_quals(c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)),C,tc_fun(D,tc_bool)). % 47.45/47.53 ** KEPT (pick-wt=28): 22 [] hAPP(A,B)!=c_Option_Ooption_ONone(C)|c_HOL_Ominus__class_Ominus(c_Map_Odom(A,D,C),c_Set_Oinsert(B,E,D),tc_fun(D,tc_bool))=c_HOL_Ominus__class_Ominus(c_Map_Odom(A,D,C),E,tc_fun(D,tc_bool)). % 47.45/47.53 ** KEPT (pick-wt=12): 23 [] c_Com_Ocom_OCall(A,B,C)!=c_Com_Ocom_OCall(D,E,F)|C=F. % 47.45/47.53 ** KEPT (pick-wt=12): 24 [] c_Com_Ocom_OCall(A,B,C)!=c_Com_Ocom_OCall(D,E,F)|B=E. % 47.45/47.53 ** KEPT (pick-wt=12): 25 [] c_Com_Ocom_OCall(A,B,C)!=c_Com_Ocom_OCall(D,E,F)|A=D. % 47.45/47.53 ** KEPT (pick-wt=5): 26 [] c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OSKIP. % 47.45/47.53 ** KEPT (pick-wt=8): 27 [] c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OLocal(C,D,E). % 47.45/47.53 ** KEPT (pick-wt=7): 28 [] -class_Orderings_Obot(A)|c_lesse_quals(c_Orderings_Obot__class_Obot(A),B,A). % 47.45/47.53 ** KEPT (pick-wt=10): 29 [] c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OSemi(C,D)|B=D. % 47.45/47.53 ** KEPT (pick-wt=10): 30 [] c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OSemi(C,D)|A=C. % 47.45/47.53 ** KEPT (pick-wt=7): 31 [] c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OWhile(C,D). % 47.45/47.53 ** KEPT (pick-wt=10): 32 [] -class_Lattices_Obounded__lattice(A)|c_Lattices_Oupper__semilattice__class_Osup(B,c_Orderings_Otop__class_Otop(A),A)=c_Orderings_Otop__class_Otop(A). % 47.45/47.53 ** KEPT (pick-wt=10): 33 [] -class_Lattices_Obounded__lattice(A)|c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Otop__class_Otop(A),B,A)=c_Orderings_Otop__class_Otop(A). % 47.45/47.53 ** KEPT (pick-wt=8): 34 [] c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OCond(C,D,E). % 47.45/47.53 ** KEPT (pick-wt=9): 35 [] c_Set_Oinsert(A,B,C)!=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)). % 47.45/47.53 ** KEPT (pick-wt=8): 36 [] c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OLocal(C,D,E). % 47.45/47.53 ** KEPT (pick-wt=8): 37 [] c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OAss(D,E). % 47.45/47.53 ** KEPT (pick-wt=14): 38 [] hBOOL(hAPP(A,B))|C=B| -hBOOL(hAPP(c_Set_Oinsert(C,A,D),B)). % 47.45/47.53 ** KEPT (pick-wt=8): 39 [] c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OWhile(D,E). % 47.45/47.53 ** KEPT (pick-wt=9): 40 [] c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OLocal(D,E,F). % 47.45/47.53 ** KEPT (pick-wt=9): 41 [] c_Finite__Set_Ofinite(A,B)| -c_Finite__Set_Ofinite(c_Set_Oinsert(C,A,B),B). % 47.45/47.53 ** KEPT (pick-wt=9): 42 [] c_Finite__Set_Ofinite(c_Set_Oinsert(A,B,C),C)| -c_Finite__Set_Ofinite(B,C). % 47.45/47.53 ** KEPT (pick-wt=48): 43 [] c_Hoare__Mirabelle_Ohoare__derivs(A,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(B,hAPP(c_Com_Ocom_OBODY,C),D,E),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(E),tc_bool)),tc_Hoare__Mirabelle_Otriple(E)),E)| -c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(B,hAPP(c_Com_Ocom_OBODY,C),D,E),A,tc_Hoare__Mirabelle_Otriple(E)),c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(B,c_Option_Othe(hAPP(c_Com_Obody,C),tc_Com_Ocom),D,E),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(E),tc_bool)),tc_Hoare__Mirabelle_Otriple(E)),E). % 47.45/47.54 ** KEPT (pick-wt=8): 44 [] c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OSemi(D,E). % 47.45/47.54 ** KEPT (pick-wt=12): 45 [] c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OCond(D,E,F)|C=F. % 47.45/47.54 ** KEPT (pick-wt=12): 46 [] c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OCond(D,E,F)|B=E. % 47.45/47.54 ** KEPT (pick-wt=12): 47 [] c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OCond(D,E,F)|A=D. % 47.45/47.54 ** KEPT (pick-wt=14): 48 [] c_Finite__Set_Ofinite(c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)),C)| -c_Finite__Set_Ofinite(B,C)| -c_Finite__Set_Ofinite(A,C). % 47.45/47.54 Following clause subsumed by 48 during input processing: 0 [] c_Finite__Set_Ofinite(c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)),C)| -c_Finite__Set_Ofinite(B,C)| -c_Finite__Set_Ofinite(A,C). % 47.45/47.54 ** KEPT (pick-wt=6): 49 [] c_Option_Ooption_OSome(A,B)!=c_Option_Ooption_ONone(B). % 47.45/47.54 Following clause subsumed by 49 during input processing: 0 [] c_Option_Ooption_OSome(A,B)!=c_Option_Ooption_ONone(B). % 47.45/47.54 ** KEPT (pick-wt=9): 50 [] c_Com_Ocom_OCall(A,B,C)!=c_Com_Ocom_OCond(D,E,F). % 47.45/47.54 ** KEPT (pick-wt=10): 51 [] c_Option_Ooption_OSome(A,B)!=c_Option_Ooption_OSome(C,B)|A=C. % 47.45/47.54 ** KEPT (pick-wt=14): 52 [] hAPP(A,B)!=c_Option_Ooption_OSome(C,D)|c_in(B,c_Map_Odom(A,E,D),E). % 47.45/47.54 ** KEPT (pick-wt=7): 53 [] c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OWhile(C,D). % 47.45/47.54 ** KEPT (pick-wt=8): 54 [] c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OLocal(C,D,E). % 47.45/47.54 ** KEPT (pick-wt=17): 55 [] hBOOL(hAPP(A,B))|hBOOL(hAPP(C,B))| -hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(C,A,tc_fun(D,tc_bool)),B)). % 47.45/47.54 ** KEPT (pick-wt=13): 56 [] hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)),D))| -hBOOL(hAPP(B,D)). % 47.45/47.54 ** KEPT (pick-wt=13): 57 [] hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)),D))| -hBOOL(hAPP(A,D)). % 47.45/47.54 ** KEPT (pick-wt=17): 58 [] c_in(A,B,C)|c_in(A,D,C)| -c_in(A,c_Lattices_Oupper__semilattice__class_Osup(D,B,tc_fun(C,tc_bool)),C). % 47.45/47.54 ** KEPT (pick-wt=8): 59 [] c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OWhile(D,E). % 47.45/47.54 ** KEPT (pick-wt=13): 60 [] hAPP(A,B)!=c_Option_Ooption_ONone(C)| -c_in(B,c_Map_Odom(A,D,C),D). % 47.45/47.54 ** KEPT (pick-wt=11): 61 [] c_Finite__Set_Ofinite(A,B)| -c_Finite__Set_Ofinite(c_Lattices_Oupper__semilattice__class_Osup(A,C,tc_fun(B,tc_bool)),B). % 47.45/47.54 ** KEPT (pick-wt=11): 62 [] c_Finite__Set_Ofinite(A,B)| -c_Finite__Set_Ofinite(c_Lattices_Oupper__semilattice__class_Osup(C,A,tc_fun(B,tc_bool)),B). % 47.45/47.54 ** KEPT (pick-wt=9): 63 [] -class_Lattices_Obounded__lattice(A)|c_Lattices_Oupper__semilattice__class_Osup(B,c_Orderings_Obot__class_Obot(A),A)=B. % 47.45/47.54 ** KEPT (pick-wt=9): 64 [] -class_Lattices_Obounded__lattice(A)|c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(A),B,A)=B. % 47.45/47.54 ** KEPT (pick-wt=8): 65 [] c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OCond(C,D,E). % 47.45/47.54 ** KEPT (pick-wt=50): 66 [] c_Hoare__Mirabelle_Ohoare__derivs(A,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(B,c_Com_Ocom_OSemi(C,D),E,F),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(F),tc_bool)),tc_Hoare__Mirabelle_Otriple(F)),F)| -c_Hoare__Mirabelle_Ohoare__derivs(A,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(G,D,E,F),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(F),tc_bool)),tc_Hoare__Mirabelle_Otriple(F)),F)| -c_Hoare__Mirabelle_Ohoare__derivs(A,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(B,C,G,F),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(F),tc_bool)),tc_Hoare__Mirabelle_Otriple(F)),F). % 47.45/47.54 Following clause subsumed by 26 during input processing: 0 [flip.1] c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OSKIP. % 47.45/47.54 ** KEPT (pick-wt=7): 67 [] -hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),B)). % 47.45/47.54 ** KEPT (pick-wt=6): 69 [copy,68,flip.1] c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OSKIP. % 47.47/47.54 ** KEPT (pick-wt=9): 70 [] c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool))!=c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=58): 71 [] c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(A,B,C,tc_Com_Ostate),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)| -c_Hoare__Mirabelle_Ohoare__valids(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(A,B,C,tc_Com_Ostate),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)| -c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,B),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate). % 47.47/47.54 ** KEPT (pick-wt=21): 72 [] hAPP(A,c_Map_Osko__Map__Xfinite__map__freshness__1__1(A,B,C))=c_Option_Ooption_ONone(C)|c_Finite__Set_Ofinite(c_Orderings_Otop__class_Otop(tc_fun(B,tc_bool)),B)| -c_Finite__Set_Ofinite(c_Map_Odom(A,B,C),B). % 47.47/47.54 ** KEPT (pick-wt=30): 73 [] c_lesse_quals(c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),tc_fun(C,tc_bool)),D,tc_fun(C,tc_bool))| -c_in(B,A,C)| -c_lesse_quals(A,c_Set_Oinsert(B,D,C),tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=30): 74 [] c_lesse_quals(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))| -c_in(B,A,D)| -c_lesse_quals(c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)),C,tc_fun(D,tc_bool)). % 47.47/47.54 Following clause subsumed by 74 during input processing: 0 [] c_lesse_quals(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))| -c_in(B,A,D)| -c_lesse_quals(c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)),C,tc_fun(D,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=7): 75 [] c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OSemi(C,D). % 47.47/47.54 ** KEPT (pick-wt=15): 76 [] c_lesse_quals(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))| -c_lesse_quals(A,C,tc_fun(D,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=15): 77 [] c_lesse_quals(A,B,tc_fun(C,tc_bool))| -c_lesse_quals(c_Set_Oinsert(D,A,C),B,tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=9): 78 [] c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OCond(D,E,F). % 47.47/47.54 ** KEPT (pick-wt=9): 79 [] c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OCall(D,E,F). % 47.47/47.54 ** KEPT (pick-wt=16): 80 [] c_Finite__Set_Ofinite(A,B)| -c_lesse_quals(A,c_Set_Oimage(C,D,E,B),tc_fun(B,tc_bool))| -c_Finite__Set_Ofinite(D,E). % 47.47/47.54 ** KEPT (pick-wt=20): 81 [] c_in(hAPP(A,B),C,D)| -c_in(B,E,F)| -c_lesse_quals(c_Set_Oimage(A,E,F,D),C,tc_fun(D,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=20): 82 [] c_Set_Oimage(c_COMBK(A,B,C),D,C,B)=c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B)| -c_in(E,D,C). % 47.47/47.54 ** KEPT (pick-wt=13): 83 [] A=B| -c_in(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C). % 47.47/47.54 ** KEPT (pick-wt=8): 84 [] -class_Lattices_Oupper__semilattice(A)|c_Lattices_Oupper__semilattice__class_Osup(B,B,A)=B. % 47.47/47.54 ** KEPT (pick-wt=8): 85 [] c_Com_Ocom_OCall(A,B,C)!=c_Com_Ocom_OSemi(D,E). % 47.47/47.54 ** KEPT (pick-wt=38): 86 [] c_Hoare__Mirabelle_Ohoare__derivs(A,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(B,hAPP(c_Com_Ocom_OBODY,C),D,E),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(E),tc_bool)),tc_Hoare__Mirabelle_Otriple(E)),E)| -c_Hoare__Mirabelle_Ohoare__derivs(A,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(B,c_Option_Othe(hAPP(c_Com_Obody,C),tc_Com_Ocom),D,E),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(E),tc_bool)),tc_Hoare__Mirabelle_Otriple(E)),E). % 47.47/47.54 ** KEPT (pick-wt=8): 87 [] c_in(A,B,C)| -hBOOL(hAPP(B,A)). % 47.47/47.54 ** KEPT (pick-wt=8): 88 [] hBOOL(hAPP(A,B))| -c_in(B,A,C). % 47.47/47.54 ** KEPT (pick-wt=6): 89 [] c_Option_Ooption_ONone(A)!=c_Option_Ooption_OSome(B,A). % 47.47/47.54 Following clause subsumed by 89 during input processing: 0 [] c_Option_Ooption_ONone(A)!=c_Option_Ooption_OSome(B,A). % 47.47/47.54 ** KEPT (pick-wt=29): 90 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OWhile(A,B)),C),D))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OWhile(A,B)),E),D))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(B),C),E))| -hBOOL(hAPP(A,C)). % 47.47/47.54 ** KEPT (pick-wt=21): 91 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OCond(A,B,C)),D),E))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(B),D),E))| -hBOOL(hAPP(A,D)). % 47.47/47.54 ** KEPT (pick-wt=21): 92 [] -hBOOL(hAPP(A,B))|hBOOL(hAPP(hAPP(c_Natural_Oevalc(C),B),D))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OCond(A,C,E)),B),D)). % 47.47/47.54 ** KEPT (pick-wt=23): 93 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSemi(A,B)),C),D))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(B),E),D))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(A),C),E)). % 47.47/47.54 ** KEPT (pick-wt=17): 94 [] -class_Lattices_Oupper__semilattice(A)|c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(B,C,A),D,A)=c_Lattices_Oupper__semilattice__class_Osup(B,c_Lattices_Oupper__semilattice__class_Osup(C,D,A),A). % 47.47/47.54 ** KEPT (pick-wt=17): 95 [] -class_Lattices_Oupper__semilattice(A)|c_Lattices_Oupper__semilattice__class_Osup(B,c_Lattices_Oupper__semilattice__class_Osup(C,D,A),A)=c_Lattices_Oupper__semilattice__class_Osup(C,c_Lattices_Oupper__semilattice__class_Osup(B,D,A),A). % 47.47/47.54 ** KEPT (pick-wt=17): 96 [] -class_Lattices_Olattice(A)|c_Lattices_Oupper__semilattice__class_Osup(B,c_Lattices_Oupper__semilattice__class_Osup(C,D,A),A)=c_Lattices_Oupper__semilattice__class_Osup(C,c_Lattices_Oupper__semilattice__class_Osup(B,D,A),A). % 47.47/47.54 ** KEPT (pick-wt=17): 97 [] -class_Lattices_Olattice(A)|c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(B,C,A),D,A)=c_Lattices_Oupper__semilattice__class_Osup(B,c_Lattices_Oupper__semilattice__class_Osup(C,D,A),A). % 47.47/47.54 ** KEPT (pick-wt=23): 98 [] c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)),D,tc_fun(C,tc_bool))| -c_lesse_quals(B,D,tc_fun(C,tc_bool))| -c_lesse_quals(A,D,tc_fun(C,tc_bool)). % 47.47/47.54 Following clause subsumed by 98 during input processing: 0 [] c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)),D,tc_fun(C,tc_bool))| -c_lesse_quals(B,D,tc_fun(C,tc_bool))| -c_lesse_quals(A,D,tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=17): 99 [] -class_Lattices_Oupper__semilattice(A)|c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(B,C,A),D,A)| -c_lesse_quals(C,D,A)| -c_lesse_quals(B,D,A). % 47.47/47.54 ** KEPT (pick-wt=9): 100 [] -class_Lattices_Oupper__semilattice(A)|c_lesse_quals(B,c_Lattices_Oupper__semilattice__class_Osup(B,C,A),A). % 47.47/47.54 ** KEPT (pick-wt=9): 101 [] -class_Lattices_Oupper__semilattice(A)|c_lesse_quals(B,c_Lattices_Oupper__semilattice__class_Osup(C,B,A),A). % 47.47/47.54 Following clause subsumed by 99 during input processing: 0 [] -class_Lattices_Oupper__semilattice(A)|c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(B,C,A),D,A)| -c_lesse_quals(C,D,A)| -c_lesse_quals(B,D,A). % 47.47/47.54 Following clause subsumed by 99 during input processing: 0 [] -class_Lattices_Oupper__semilattice(A)|c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(B,C,A),D,A)| -c_lesse_quals(C,D,A)| -c_lesse_quals(B,D,A). % 47.47/47.54 ** KEPT (pick-wt=9): 102 [] -class_Lattices_Olattice(A)|c_lesse_quals(B,c_Lattices_Oupper__semilattice__class_Osup(C,B,A),A). % 47.47/47.54 ** KEPT (pick-wt=9): 103 [] -class_Lattices_Olattice(A)|c_lesse_quals(B,c_Lattices_Oupper__semilattice__class_Osup(B,C,A),A). % 47.47/47.54 ** KEPT (pick-wt=19): 104 [] hAPP(A,B)!=c_Option_Ooption_OSome(C,D)|c_Set_Oinsert(B,c_Map_Odom(A,E,D),E)=c_Map_Odom(A,E,D). % 47.47/47.54 ** KEPT (pick-wt=6): 106 [copy,105,flip.1] c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OSKIP. % 47.47/47.54 ** KEPT (pick-wt=8): 107 [] c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OCall(C,D,E). % 47.47/47.54 ** KEPT (pick-wt=18): 108 [] c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B)!=c_Set_Oinsert(C,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B)|A=C. % 47.47/47.54 ** KEPT (pick-wt=11): 109 [] -hBOOL(hAPP(A,B))| -c_in(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C). % 47.47/47.54 Following clause subsumed by 35 during input processing: 0 [] c_Set_Oinsert(A,B,C)!=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool))|c_in(A,B,C). % 47.47/47.54 ** KEPT (pick-wt=20): 110 [] c_Hoare__Mirabelle_Ohoare__derivs(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(C),tc_bool)),tc_Hoare__Mirabelle_Otriple(C)),C)| -c_Hoare__Mirabelle_Ohoare__derivs(A,c_Set_Oinsert(B,D,tc_Hoare__Mirabelle_Otriple(C)),C). % 47.47/47.54 ** KEPT (pick-wt=9): 111 [] c_Com_Ocom_OCall(A,B,C)!=c_Com_Ocom_OLocal(D,E,F). % 47.47/47.54 ** KEPT (pick-wt=13): 112 [] c_in(A,B,C)| -c_lesse_quals(c_Set_Oinsert(A,D,C),B,tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=8): 113 [] c_Com_Ocom_OCall(A,B,C)!=c_Com_Ocom_OWhile(D,E). % 47.47/47.54 ** KEPT (pick-wt=11): 114 [] hBOOL(hAPP(c_Set_Oinsert(A,B,C),D))| -hBOOL(hAPP(B,D)). % 47.47/47.54 ** KEPT (pick-wt=20): 115 [] c_Set_Oinsert(hAPP(A,B),c_Set_Oimage(A,C,D,E),E)=c_Set_Oimage(A,C,D,E)| -c_in(B,C,D). % 47.47/47.54 Following clause subsumed by 76 during input processing: 0 [] c_lesse_quals(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))| -c_lesse_quals(A,C,tc_fun(D,tc_bool))|c_in(B,A,D). % 47.47/47.54 ** KEPT (pick-wt=19): 116 [] c_lesse_quals(A,B,tc_fun(C,tc_bool))|c_in(D,A,C)| -c_lesse_quals(A,c_Set_Oinsert(D,B,C),tc_fun(C,tc_bool)). % 47.47/47.54 Following clause subsumed by 76 during input processing: 0 [] c_lesse_quals(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))| -c_lesse_quals(A,C,tc_fun(D,tc_bool))|c_in(B,A,D). % 47.47/47.54 Following clause subsumed by 116 during input processing: 0 [] c_lesse_quals(A,B,tc_fun(C,tc_bool))| -c_lesse_quals(A,c_Set_Oinsert(D,B,C),tc_fun(C,tc_bool))|c_in(D,A,C). % 47.47/47.54 ** KEPT (pick-wt=20): 117 [] c_Set_Oinsert(A,B,C)!=c_Set_Oinsert(A,D,C)|c_in(A,D,C)|c_in(A,B,C)|B=D. % 47.47/47.54 ** KEPT (pick-wt=17): 118 [] c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool))!=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool))|B=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=17): 119 [] c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool))!=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool))|A=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=13): 120 [] -class_Lattices_Obounded__lattice(A)|c_Lattices_Oupper__semilattice__class_Osup(B,C,A)!=c_Orderings_Obot__class_Obot(A)|B=c_Orderings_Obot__class_Obot(A). % 47.47/47.54 ** KEPT (pick-wt=13): 121 [] -class_Lattices_Obounded__lattice(A)|c_Lattices_Oupper__semilattice__class_Osup(B,C,A)!=c_Orderings_Obot__class_Obot(A)|C=c_Orderings_Obot__class_Obot(A). % 47.47/47.54 ** KEPT (pick-wt=23): 122 [] c_Fun_Ocomp(A,B,C,D,E)!=c_Fun_Ocomp(c_Fun_Oid(D),F,D,D,E)|hAPP(A,hAPP(B,G))=hAPP(F,G). % 47.47/47.54 ** KEPT (pick-wt=8): 123 [] c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OSemi(D,E). % 47.47/47.54 ** KEPT (pick-wt=11): 124 [] -class_Lattices_Oupper__semilattice(A)|c_Lattices_Oupper__semilattice__class_Osup(B,C,A)=c_Lattices_Oupper__semilattice__class_Osup(C,B,A). % 47.47/47.54 ** KEPT (pick-wt=11): 125 [] -class_Lattices_Olattice(A)|c_Lattices_Oupper__semilattice__class_Osup(B,C,A)=c_Lattices_Oupper__semilattice__class_Osup(C,B,A). % 47.47/47.54 ** KEPT (pick-wt=10): 126 [] c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OWhile(C,D)|A=C. % 47.47/47.54 ** KEPT (pick-wt=10): 127 [] c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OWhile(C,D)|B=D. % 47.47/47.54 ** KEPT (pick-wt=10): 128 [] c_Set_Oinsert(A,B,C)=B| -c_in(A,B,C). % 47.47/47.54 ** KEPT (pick-wt=14): 129 [] -class_Lattices_Oupper__semilattice(A)|c_Lattices_Oupper__semilattice__class_Osup(B,c_Lattices_Oupper__semilattice__class_Osup(B,C,A),A)=c_Lattices_Oupper__semilattice__class_Osup(B,C,A). % 47.47/47.54 ** KEPT (pick-wt=14): 130 [] -class_Lattices_Olattice(A)|c_Lattices_Oupper__semilattice__class_Osup(B,c_Lattices_Oupper__semilattice__class_Osup(B,C,A),A)=c_Lattices_Oupper__semilattice__class_Osup(B,C,A). % 47.47/47.54 Following clause subsumed by 106 during input processing: 0 [] c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OSKIP. % 47.47/47.54 ** KEPT (pick-wt=8): 131 [] c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OCond(C,D,E). % 47.47/47.54 ** KEPT (pick-wt=5): 132 [] -class_Finite__Set_Ofinite_Ofinite(A)|c_Finite__Set_Ofinite(B,A). % 47.47/47.54 ** KEPT (pick-wt=8): 133 [] c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OCall(C,D,E). % 47.47/47.54 ** KEPT (pick-wt=8): 134 [] c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OAss(D,E). % 47.47/47.54 ** KEPT (pick-wt=10): 135 [] A=B| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),B),A)). % 47.47/47.54 ** KEPT (pick-wt=16): 136 [] -class_HOL_Oord(A)|c_lesse_quals(hAPP(B,C),hAPP(D,C),A)| -c_lesse_quals(B,D,tc_fun(E,A)). % 47.47/47.54 ** KEPT (pick-wt=14): 137 [] c_in(A,B,C)|A=D| -c_in(A,c_Set_Oinsert(D,B,C),C). % 47.47/47.54 ** KEPT (pick-wt=8): 138 [] c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OCall(C,D,E). % 47.47/47.54 ** KEPT (pick-wt=7): 139 [] c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OAss(C,D). % 47.47/47.54 ** KEPT (pick-wt=15): 140 [] A=B| -c_lesse_quals(B,A,tc_fun(C,tc_bool))| -c_lesse_quals(A,B,tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=17): 141 [] A=B| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(C),D),A))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(C),D),B)). % 47.47/47.54 Following clause subsumed by 140 during input processing: 0 [] A=B| -c_lesse_quals(B,A,tc_fun(C,tc_bool))| -c_lesse_quals(A,B,tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=13): 142 [] -class_Orderings_Oorder(A)|B=C| -c_lesse_quals(C,B,A)| -c_lesse_quals(B,C,A). % 47.47/47.54 Following clause subsumed by 142 during input processing: 0 [] -class_Orderings_Oorder(A)|B=C| -c_lesse_quals(C,B,A)| -c_lesse_quals(B,C,A). % 47.47/47.54 Following clause subsumed by 142 during input processing: 0 [] -class_Orderings_Oorder(A)|B=C| -c_lesse_quals(B,C,A)| -c_lesse_quals(C,B,A). % 47.47/47.54 Following clause subsumed by 69 during input processing: 0 [] c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OSKIP. % 47.47/47.54 ** KEPT (pick-wt=12): 143 [] -class_Lattices_Oupper__semilattice(A)|c_Lattices_Oupper__semilattice__class_Osup(B,C,A)=B| -c_lesse_quals(C,B,A). % 47.47/47.54 ** KEPT (pick-wt=12): 144 [] -class_Lattices_Oupper__semilattice(A)|c_Lattices_Oupper__semilattice__class_Osup(B,C,A)!=C|c_lesse_quals(B,C,A). % 47.47/47.54 ** KEPT (pick-wt=12): 145 [] -class_Lattices_Oupper__semilattice(A)|c_Lattices_Oupper__semilattice__class_Osup(B,C,A)=C| -c_lesse_quals(B,C,A). % 47.47/47.54 ** KEPT (pick-wt=14): 146 [] c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool))=B| -c_lesse_quals(A,B,tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=14): 147 [] c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool))=A| -c_lesse_quals(B,A,tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=14): 148 [] c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool))!=B|c_lesse_quals(A,B,tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=27): 149 [] c_Set_Oinsert(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)!=c_Set_Oinsert(D,c_Set_Oinsert(E,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)|A=E|A=D. % 47.47/47.54 ** KEPT (pick-wt=27): 150 [] c_Set_Oinsert(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)!=c_Set_Oinsert(D,c_Set_Oinsert(E,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)|B=D|A=D. % 47.47/47.54 ** KEPT (pick-wt=27): 151 [] c_Set_Oinsert(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)!=c_Set_Oinsert(D,c_Set_Oinsert(E,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)|A=E|B=E. % 47.47/47.54 ** KEPT (pick-wt=27): 152 [] c_Set_Oinsert(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)!=c_Set_Oinsert(D,c_Set_Oinsert(E,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)|B=D|B=E. % 47.47/47.54 ** KEPT (pick-wt=23): 153 [] c_Fun_Obij__betw(c_Fun_Ocomp(A,B,C,D,E),F,G,E,D)| -c_Fun_Obij__betw(A,H,G,C,D)| -c_Fun_Obij__betw(B,F,H,E,C). % 47.47/47.54 ** KEPT (pick-wt=21): 154 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(A),B),C))|hBOOL(hAPP(D,B))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OCond(D,E,A)),B),C)). % 47.47/47.54 ** KEPT (pick-wt=21): 155 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OCond(A,B,C)),D),E))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(C),D),E))|hBOOL(hAPP(A,D)). % 47.47/47.54 ** KEPT (pick-wt=5): 157 [copy,156,flip.1] c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OSKIP. % 47.47/47.54 ** KEPT (pick-wt=14): 158 [] c_Hoare__Mirabelle_Otriple_Otriple(A,B,C,D)!=c_Hoare__Mirabelle_Otriple_Otriple(E,F,G,D)|A=E. % 47.47/47.54 ** KEPT (pick-wt=14): 159 [] c_Hoare__Mirabelle_Otriple_Otriple(A,B,C,D)!=c_Hoare__Mirabelle_Otriple_Otriple(E,F,G,D)|B=F. % 47.47/47.54 ** KEPT (pick-wt=14): 160 [] c_Hoare__Mirabelle_Otriple_Otriple(A,B,C,D)!=c_Hoare__Mirabelle_Otriple_Otriple(E,F,G,D)|C=G. % 47.47/47.54 ** KEPT (pick-wt=15): 161 [] A=c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool))| -c_lesse_quals(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),tc_fun(B,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=7): 162 [] c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OAss(C,D). % 47.47/47.54 ** KEPT (pick-wt=9): 163 [] c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))!=c_Set_Oinsert(B,C,A). % 47.47/47.54 ** KEPT (pick-wt=7): 164 [] -c_in(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B). % 47.47/47.54 Following clause subsumed by 164 during input processing: 0 [] -c_in(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B). % 47.47/47.54 Following clause subsumed by 164 during input processing: 0 [] hBOOL(hAPP(A,B))| -c_in(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C). % 47.47/47.54 Following clause subsumed by 164 during input processing: 0 [] -c_in(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B). % 47.47/47.54 ** KEPT (pick-wt=12): 165 [] c_Hoare__Mirabelle_Ohoare__derivs(A,B,C)| -c_Hoare__Mirabelle_Ohoare__derivs(A,D,C)| -c_Hoare__Mirabelle_Ohoare__derivs(D,B,C). % 47.47/47.54 ** KEPT (pick-wt=28): 166 [] c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)),c_Lattices_Oupper__semilattice__class_Osup(D,E,tc_fun(C,tc_bool)),tc_fun(C,tc_bool))| -c_lesse_quals(B,E,tc_fun(C,tc_bool))| -c_lesse_quals(A,D,tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=7): 167 [] -class_Orderings_Otop(A)|c_lesse_quals(B,c_Orderings_Otop__class_Otop(A),A). % 47.47/47.54 ** KEPT (pick-wt=10): 168 [] c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OAss(C,D)|B=D. % 47.47/47.54 ** KEPT (pick-wt=10): 169 [] c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OAss(C,D)|A=C. % 47.47/47.54 ** KEPT (pick-wt=8): 170 [] c_Com_Ocom_OCall(A,B,C)!=c_Com_Ocom_OAss(D,E). % 47.47/47.54 ** KEPT (pick-wt=5): 171 [] c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OSKIP. % 47.47/47.54 ** KEPT (pick-wt=19): 172 [] c_lesse_quals(c_Set_Oinsert(A,B,C),D,tc_fun(C,tc_bool))| -c_lesse_quals(B,D,tc_fun(C,tc_bool))| -c_in(A,D,C). % 47.47/47.54 ** KEPT (pick-wt=12): 173 [] c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OLocal(D,E,F)|C=F. % 47.47/47.54 ** KEPT (pick-wt=12): 174 [] c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OLocal(D,E,F)|B=E. % 47.47/47.54 ** KEPT (pick-wt=12): 175 [] c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OLocal(D,E,F)|A=D. % 47.47/47.54 ** KEPT (pick-wt=6): 177 [copy,176,flip.1] c_Com_Ocom_OCall(A,B,C)!=c_Com_Ocom_OSKIP. % 47.47/47.54 ** KEPT (pick-wt=7): 178 [] c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OSemi(C,D). % 47.47/47.54 Following clause subsumed by 132 during input processing: 0 [] -class_Finite__Set_Ofinite_Ofinite(A)|c_Finite__Set_Ofinite(c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool)),A). % 47.47/47.54 ** KEPT (pick-wt=13): 179 [] c_in(A,c_Lattices_Oupper__semilattice__class_Osup(B,C,tc_fun(D,tc_bool)),D)| -c_in(A,C,D). % 47.47/47.54 ** KEPT (pick-wt=13): 180 [] c_in(A,c_Lattices_Oupper__semilattice__class_Osup(B,C,tc_fun(D,tc_bool)),D)| -c_in(A,B,D). % 47.47/47.54 ** KEPT (pick-wt=16): 181 [] hBOOL(hAPP(A,B))|C=B| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OWhile(A,D)),B),C)). % 47.47/47.54 ** KEPT (pick-wt=13): 182 [] -class_Lattices_Oupper__semilattice(A)|c_lesse_quals(B,C,A)| -c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(D,B,A),C,A). % 47.47/47.54 ** KEPT (pick-wt=13): 183 [] -class_Lattices_Oupper__semilattice(A)|c_lesse_quals(B,C,A)| -c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(B,D,A),C,A). % 47.47/47.54 ** KEPT (pick-wt=13): 184 [] -class_Lattices_Oupper__semilattice(A)|c_lesse_quals(B,c_Lattices_Oupper__semilattice__class_Osup(C,D,A),A)| -c_lesse_quals(B,D,A). % 47.47/47.54 ** KEPT (pick-wt=13): 185 [] -class_Lattices_Oupper__semilattice(A)|c_lesse_quals(B,c_Lattices_Oupper__semilattice__class_Osup(C,D,A),A)| -c_lesse_quals(B,C,A). % 47.47/47.54 Following clause subsumed by 182 during input processing: 0 [] -class_Lattices_Oupper__semilattice(A)|c_lesse_quals(B,C,A)| -c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(D,B,A),C,A). % 47.47/47.54 Following clause subsumed by 183 during input processing: 0 [] -class_Lattices_Oupper__semilattice(A)|c_lesse_quals(B,C,A)| -c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(B,D,A),C,A). % 47.47/47.54 ** KEPT (pick-wt=17): 186 [] c_lesse_quals(A,B,tc_fun(C,tc_bool))| -c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(A,D,tc_fun(C,tc_bool)),B,tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=17): 187 [] c_lesse_quals(A,B,tc_fun(C,tc_bool))| -c_lesse_quals(c_Lattices_Oupper__semilattice__class_Osup(D,A,tc_fun(C,tc_bool)),B,tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=14): 188 [] -class_Orderings_Oorder(A)|c_lesse_quals(B,C,A)| -c_lesse_quals(B,D,A)| -c_lesse_quals(D,C,A). % 47.47/47.54 ** KEPT (pick-wt=14): 189 [] -class_Orderings_Opreorder(A)|c_lesse_quals(B,C,A)| -c_lesse_quals(D,C,A)| -c_lesse_quals(B,D,A). % 47.47/47.54 ** KEPT (pick-wt=14): 190 [] c_in(A,B,C)| -c_in(A,D,C)| -c_lesse_quals(D,B,tc_fun(C,tc_bool)). % 47.47/47.54 Following clause subsumed by 190 during input processing: 0 [] c_in(A,B,C)| -c_in(A,D,C)| -c_lesse_quals(D,B,tc_fun(C,tc_bool)). % 47.47/47.54 Following clause subsumed by 190 during input processing: 0 [] c_in(A,B,C)| -c_lesse_quals(D,B,tc_fun(C,tc_bool))| -c_in(A,D,C). % 47.47/47.54 Following clause subsumed by 190 during input processing: 0 [] c_in(A,B,C)| -c_in(A,D,C)| -c_lesse_quals(D,B,tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=18): 191 [] c_lesse_quals(A,B,tc_fun(C,tc_bool))| -c_lesse_quals(D,B,tc_fun(C,tc_bool))| -c_lesse_quals(A,D,tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=14): 192 [] hBOOL(hAPP(A,B))| -hBOOL(hAPP(C,B))| -c_lesse_quals(C,A,tc_fun(D,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=6): 193 [] -class_Orderings_Oorder(A)|c_lesse_quals(B,B,A). % 47.47/47.54 ** KEPT (pick-wt=6): 194 [] -class_Orderings_Opreorder(A)|c_lesse_quals(B,B,A). % 47.47/47.54 ** KEPT (pick-wt=12): 195 [] c_Finite__Set_Ofinite(A,B)| -c_Finite__Set_Ofinite(C,B)| -c_lesse_quals(A,C,tc_fun(B,tc_bool)). % 47.47/47.54 Following clause subsumed by 192 during input processing: 0 [] hBOOL(hAPP(A,B))| -c_lesse_quals(C,A,tc_fun(D,tc_bool))| -hBOOL(hAPP(C,B)). % 47.47/47.54 Following clause subsumed by 195 during input processing: 0 [] c_Finite__Set_Ofinite(A,B)| -c_lesse_quals(A,C,tc_fun(B,tc_bool))| -c_Finite__Set_Ofinite(C,B). % 47.47/47.54 Following clause subsumed by 177 during input processing: 0 [] c_Com_Ocom_OCall(A,B,C)!=c_Com_Ocom_OSKIP. % 47.47/47.54 ** KEPT (pick-wt=11): 196 [] c_in(A,c_Set_Oinsert(B,C,D),D)| -c_in(A,C,D). % 47.47/47.54 Following clause subsumed by 196 during input processing: 0 [] c_in(A,c_Set_Oinsert(B,C,D),D)| -c_in(A,C,D). % 47.47/47.54 ** KEPT (pick-wt=24): 197 [] c_Fun_Ocomp(A,B,C,D,E)!=c_Fun_Ocomp(F,G,H,D,E)|hAPP(A,hAPP(B,I))=hAPP(F,hAPP(G,I)). % 47.47/47.54 ** KEPT (pick-wt=28): 198 [] hAPP(A,hAPP(B,C))!=hAPP(D,hAPP(E,F))|hAPP(c_Fun_Ocomp(A,B,G,H,I),C)=hAPP(c_Fun_Ocomp(D,E,J,H,K),F). % 47.47/47.54 ** KEPT (pick-wt=27): 199 [] A=c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C)|A=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool))| -c_lesse_quals(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=12): 200 [] c_Hoare__Mirabelle_Ohoare__derivs(A,B,C)| -c_Hoare__Mirabelle_Ohoare__derivs(A,c_Set_Oinsert(D,B,tc_Hoare__Mirabelle_Otriple(C)),C). % 47.47/47.54 ** KEPT (pick-wt=24): 201 [] c_Hoare__Mirabelle_Ohoare__derivs(A,c_Set_Oinsert(B,C,tc_Hoare__Mirabelle_Otriple(D)),D)| -c_Hoare__Mirabelle_Ohoare__derivs(A,C,D)| -c_Hoare__Mirabelle_Ohoare__derivs(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(D),tc_bool)),tc_Hoare__Mirabelle_Otriple(D)),D). % 47.47/47.54 Following clause subsumed by 157 during input processing: 0 [] c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OSKIP. % 47.47/47.54 ** KEPT (pick-wt=18): 202 [] c_lesse_quals(c_Set_Oinsert(A,B,C),c_Set_Oinsert(A,D,C),tc_fun(C,tc_bool))| -c_lesse_quals(B,D,tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=9): 203 [] c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OCall(D,E,F). % 47.47/47.54 ** KEPT (pick-wt=24): 204 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(A),B),C))|hBOOL(hAPP(hAPP(c_Natural_Oevalc(D),B),C))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OCond(E,D,A)),B),C)). % 47.47/47.54 Following clause subsumed by 171 during input processing: 0 [flip.1] c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OSKIP. % 47.47/47.54 ** KEPT (pick-wt=10): 205 [] -class_Orderings_Olinorder(A)|c_lesse_quals(B,C,A)|c_lesse_quals(C,B,A). % 47.47/47.54 ** KEPT (pick-wt=11): 206 [] hBOOL(hAPP(c_Com_OWT,A))| -hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OCond(B,A,C))). % 47.47/47.54 ** KEPT (pick-wt=11): 207 [] hBOOL(hAPP(c_Com_OWT,A))| -hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OCond(B,C,A))). % 47.47/47.54 ** KEPT (pick-wt=20): 208 [] -c_lesse_quals(A,B,tc_fun(C,tc_bool))|c_lesse_quals(c_Set_Oimage(D,A,C,E),c_Set_Oimage(D,B,C,E),tc_fun(E,tc_bool)). % 47.47/47.54 Following clause subsumed by 208 during input processing: 0 [] c_lesse_quals(c_Set_Oimage(A,B,C,D),c_Set_Oimage(A,E,C,D),tc_fun(D,tc_bool))| -c_lesse_quals(B,E,tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=28): 209 [] hAPP(A,c_ATP__Linkup_Osko__Set__Ximage__cong__1__1(B,A,C,D,E))!=hAPP(C,c_ATP__Linkup_Osko__Set__Ximage__cong__1__1(B,A,C,D,E))|c_Set_Oimage(A,B,D,E)=c_Set_Oimage(C,B,D,E). % 47.47/47.54 ** KEPT (pick-wt=5): 210 [] hAPP(c_Com_Ocom_OBODY,A)!=c_Com_Ocom_OSKIP. % 47.47/47.54 ** KEPT (pick-wt=7): 211 [] c_Com_Ocom_OWhile(A,B)!=hAPP(c_Com_Ocom_OBODY,C). % 47.47/47.54 ** KEPT (pick-wt=16): 212 [] c_Set_Oimage(A,B,C,D)!=c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool))|B=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=20): 213 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(hAPP(c_Com_Ocom_OBODY,A)),B),C))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Option_Othe(hAPP(c_Com_Obody,A),tc_Com_Ocom)),B),C)). % 47.47/47.54 ** KEPT (pick-wt=20): 214 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Option_Othe(hAPP(c_Com_Obody,A),tc_Com_Ocom)),B),C))| -hBOOL(hAPP(hAPP(c_Natural_Oevalc(hAPP(c_Com_Ocom_OBODY,A)),B),C)). % 47.47/47.54 ** KEPT (pick-wt=13): 215 [] c_Set_Oimage(A,B,C,D)=E| -c_Fun_Obij__betw(A,B,E,C,D). % 47.47/47.54 ** KEPT (pick-wt=12): 216 [] hAPP(c_Com_Obody,A)!=c_Option_Ooption_OSome(B,tc_Com_Ocom)| -c_Com_OWT__bodies|hBOOL(hAPP(c_Com_OWT,B)). % 47.47/47.54 ** KEPT (pick-wt=14): 217 [] hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OSemi(A,B)))| -hBOOL(hAPP(c_Com_OWT,B))| -hBOOL(hAPP(c_Com_OWT,A)). % 47.47/47.54 ** KEPT (pick-wt=10): 218 [] hBOOL(hAPP(c_Com_OWT,A))| -hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OSemi(A,B))). % 47.47/47.54 ** KEPT (pick-wt=10): 219 [] hBOOL(hAPP(c_Com_OWT,A))| -hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OSemi(B,A))). % 47.47/47.54 ** KEPT (pick-wt=10): 220 [] c_Finite__Set_Ofinite(c_Set_Oimage(A,B,C,D),D)| -c_Finite__Set_Ofinite(B,C). % 47.47/47.54 ** KEPT (pick-wt=12): 221 [] c_Com_OWT__bodies| -c_split(c_COMBK(c_Com_OWT,tc_fun(tc_Com_Ocom,tc_bool),tc_Com_Opname),c_Com_Osko__Com__XWT__bodies__def__1__1,tc_Com_Opname,tc_Com_Ocom,tc_bool). % 47.47/47.54 ** KEPT (pick-wt=8): 222 [] hAPP(c_Com_Ocom_OBODY,A)!=c_Com_Ocom_OCond(B,C,D). % 47.47/47.54 ** KEPT (pick-wt=8): 223 [] c_Com_Ocom_OCond(A,B,C)!=hAPP(c_Com_Ocom_OBODY,D). % 47.47/47.54 ** KEPT (pick-wt=15): 224 [] hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OCond(A,B,C)))| -hBOOL(hAPP(c_Com_OWT,C))| -hBOOL(hAPP(c_Com_OWT,B)). % 47.47/47.54 ** KEPT (pick-wt=36): 225 [] c_Hoare__Mirabelle_Ohoare__derivs(A,c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,B),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)| -hBOOL(hAPP(c_Com_OWT,B))| -c_Hoare__Mirabelle_Ohoare__derivs(A,c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_sko__Hoare__Mirabelle__XMGF__lemma1__1(A))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)| -c_Hoare__Mirabelle_Ostate__not__singleton. % 47.47/47.54 ** KEPT (pick-wt=5): 226 [] v_sko__Hoare__Mirabelle__Xsingle__stateE__1(A)!=A| -c_Hoare__Mirabelle_Ostate__not__singleton. % 47.47/47.54 ** KEPT (pick-wt=7): 227 [] hAPP(c_Com_Ocom_OBODY,A)!=c_Com_Ocom_OAss(B,C). % 47.47/47.54 ** KEPT (pick-wt=7): 228 [] c_Com_Ocom_OAss(A,B)!=hAPP(c_Com_Ocom_OBODY,C). % 47.47/47.54 ** KEPT (pick-wt=16): 229 [] c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))!=c_Set_Oimage(B,C,D,A)|C=c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)). % 47.47/47.54 ** KEPT (pick-wt=8): 230 [] hAPP(c_Com_Ocom_OBODY,A)!=c_Com_Ocom_OLocal(B,C,D). % 47.47/47.54 ** KEPT (pick-wt=7): 231 [] hAPP(c_Com_Ocom_OBODY,A)!=c_Com_Ocom_OWhile(B,C). % 47.47/47.54 ** KEPT (pick-wt=14): 233 [copy,232,flip.1] c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(A),tc_Com_Ocom)=hAPP(c_Com_Obody,A)| -hBOOL(hAPP(c_Com_OWT,hAPP(c_Com_Ocom_OBODY,A))). % 47.47/47.54 ** KEPT (pick-wt=12): 234 [] c_Com_OWT__bodies| -c_split(c_COMBK(c_Com_OWT,tc_fun(tc_Com_Ocom,tc_bool),tc_Com_Opname),c_Com_Osko__Com__XWT__bodies__def__raw__1__1,tc_Com_Opname,tc_Com_Ocom,tc_bool). % 47.47/47.54 ** KEPT (pick-wt=42): 235 [] c_Hoare__Mirabelle_Ohoare__derivs(A,c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,B)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)| -c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,B)),A,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,c_Option_Othe(hAPP(c_Com_Obody,B),tc_Com_Ocom)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate). % 47.47/47.54 ** KEPT (pick-wt=8): 236 [] c_Com_Ocom_OCall(A,B,C)!=hAPP(c_Com_Ocom_OBODY,D). % 47.47/47.55 ** KEPT (pick-wt=25): 237 [] c_Finite__Set_Ofinite(c_Set_Oimage(c_COMBB(A,B,C,D,E),c_Orderings_Otop__class_Otop(tc_fun(E,tc_bool)),E,D),D)| -c_Finite__Set_Ofinite(c_Set_Oimage(B,c_Orderings_Otop__class_Otop(tc_fun(E,tc_bool)),E,C),C). % 47.47/47.55 ** KEPT (pick-wt=7): 238 [] hAPP(c_Com_Ocom_OBODY,A)!=c_Com_Ocom_OSemi(B,C). % 47.47/47.55 ** KEPT (pick-wt=7): 239 [] c_Com_Ocom_OSemi(A,B)!=hAPP(c_Com_Ocom_OBODY,C). % 47.47/47.55 ** KEPT (pick-wt=13): 240 [] hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OCall(A,B,C)))| -hBOOL(hAPP(c_Com_OWT,hAPP(c_Com_Ocom_OBODY,B))). % 47.47/47.55 ** KEPT (pick-wt=13): 241 [] hBOOL(hAPP(c_Com_OWT,hAPP(c_Com_Ocom_OBODY,A)))| -hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OCall(B,A,C))). % 47.47/47.55 ** KEPT (pick-wt=8): 242 [] c_Com_Ocom_OLocal(A,B,C)!=hAPP(c_Com_Ocom_OBODY,D). % 47.47/47.55 ** KEPT (pick-wt=8): 243 [] hAPP(c_Com_Ocom_OBODY,A)!=c_Com_Ocom_OCall(B,C,D). % 47.47/47.55 ** KEPT (pick-wt=27): 244 [] c_Hoare__Mirabelle_Ohoare__derivs(A,c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,B),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)| -hBOOL(hAPP(c_Com_OWT,B))|c_in(v_sko__Hoare__Mirabelle__XMGF__lemma1__1(A),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)| -c_Hoare__Mirabelle_Ostate__not__singleton. % 47.47/47.55 ** KEPT (pick-wt=10): 245 [] hAPP(c_Com_Ocom_OBODY,A)!=hAPP(c_Com_Ocom_OBODY,B)|A=B. % 47.47/47.55 ** KEPT (pick-wt=10): 246 [] hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OWhile(A,B)))| -hBOOL(hAPP(c_Com_OWT,B)). % 47.47/47.55 ** KEPT (pick-wt=10): 247 [] hBOOL(hAPP(c_Com_OWT,A))| -hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OWhile(B,A))). % 47.47/47.55 ** KEPT (pick-wt=11): 248 [] hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OLocal(A,B,C)))| -hBOOL(hAPP(c_Com_OWT,C)). % 47.47/47.55 ** KEPT (pick-wt=11): 249 [] hBOOL(hAPP(c_Com_OWT,A))| -hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OLocal(B,C,A))). % 47.47/47.55 Following clause subsumed by 210 during input processing: 0 [flip.1] hAPP(c_Com_Ocom_OBODY,A)!=c_Com_Ocom_OSKIP. % 47.47/47.55 ** KEPT (pick-wt=14): 250 [] -c_in(A,B,C)|c_in(hAPP(D,A),c_Set_Oimage(D,B,C,E),E). % 47.47/47.55 Following clause subsumed by 250 during input processing: 0 [] -c_in(A,B,C)|c_in(hAPP(D,A),c_Set_Oimage(D,B,C,E),E). % 47.47/47.55 Following clause subsumed by 250 during input processing: 0 [] c_in(hAPP(A,B),c_Set_Oimage(A,C,D,E),E)| -c_in(B,C,D). % 47.47/47.55 Following clause subsumed by 250 during input processing: 0 [] c_in(hAPP(A,B),c_Set_Oimage(A,C,D,E),E)| -c_in(B,C,D). % 47.47/47.55 ** KEPT (pick-wt=17): 252 [copy,251,flip.1] c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate))!=v_uG. % 47.47/47.55 ** KEPT (pick-wt=6): 253 [] class_Lattices_Oupper__semilattice(tc_fun(A,B))| -class_Lattices_Olattice(B). % 47.47/47.55 ** KEPT (pick-wt=6): 254 [] class_Lattices_Obounded__lattice(tc_fun(A,B))| -class_Lattices_Obounded__lattice(B). % 47.47/47.55 ** KEPT (pick-wt=8): 255 [] class_Finite__Set_Ofinite_Ofinite(tc_fun(A,B))| -class_Finite__Set_Ofinite_Ofinite(B)| -class_Finite__Set_Ofinite_Ofinite(A). % 47.47/47.55 ** KEPT (pick-wt=6): 256 [] class_Orderings_Opreorder(tc_fun(A,B))| -class_Orderings_Opreorder(B). % 47.47/47.55 ** KEPT (pick-wt=6): 257 [] class_Lattices_Olattice(tc_fun(A,B))| -class_Lattices_Olattice(B). % 47.47/47.55 ** KEPT (pick-wt=6): 258 [] class_Orderings_Oorder(tc_fun(A,B))| -class_Orderings_Oorder(B). % 47.47/47.55 ** KEPT (pick-wt=6): 259 [] class_Orderings_Otop(tc_fun(A,B))| -class_Orderings_Otop(B). % 47.47/47.55 ** KEPT (pick-wt=6): 260 [] class_Orderings_Obot(tc_fun(A,B))| -class_Orderings_Obot(B). % 47.47/47.55 ** KEPT (pick-wt=6): 261 [] class_HOL_Oord(tc_fun(A,B))| -class_HOL_Oord(B). % 47.47/47.55 ** KEPT (pick-wt=5): 262 [] class_Finite__Set_Ofinite_Ofinite(tc_Option_Ooption(A))| -class_Finite__Set_Ofinite_Ofinite(A). % 47.47/47.55 ** KEPT (pick-wt=10): 263 [] A=B| -hBOOL(hAPP(hAPP(c_fe_qual(C),A),B)). % 47.47/47.55 15 back subsumes 13. % 47.47/47.55 Following clause subsumed by 59 during input processing: 0 [copy,27,flip.1] c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OWhile(D,E). % 47.47/47.55 Following clause subsumed by 178 during input processing: 0 [copy,31,flip.1] c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OSemi(C,D). % 47.47/47.55 Following clause subsumed by 44 during input processing: 0 [copy,34,flip.1] c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OSemi(D,E). % 47.47/47.55 Following clause subsumed by 163 during input processing: 0 [copy,35,flip.1] c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))!=c_Set_Oinsert(B,C,A). % 47.47/47.55 Following clause subsumed by 123 during input processing: 0 [copy,36,flip.1] c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OSemi(D,E). % 47.47/47.55 Following clause subsumed by 54 during input processing: 0 [copy,37,flip.1] c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OLocal(C,D,E). % 47.47/47.55 Following clause subsumed by 131 during input processing: 0 [copy,39,flip.1] c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OCond(C,D,E). % 47.47/47.55 Following clause subsumed by 78 during input processing: 0 [copy,40,flip.1] c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OCond(D,E,F). % 47.47/47.55 Following clause subsumed by 34 during input processing: 0 [copy,44,flip.1] c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OCond(C,D,E). % 47.47/47.55 Following clause subsumed by 89 during input processing: 0 [copy,49,flip.1] c_Option_Ooption_ONone(A)!=c_Option_Ooption_OSome(B,A). % 47.47/47.55 Following clause subsumed by 79 during input processing: 0 [copy,50,flip.1] c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OCall(D,E,F). % 47.47/47.55 Following clause subsumed by 162 during input processing: 0 [copy,53,flip.1] c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OAss(C,D). % 47.47/47.55 Following clause subsumed by 37 during input processing: 0 [copy,54,flip.1] c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OAss(D,E). % 47.47/47.55 Following clause subsumed by 27 during input processing: 0 [copy,59,flip.1] c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OLocal(C,D,E). % 47.47/47.55 Following clause subsumed by 134 during input processing: 0 [copy,65,flip.1] c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OAss(D,E). % 47.47/47.55 Following clause subsumed by 139 during input processing: 0 [copy,75,flip.1] c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OAss(C,D). % 47.47/47.55 76 back subsumes 21. % 47.47/47.55 Following clause subsumed by 40 during input processing: 0 [copy,78,flip.1] c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OLocal(D,E,F). % 47.47/47.55 Following clause subsumed by 50 during input processing: 0 [copy,79,flip.1] c_Com_Ocom_OCall(A,B,C)!=c_Com_Ocom_OCond(D,E,F). % 47.47/47.55 Following clause subsumed by 133 during input processing: 0 [copy,85,flip.1] c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OCall(C,D,E). % 47.47/47.55 Following clause subsumed by 49 during input processing: 0 [copy,89,flip.1] c_Option_Ooption_OSome(A,B)!=c_Option_Ooption_ONone(B). % 47.47/47.55 Following clause subsumed by 170 during input processing: 0 [copy,107,flip.1] c_Com_Ocom_OCall(A,B,C)!=c_Com_Ocom_OAss(D,E). % 47.47/47.55 Following clause subsumed by 203 during input processing: 0 [copy,111,flip.1] c_Com_Ocom_OLocal(A,B,C)!=c_Com_Ocom_OCall(D,E,F). % 47.47/47.55 Following clause subsumed by 138 during input processing: 0 [copy,113,flip.1] c_Com_Ocom_OWhile(A,B)!=c_Com_Ocom_OCall(C,D,E). % 47.47/47.55 Following clause subsumed by 36 during input processing: 0 [copy,123,flip.1] c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OLocal(C,D,E). % 47.47/47.55 Following clause subsumed by 39 during input processing: 0 [copy,131,flip.1] c_Com_Ocom_OCond(A,B,C)!=c_Com_Ocom_OWhile(D,E). % 47.47/47.55 Following clause subsumed by 85 during input processing: 0 [copy,133,flip.1] c_Com_Ocom_OCall(A,B,C)!=c_Com_Ocom_OSemi(D,E). % 47.47/47.55 Following clause subsumed by 65 during input processing: 0 [copy,134,flip.1] c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OCond(C,D,E). % 47.47/47.55 Following clause subsumed by 113 during input processing: 0 [copy,138,flip.1] c_Com_Ocom_OCall(A,B,C)!=c_Com_Ocom_OWhile(D,E). % 47.47/47.55 Following clause subsumed by 75 during input processing: 0 [copy,139,flip.1] c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OSemi(C,D). % 47.47/47.55 Following clause subsumed by 53 during input processing: 0 [copy,162,flip.1] c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OWhile(C,D). % 47.47/47.55 Following clause subsumed by 35 during input processing: 0 [copy,163,flip.1] c_Set_Oinsert(A,B,C)!=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)). % 47.47/47.55 164 back subsumes 109. % 47.47/47.55 Following clause subsumed by 107 during input processing: 0 [copy,170,flip.1] c_Com_Ocom_OAss(A,B)!=c_Com_Ocom_OCall(C,D,E). % 47.47/47.55 Following clause subsumed by 31 during input processing: 0 [copy,178,flip.1] c_Com_Ocom_OSemi(A,B)!=c_Com_Ocom_OWhile(C,D). % 47.47/47.55 Following clause subsumed by 111 during input processing: 0 [copy,203,flip.1] c_Com_Ocom_OCall(A,B,C)!=c_Com_Ocom_OLocal(D,E,F). % 47.47/47.55 Following clause subsumed by 231 during input processing: 0 [copy,211,flip.1] hAPP(c_Com_Ocom_OBODY,A)!=c_Com_Ocom_OWhile(B,C). % 47.47/47.55 Following clause subsumed by 223 during input processing: 0 [copy,222,flip.1] c_Com_Ocom_OCond(A,B,C)!=hAPP(c_Com_Ocom_OBODY,D). % 47.47/47.55 Following clause subsumed by 222 during input processing: 0 [copy,223,flip.1] hAPP(c_Com_Ocom_OBODY,A)!=c_Com_Ocom_OCond(B,C,D). % 47.47/47.55 Following clause subsumed by 228 during input processing: 0 [copy,227,flip.1] c_Com_Ocom_OAss(A,B)!=hAPP(c_Com_Ocom_OBODY,C). % 47.47/47.55 Following clause subsumed by 227 during input processing: 0 [copy,228,flip.1] hAPP(c_Com_Ocom_OBODY,A)!=c_Com_Ocom_OAss(B,C). % 47.47/47.55 Following clause subsumed by 242 during input processing: 0 [copy,230,flip.1] c_Com_Ocom_OLocal(A,B,C)!=hAPP(c_Com_Ocom_OBODY,D). % 47.47/47.55 Following clause subsumed by 211 during input processing: 0 [copy,231,flip.1] c_Com_Ocom_OWhile(A,B)!=hAPP(c_Com_Ocom_OBODY,C). % 47.47/47.55 Following clause subsumed by 243 during input processing: 0 [copy,236,flip.1] hAPP(c_Com_Ocom_OBODY,A)!=c_Com_Ocom_OCall(B,C,D). % 47.47/47.55 Following clause subsumed by 239 during input processing: 0 [copy,238,flip.1] c_Com_Ocom_OSemi(A,B)!=hAPP(c_Com_Ocom_OBODY,C). % 47.47/47.55 Following clause subsumed by 238 during input processing: 0 [copy,239,flip.1] hAPP(c_Com_Ocom_OBODY,A)!=c_Com_Ocom_OSemi(B,C). % 47.47/47.55 Following clause subsumed by 230 during input processing: 0 [copy,242,flip.1] hAPP(c_Com_Ocom_OBODY,A)!=c_Com_Ocom_OLocal(B,C,D). % 47.47/47.55 Following clause subsumed by 236 during input processing: 0 [copy,243,flip.1] c_Com_Ocom_OCall(A,B,C)!=hAPP(c_Com_Ocom_OBODY,D). % 47.47/47.55 % 47.47/47.55 ------------> process sos: % 47.47/47.55 ** KEPT (pick-wt=3): 291 [] A=A. % 47.47/47.55 ** KEPT (pick-wt=28): 292 [] c_lesse_quals(c_HOL_Ominus__class_Ominus(c_Set_Oimage(A,B,C,D),c_Set_Oimage(A,E,C,D),tc_fun(D,tc_bool)),c_Set_Oimage(A,c_HOL_Ominus__class_Ominus(B,E,tc_fun(C,tc_bool)),C,D),tc_fun(D,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=14): 293 [] c_HOL_Ominus__class_Ominus(A,c_Orderings_Otop__class_Otop(tc_fun(B,tc_bool)),tc_fun(B,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)). % 47.47/47.55 ---> New Demodulator: 294 [new_demod,293] c_HOL_Ominus__class_Ominus(A,c_Orderings_Otop__class_Otop(tc_fun(B,tc_bool)),tc_fun(B,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=27): 295 [] c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))=c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)),C,tc_fun(D,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=27): 296 [] c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))=c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,C,tc_fun(D,tc_bool)),c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=20): 297 [] c_Set_Oinsert(A,c_HOL_Ominus__class_Ominus(B,c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),tc_fun(C,tc_bool)),C)=c_Set_Oinsert(A,B,C). % 47.47/47.55 ---> New Demodulator: 298 [new_demod,297] c_Set_Oinsert(A,c_HOL_Ominus__class_Ominus(B,c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),tc_fun(C,tc_bool)),C)=c_Set_Oinsert(A,B,C). % 47.47/47.55 ** KEPT (pick-wt=23): 300 [copy,299,flip.1] c_Set_Oinsert(A,c_HOL_Ominus__class_Ominus(B,C,tc_fun(D,tc_bool)),D)=c_HOL_Ominus__class_Ominus(c_Set_Oinsert(A,B,D),C,tc_fun(D,tc_bool))|c_in(A,C,D). % 47.47/47.55 ** KEPT (pick-wt=14): 301 [] c_HOL_Ominus__class_Ominus(c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),B,tc_fun(A,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)). % 47.47/47.55 ---> New Demodulator: 302 [new_demod,301] c_HOL_Ominus__class_Ominus(c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),B,tc_fun(A,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=11): 303 [] c_HOL_Ominus__class_Ominus(A,A,tc_fun(B,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=11): 304 [] c_HOL_Ominus__class_Ominus(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),tc_fun(B,tc_bool))=A. % 47.47/47.55 ---> New Demodulator: 305 [new_demod,304] c_HOL_Ominus__class_Ominus(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),tc_fun(B,tc_bool))=A. % 47.47/47.55 ** KEPT (pick-wt=18): 306 [] c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),B,tc_fun(C,tc_bool))=c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)). % 47.47/47.55 ---> New Demodulator: 307 [new_demod,306] c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),B,tc_fun(C,tc_bool))=c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=11): 308 [] c_lesse_quals(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),A,tc_fun(C,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=18): 309 [] c_Lattices_Oupper__semilattice__class_Osup(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),B,tc_fun(C,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)). % 47.47/47.55 ---> New Demodulator: 310 [new_demod,309] c_Lattices_Oupper__semilattice__class_Osup(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),B,tc_fun(C,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=18): 311 [] c_Lattices_Oupper__semilattice__class_Osup(A,c_HOL_Ominus__class_Ominus(B,A,tc_fun(C,tc_bool)),tc_fun(C,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)). % 47.47/47.55 ---> New Demodulator: 312 [new_demod,311] c_Lattices_Oupper__semilattice__class_Osup(A,c_HOL_Ominus__class_Ominus(B,A,tc_fun(C,tc_bool)),tc_fun(C,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=28): 314 [copy,313,flip.1] c_Lattices_Oupper__semilattice__class_Osup(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),c_HOL_Ominus__class_Ominus(D,B,tc_fun(C,tc_bool)),tc_fun(C,tc_bool))=c_HOL_Ominus__class_Ominus(c_Lattices_Oupper__semilattice__class_Osup(A,D,tc_fun(C,tc_bool)),B,tc_fun(C,tc_bool)). % 47.47/47.55 ---> New Demodulator: 315 [new_demod,314] c_Lattices_Oupper__semilattice__class_Osup(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),c_HOL_Ominus__class_Ominus(D,B,tc_fun(C,tc_bool)),tc_fun(C,tc_bool))=c_HOL_Ominus__class_Ominus(c_Lattices_Oupper__semilattice__class_Osup(A,D,tc_fun(C,tc_bool)),B,tc_fun(C,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=21): 316 [] c_HOL_Ominus__class_Ominus(c_Set_Oinsert(A,B,C),c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),tc_fun(C,tc_bool))=B|c_in(A,B,C). % 47.47/47.55 ** KEPT (pick-wt=43): 318 [copy,317,flip.1] hAPP(hAPP(hAPP(hAPP(A,B),C),c_Com_Ocom_Ocom__rec(D,E,F,A,G,H,I,J,B,K)),c_Com_Ocom_Ocom__rec(D,E,F,A,G,H,I,J,C,K))=c_Com_Ocom_Ocom__rec(D,E,F,A,G,H,I,J,c_Com_Ocom_OSemi(B,C),K). % 47.47/47.55 ---> New Demodulator: 319 [new_demod,318] hAPP(hAPP(hAPP(hAPP(A,B),C),c_Com_Ocom_Ocom__rec(D,E,F,A,G,H,I,J,B,K)),c_Com_Ocom_Ocom__rec(D,E,F,A,G,H,I,J,C,K))=c_Com_Ocom_Ocom__rec(D,E,F,A,G,H,I,J,c_Com_Ocom_OSemi(B,C),K). % 47.47/47.55 ** KEPT (pick-wt=13): 320 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OWhile(A,B)),C),C))|hBOOL(hAPP(A,C)). % 47.47/47.55 ** KEPT (pick-wt=19): 322 [copy,321,flip.1] c_Set_Oinsert(A,c_Lattices_Oupper__semilattice__class_Osup(B,C,tc_fun(D,tc_bool)),D)=c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(A,B,D),C,tc_fun(D,tc_bool)). % 47.47/47.55 ---> New Demodulator: 323 [new_demod,322] c_Set_Oinsert(A,c_Lattices_Oupper__semilattice__class_Osup(B,C,tc_fun(D,tc_bool)),D)=c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(A,B,D),C,tc_fun(D,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=19): 325 [copy,324,demod,323] c_Lattices_Oupper__semilattice__class_Osup(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(B,A,D),C,tc_fun(D,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=9): 326 [] c_lesse_quals(c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),B,tc_fun(A,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=14): 327 [] c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool)),B,tc_fun(A,tc_bool))=c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool)). % 47.47/47.55 ---> New Demodulator: 328 [new_demod,327] c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool)),B,tc_fun(A,tc_bool))=c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=14): 329 [] c_Lattices_Oupper__semilattice__class_Osup(A,c_Orderings_Otop__class_Otop(tc_fun(B,tc_bool)),tc_fun(B,tc_bool))=c_Orderings_Otop__class_Otop(tc_fun(B,tc_bool)). % 47.47/47.55 ---> New Demodulator: 330 [new_demod,329] c_Lattices_Oupper__semilattice__class_Osup(A,c_Orderings_Otop__class_Otop(tc_fun(B,tc_bool)),tc_fun(B,tc_bool))=c_Orderings_Otop__class_Otop(tc_fun(B,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=12): 331 [] c_Set_Oinsert(A,c_Set_Oinsert(A,B,C),C)=c_Set_Oinsert(A,B,C). % 47.47/47.55 ---> New Demodulator: 332 [new_demod,331] c_Set_Oinsert(A,c_Set_Oinsert(A,B,C),C)=c_Set_Oinsert(A,B,C). % 47.47/47.55 ** KEPT (pick-wt=9): 333 [] c_lesse_quals(A,c_Set_Oinsert(B,A,C),tc_fun(C,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=6): 334 [] c_Finite__Set_Ofinite(c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),A). % 47.47/47.55 ** KEPT (pick-wt=7): 335 [] c_in(A,c_Orderings_Otop__class_Otop(tc_fun(B,tc_bool)),B). % 47.47/47.55 ** KEPT (pick-wt=14): 336 [] hAPP(c_Fun_Ocomp(A,B,C,D,E),F)=hAPP(A,hAPP(B,F)). % 47.47/47.55 ---> New Demodulator: 337 [new_demod,336] hAPP(c_Fun_Ocomp(A,B,C,D,E),F)=hAPP(A,hAPP(B,F)). % 47.47/47.55 Following clause subsumed by 291 during input processing: 0 [demod,337] hAPP(A,hAPP(B,C))=hAPP(A,hAPP(B,C)). % 47.47/47.55 ** KEPT (pick-wt=13): 338 [] c_Com_Ocom_Ocom__case(A,B,C,D,E,F,G,H,c_Com_Ocom_OSKIP,I)=A. % 47.47/47.55 ---> New Demodulator: 339 [new_demod,338] c_Com_Ocom_Ocom__case(A,B,C,D,E,F,G,H,c_Com_Ocom_OSKIP,I)=A. % 47.47/47.55 ** KEPT (pick-wt=13): 340 [] c_in(A,c_Map_Odom(B,C,D),C)|hAPP(B,A)=c_Option_Ooption_ONone(D). % 47.47/47.55 ** KEPT (pick-wt=11): 341 [] c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),B,tc_fun(A,tc_bool))=B. % 47.47/47.55 ---> New Demodulator: 342 [new_demod,341] c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),B,tc_fun(A,tc_bool))=B. % 47.47/47.55 ** KEPT (pick-wt=11): 343 [] c_Lattices_Oupper__semilattice__class_Osup(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),tc_fun(B,tc_bool))=A. % 47.47/47.55 ---> New Demodulator: 344 [new_demod,343] c_Lattices_Oupper__semilattice__class_Osup(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),tc_fun(B,tc_bool))=A. % 47.47/47.55 ** KEPT (pick-wt=8): 345 [] c_Hoare__Mirabelle_Ohoare__derivs(A,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(B),tc_bool)),B). % 47.47/47.55 ** KEPT (pick-wt=22): 346 [] c_Set_Oimage(c_COMBK(A,B,C),D,C,B)=c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B)|D=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=7): 347 [] hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool)),B)). % 47.47/47.55 ** KEPT (pick-wt=20): 348 [] c_Set_Oimage(A,B,C,D)=c_Set_Oimage(E,B,C,D)|c_in(c_ATP__Linkup_Osko__Set__Ximage__cong__1__1(B,A,E,C,D),B,C). % 47.47/47.55 ** KEPT (pick-wt=34): 350 [copy,349,flip.1] hAPP(hAPP(hAPP(hAPP(A,B),C),D),c_Com_Ocom_Ocom__rec(E,F,A,G,H,I,J,K,D,L))=c_Com_Ocom_Ocom__rec(E,F,A,G,H,I,J,K,c_Com_Ocom_OLocal(B,C,D),L). % 47.47/47.55 ---> New Demodulator: 351 [new_demod,350] hAPP(hAPP(hAPP(hAPP(A,B),C),D),c_Com_Ocom_Ocom__rec(E,F,A,G,H,I,J,K,D,L))=c_Com_Ocom_Ocom__rec(E,F,A,G,H,I,J,K,c_Com_Ocom_OLocal(B,C,D),L). % 47.47/47.55 ** KEPT (pick-wt=13): 352 [] c_Com_Ocom_Ocom__rec(A,B,C,D,E,F,G,H,c_Com_Ocom_OSKIP,I)=A. % 47.47/47.55 ---> New Demodulator: 353 [new_demod,352] c_Com_Ocom_Ocom__rec(A,B,C,D,E,F,G,H,c_Com_Ocom_OSKIP,I)=A. % 47.47/47.55 ** KEPT (pick-wt=9): 354 [] c_Fun_Ocomp(A,c_Fun_Oid(B),B,C,B)=A. % 47.47/47.55 ---> New Demodulator: 355 [new_demod,354] c_Fun_Ocomp(A,c_Fun_Oid(B),B,C,B)=A. % 47.47/47.55 ** KEPT (pick-wt=9): 356 [] c_Fun_Ocomp(c_Fun_Oid(A),B,A,A,C)=B. % 47.47/47.55 ---> New Demodulator: 357 [new_demod,356] c_Fun_Ocomp(c_Fun_Oid(A),B,A,A,C)=B. % 47.47/47.55 ** KEPT (pick-wt=8): 358 [] c_Lattices_Oupper__semilattice__class_Osup(A,A,tc_fun(B,tc_bool))=A. % 47.47/47.55 ---> New Demodulator: 359 [new_demod,358] c_Lattices_Oupper__semilattice__class_Osup(A,A,tc_fun(B,tc_bool))=A. % 47.47/47.55 ** KEPT (pick-wt=7): 360 [] c_in(A,c_Set_Oinsert(A,B,C),C). % 47.47/47.55 Following clause subsumed by 360 during input processing: 0 [] c_in(A,c_Set_Oinsert(A,B,C),C). % 47.47/47.55 Following clause subsumed by 360 during input processing: 0 [] c_in(A,c_Set_Oinsert(A,B,C),C). % 47.47/47.55 ** KEPT (pick-wt=22): 361 [] c_Com_Ocom_Ocom__case(A,B,C,D,E,F,G,H,c_Com_Ocom_OCall(I,J,K),L)=hAPP(hAPP(hAPP(H,I),J),K). % 47.47/47.55 ** KEPT (pick-wt=15): 362 [] c_Set_Oinsert(A,c_Set_Oinsert(B,C,D),D)=c_Set_Oinsert(B,c_Set_Oinsert(A,C,D),D). % 47.47/47.55 ** KEPT (pick-wt=6): 363 [] hAPP(c_COMBI(A),B)=B. % 47.47/47.55 ---> New Demodulator: 364 [new_demod,363] hAPP(c_COMBI(A),B)=B. % 47.47/47.55 ** KEPT (pick-wt=8): 365 [] hAPP(c_COMBK(A,B,C),D)=A. % 47.47/47.55 ---> New Demodulator: 366 [new_demod,365] hAPP(c_COMBK(A,B,C),D)=A. % 47.47/47.55 ** KEPT (pick-wt=19): 367 [] c_Com_Ocom_Ocom__case(A,B,C,D,E,F,G,H,c_Com_Ocom_OAss(I,J),K)=hAPP(hAPP(B,I),J). % 47.47/47.55 ** KEPT (pick-wt=13): 368 [] c_in(hAPP(A,B),c_Set_Oimage(A,c_Orderings_Otop__class_Otop(tc_fun(C,tc_bool)),C,D),D). % 47.47/47.55 Following clause subsumed by 362 during input processing: 0 [] c_Set_Oinsert(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)=c_Set_Oinsert(B,c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C). % 47.47/47.55 ** KEPT (pick-wt=23): 369 [] c_Lattices_Oupper__semilattice__class_Osup(A,c_Lattices_Oupper__semilattice__class_Osup(B,C,tc_fun(D,tc_bool)),tc_fun(D,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(B,c_Lattices_Oupper__semilattice__class_Osup(A,C,tc_fun(D,tc_bool)),tc_fun(D,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=23): 370 [] c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)),D,tc_fun(C,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(A,c_Lattices_Oupper__semilattice__class_Osup(B,D,tc_fun(C,tc_bool)),tc_fun(C,tc_bool)). % 47.47/47.55 ---> New Demodulator: 371 [new_demod,370] c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)),D,tc_fun(C,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(A,c_Lattices_Oupper__semilattice__class_Osup(B,D,tc_fun(C,tc_bool)),tc_fun(C,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=11): 372 [] c_lesse_quals(A,c_Lattices_Oupper__semilattice__class_Osup(B,A,tc_fun(C,tc_bool)),tc_fun(C,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=11): 373 [] c_lesse_quals(A,c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)),tc_fun(C,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=16): 374 [] c_Set_Oimage(c_COMBK(A,B,C),c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C,B)=c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=19): 375 [] c_Com_Ocom_Ocom__case(A,B,C,D,E,F,G,H,c_Com_Ocom_OSemi(I,J),K)=hAPP(hAPP(D,I),J). % 47.47/47.55 ** KEPT (pick-wt=13): 376 [] c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(B,A,tc_fun(C,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=22): 377 [] c_Com_Ocom_Ocom__rec(A,B,C,D,E,F,G,H,c_Com_Ocom_OCall(I,J,K),L)=hAPP(hAPP(hAPP(H,I),J),K). % 47.47/47.55 ** KEPT (pick-wt=17): 378 [] c_Set_Oinsert(A,B,C)=c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),B,tc_fun(C,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=18): 379 [] c_Lattices_Oupper__semilattice__class_Osup(A,c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)),tc_fun(C,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)). % 47.47/47.55 ---> New Demodulator: 380 [new_demod,379] c_Lattices_Oupper__semilattice__class_Osup(A,c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)),tc_fun(C,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=11): 382 [copy,381,flip.1] c_Hoare__Mirabelle_Otriple_Otriple(c_fe_qual(tc_Com_Ostate),A,c_Natural_Oevalc(A),tc_Com_Ostate)=hAPP(c_Hoare__Mirabelle_OMGT,A). % 47.47/47.55 ---> New Demodulator: 383 [new_demod,382] c_Hoare__Mirabelle_Otriple_Otriple(c_fe_qual(tc_Com_Ostate),A,c_Natural_Oevalc(A),tc_Com_Ostate)=hAPP(c_Hoare__Mirabelle_OMGT,A). % 47.47/47.55 ** KEPT (pick-wt=19): 384 [] c_Com_Ocom_Ocom__rec(A,B,C,D,E,F,G,H,c_Com_Ocom_OAss(I,J),K)=hAPP(hAPP(B,I),J). % 47.47/47.55 ** KEPT (pick-wt=31): 386 [copy,385,flip.1] hAPP(hAPP(hAPP(A,B),C),c_Com_Ocom_Ocom__rec(D,E,F,G,H,A,I,J,C,K))=c_Com_Ocom_Ocom__rec(D,E,F,G,H,A,I,J,c_Com_Ocom_OWhile(B,C),K). % 47.47/47.55 ---> New Demodulator: 387 [new_demod,386] hAPP(hAPP(hAPP(A,B),C),c_Com_Ocom_Ocom__rec(D,E,F,G,H,A,I,J,C,K))=c_Com_Ocom_Ocom__rec(D,E,F,G,H,A,I,J,c_Com_Ocom_OWhile(B,C),K). % 47.47/47.55 ** KEPT (pick-wt=6): 388 [] hAPP(c_Fun_Oid(A),B)=B. % 47.47/47.55 ---> New Demodulator: 389 [new_demod,388] hAPP(c_Fun_Oid(A),B)=B. % 47.47/47.55 ** KEPT (pick-wt=46): 391 [copy,390,flip.1] hAPP(hAPP(hAPP(hAPP(hAPP(A,B),C),D),c_Com_Ocom_Ocom__rec(E,F,G,H,A,I,J,K,C,L)),c_Com_Ocom_Ocom__rec(E,F,G,H,A,I,J,K,D,L))=c_Com_Ocom_Ocom__rec(E,F,G,H,A,I,J,K,c_Com_Ocom_OCond(B,C,D),L). % 47.47/47.55 ---> New Demodulator: 392 [new_demod,391] hAPP(hAPP(hAPP(hAPP(hAPP(A,B),C),D),c_Com_Ocom_Ocom__rec(E,F,G,H,A,I,J,K,C,L)),c_Com_Ocom_Ocom__rec(E,F,G,H,A,I,J,K,D,L))=c_Com_Ocom_Ocom__rec(E,F,G,H,A,I,J,K,c_Com_Ocom_OCond(B,C,D),L). % 47.47/47.55 ** KEPT (pick-wt=7): 393 [] hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),A),A)). % 47.47/47.55 Following clause subsumed by 326 during input processing: 0 [] c_lesse_quals(c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),tc_fun(A,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=22): 394 [] c_Com_Ocom_Ocom__case(A,B,C,D,E,F,G,H,c_Com_Ocom_OLocal(I,J,K),L)=hAPP(hAPP(hAPP(C,I),J),K). % 47.47/47.55 ** KEPT (pick-wt=19): 395 [] c_Com_Ocom_Ocom__case(A,B,C,D,E,F,G,H,c_Com_Ocom_OWhile(I,J),K)=hAPP(hAPP(F,I),J). % 47.47/47.55 ** KEPT (pick-wt=9): 396 [] c_lesse_quals(A,c_Orderings_Otop__class_Otop(tc_fun(B,tc_bool)),tc_fun(B,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=23): 398 [copy,397,flip.1] c_Fun_Ocomp(c_Fun_Ocomp(A,B,C,D,E),F,E,D,G)=c_Fun_Ocomp(A,c_Fun_Ocomp(B,F,E,C,G),C,D,G). % 47.47/47.55 ---> New Demodulator: 399 [new_demod,398] c_Fun_Ocomp(c_Fun_Ocomp(A,B,C,D,E),F,E,D,G)=c_Fun_Ocomp(A,c_Fun_Ocomp(B,F,E,C,G),C,D,G). % 47.47/47.55 ** KEPT (pick-wt=16): 400 [] c_Hoare__Mirabelle_Ohoare__derivs(A,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(B,c_Com_Ocom_OSKIP,B,C),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(C),tc_bool)),tc_Hoare__Mirabelle_Otriple(C)),C). % 47.47/47.55 ** KEPT (pick-wt=7): 401 [] hBOOL(hAPP(c_Set_Oinsert(A,B,C),A)). % 47.47/47.55 ** KEPT (pick-wt=6): 402 [] c_lesse_quals(A,A,tc_fun(B,tc_bool)). % 47.47/47.55 Following clause subsumed by 402 during input processing: 0 [] c_lesse_quals(A,A,tc_fun(B,tc_bool)). % 47.47/47.55 Following clause subsumed by 360 during input processing: 0 [] c_in(A,c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B),B). % 47.47/47.55 ** KEPT (pick-wt=22): 403 [] c_Com_Ocom_Ocom__case(A,B,C,D,E,F,G,H,c_Com_Ocom_OCond(I,J,K),L)=hAPP(hAPP(hAPP(E,I),J),K). % 47.47/47.55 Following clause subsumed by 291 during input processing: 0 [demod,359] c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=7): 404 [] c_Option_Othe(c_Option_Ooption_OSome(A,B),B)=A. % 47.47/47.55 ---> New Demodulator: 405 [new_demod,404] c_Option_Othe(c_Option_Ooption_OSome(A,B),B)=A. % 47.47/47.55 ** KEPT (pick-wt=25): 406 [] c_Set_Oimage(A,c_Lattices_Oupper__semilattice__class_Osup(B,C,tc_fun(D,tc_bool)),D,E)=c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(A,B,D,E),c_Set_Oimage(A,C,D,E),tc_fun(E,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=12): 407 [] hBOOL(hAPP(c_Com_OWT,hAPP(c_Com_Ocom_OBODY,A)))|hAPP(c_Com_Obody,A)=c_Option_Ooption_ONone(tc_Com_Ocom). % 47.47/47.55 ** KEPT (pick-wt=17): 408 [] c_Com_Ocom_Ocom__rec(A,B,C,D,E,F,G,H,hAPP(c_Com_Ocom_OBODY,I),J)=hAPP(G,I). % 47.47/47.55 ** KEPT (pick-wt=20): 409 [] c_Set_Oimage(c_Fun_Ocomp(A,B,C,D,E),F,E,D)=c_Set_Oimage(A,c_Set_Oimage(B,F,E,C),C,D). % 47.47/47.55 ---> New Demodulator: 410 [new_demod,409] c_Set_Oimage(c_Fun_Ocomp(A,B,C,D,E),F,E,D)=c_Set_Oimage(A,c_Set_Oimage(B,F,E,C),C,D). % 47.47/47.55 ** KEPT (pick-wt=20): 412 [copy,411,flip.1] c_Set_Oimage(c_COMBB(A,B,C,D,E),F,E,D)=c_Set_Oimage(A,c_Set_Oimage(B,F,E,C),C,D). % 47.47/47.55 ---> New Demodulator: 413 [new_demod,412] c_Set_Oimage(c_COMBB(A,B,C,D,E),F,E,D)=c_Set_Oimage(A,c_Set_Oimage(B,F,E,C),C,D). % 47.47/47.55 ** KEPT (pick-wt=19): 415 [copy,414,flip.1] c_Set_Oinsert(hAPP(A,B),c_Set_Oimage(A,C,D,E),E)=c_Set_Oimage(A,c_Set_Oinsert(B,C,D),D,E). % 47.47/47.55 ---> New Demodulator: 416 [new_demod,415] c_Set_Oinsert(hAPP(A,B),c_Set_Oimage(A,C,D,E),E)=c_Set_Oimage(A,c_Set_Oinsert(B,C,D),D,E). % 47.47/47.55 Following clause subsumed by 291 during input processing: 0 [demod,413] c_Set_Oimage(A,c_Set_Oimage(B,c_Orderings_Otop__class_Otop(tc_fun(E,tc_bool)),E,C),C,D)=c_Set_Oimage(A,c_Set_Oimage(B,c_Orderings_Otop__class_Otop(tc_fun(E,tc_bool)),E,C),C,D). % 47.47/47.55 ** KEPT (pick-wt=4): 417 [] c_Hoare__Mirabelle_Ostate__not__singleton|A=B. % 47.47/47.55 ** KEPT (pick-wt=8): 418 [] c_Set_Oimage(c_COMBI(A),B,A,A)=B. % 47.47/47.55 ---> New Demodulator: 419 [new_demod,418] c_Set_Oimage(c_COMBI(A),B,A,A)=B. % 47.47/47.55 ** KEPT (pick-wt=14): 420 [] hAPP(c_COMBB(A,B,C,D,E),F)=hAPP(A,hAPP(B,F)). % 47.47/47.55 ---> New Demodulator: 421 [new_demod,420] hAPP(c_COMBB(A,B,C,D,E),F)=hAPP(A,hAPP(B,F)). % 47.47/47.55 ** KEPT (pick-wt=4): 422 [] hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OSKIP)). % 47.47/47.55 ** KEPT (pick-wt=13): 423 [] c_Set_Oimage(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B,C)=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=6): 424 [] hBOOL(hAPP(c_Com_OWT,c_Com_Ocom_OAss(A,B))). % 47.47/47.55 Following clause subsumed by 291 during input processing: 0 [demod,383] hAPP(c_Hoare__Mirabelle_OMGT,v_c)=hAPP(c_Hoare__Mirabelle_OMGT,v_c). % 47.47/47.55 ** KEPT (pick-wt=6): 425 [] c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname). % 47.47/47.55 ** KEPT (pick-wt=8): 426 [] c_Set_Oimage(c_Fun_Oid(A),B,A,A)=B. % 47.47/47.55 ---> New Demodulator: 427 [new_demod,426] c_Set_Oimage(c_Fun_Oid(A),B,A,A)=B. % 47.47/47.55 ** KEPT (pick-wt=13): 428 [] c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))=c_Set_Oimage(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C,A). % 47.47/47.55 ** KEPT (pick-wt=17): 429 [] c_Com_Ocom_Ocom__case(A,B,C,D,E,F,G,H,hAPP(c_Com_Ocom_OBODY,I),J)=hAPP(G,I). % 47.47/47.55 ** KEPT (pick-wt=1): 430 [] c_Hoare__Mirabelle_Ostate__not__singleton. % 47.47/47.55 ** KEPT (pick-wt=1): 431 [] c_Com_OWT__bodies. % 47.47/47.55 ** KEPT (pick-wt=4): 432 [] hBOOL(hAPP(c_Com_OWT,v_c)). % 47.47/47.55 ** KEPT (pick-wt=2): 433 [] class_Lattices_Oupper__semilattice(tc_nat). % 47.47/47.55 ** KEPT (pick-wt=2): 434 [] class_Orderings_Opreorder(tc_nat). % 47.47/47.55 ** KEPT (pick-wt=2): 435 [] class_Orderings_Olinorder(tc_nat). % 47.47/47.55 ** KEPT (pick-wt=2): 436 [] class_Lattices_Olattice(tc_nat). % 47.47/47.55 ** KEPT (pick-wt=2): 437 [] class_Orderings_Oorder(tc_nat). % 47.47/47.55 ** KEPT (pick-wt=2): 438 [] class_Orderings_Obot(tc_nat). % 47.47/47.55 ** KEPT (pick-wt=2): 439 [] class_HOL_Oord(tc_nat). % 47.47/47.55 ** KEPT (pick-wt=2): 440 [] class_Lattices_Oupper__semilattice(tc_bool). % 47.47/47.55 ** KEPT (pick-wt=2): 441 [] class_Lattices_Obounded__lattice(tc_bool). % 47.47/47.55 ** KEPT (pick-wt=2): 442 [] class_Finite__Set_Ofinite_Ofinite(tc_bool). % 47.47/47.55 ** KEPT (pick-wt=2): 443 [] class_Orderings_Opreorder(tc_bool). % 47.47/47.55 ** KEPT (pick-wt=2): 444 [] class_Lattices_Olattice(tc_bool). % 47.47/47.55 ** KEPT (pick-wt=2): 445 [] class_Orderings_Oorder(tc_bool). % 47.47/47.55 ** KEPT (pick-wt=2): 446 [] class_Orderings_Otop(tc_bool). % 47.47/47.55 ** KEPT (pick-wt=2): 447 [] class_Orderings_Obot(tc_bool). % 47.47/47.55 ** KEPT (pick-wt=2): 448 [] class_HOL_Oord(tc_bool). % 47.47/47.55 ** KEPT (pick-wt=13): 449 [] c_COMBC(A,B,C,D,E,F)=hAPP(hAPP(A,C),B). % 47.47/47.55 Following clause subsumed by 291 during input processing: 0 [demod,421] hAPP(A,hAPP(B,F))=hAPP(A,hAPP(B,F)). % 47.47/47.55 ** KEPT (pick-wt=7): 450 [] hBOOL(hAPP(hAPP(c_fe_qual(A),B),B)). % 47.47/47.55 Following clause subsumed by 291 during input processing: 0 [copy,291,flip.1] A=A. % 47.47/47.55 291 back subsumes 277. % 47.47/47.55 291 back subsumes 276. % 47.47/47.55 291 back subsumes 275. % 47.47/47.55 291 back subsumes 274. % 47.47/47.55 >>>> Starting back demodulation with 294. % 47.47/47.55 ** KEPT (pick-wt=27): 451 [copy,295,flip.1] c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),tc_fun(C,tc_bool)),D,tc_fun(C,tc_bool))=c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,D,C),tc_fun(C,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=27): 452 [copy,296,flip.1] c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),c_Set_Oinsert(D,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),tc_fun(C,tc_bool))=c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(D,B,C),tc_fun(C,tc_bool)). % 47.47/47.55 >>>> Starting back demodulation with 298. % 47.47/47.55 >> back demodulating 20 with 298. % 47.47/47.55 >>>> Starting back demodulation with 302. % 47.47/47.55 ** KEPT (pick-wt=11): 453 [copy,303,flip.1] c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))=c_HOL_Ominus__class_Ominus(B,B,tc_fun(A,tc_bool)). % 47.47/47.55 >>>> Starting back demodulation with 305. % 47.47/47.55 >>>> Starting back demodulation with 307. % 47.47/47.55 >>>> Starting back demodulation with 310. % 47.47/47.55 >>>> Starting back demodulation with 312. % 47.47/47.55 >> back demodulating 1 with 312. % 47.47/47.55 >>>> Starting back demodulation with 315. % 47.47/47.55 >>>> Starting back demodulation with 319. % 47.47/47.55 >>>> Starting back demodulation with 323. % 47.47/47.55 ** KEPT (pick-wt=19): 454 [copy,325,flip.1] c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(A,B,C),D,tc_fun(C,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(B,c_Set_Oinsert(A,D,C),tc_fun(C,tc_bool)). % 47.47/47.55 >>>> Starting back demodulation with 328. % 47.47/47.55 >>>> Starting back demodulation with 330. % 47.47/47.55 >>>> Starting back demodulation with 332. % 47.47/47.55 >> back demodulating 285 with 332. % 47.47/47.55 >> back demodulating 281 with 332. % 47.47/47.55 >> back demodulating 280 with 332. % 47.47/47.55 >> back demodulating 279 with 332. % 47.47/47.55 >> back demodulating 278 with 332. % 47.47/47.55 >>>> Starting back demodulation with 337. % 47.47/47.55 >> back demodulating 198 with 337. % 47.47/47.55 >>>> Starting back demodulation with 339. % 47.47/47.55 >>>> Starting back demodulation with 342. % 47.47/47.55 >>>> Starting back demodulation with 344. % 47.47/47.55 >>>> Starting back demodulation with 351. % 47.47/47.55 >>>> Starting back demodulation with 353. % 47.47/47.55 >>>> Starting back demodulation with 355. % 47.47/47.55 >>>> Starting back demodulation with 357. % 47.47/47.55 >> back demodulating 122 with 357. % 47.47/47.55 >>>> Starting back demodulation with 359. % 47.47/47.55 >> back demodulating 284 with 359. % 47.47/47.55 >> back demodulating 272 with 359. % 47.47/47.55 >> back demodulating 268 with 359. % 47.47/47.55 >> back demodulating 267 with 359. % 47.47/47.55 >> back demodulating 266 with 359. % 47.47/47.55 ** KEPT (pick-wt=22): 460 [copy,361,flip.1] hAPP(hAPP(hAPP(A,B),C),D)=c_Com_Ocom_Ocom__case(E,F,G,H,I,J,K,A,c_Com_Ocom_OCall(B,C,D),L). % 47.47/47.55 Following clause subsumed by 362 during input processing: 0 [copy,362,flip.1] c_Set_Oinsert(A,c_Set_Oinsert(B,C,D),D)=c_Set_Oinsert(B,c_Set_Oinsert(A,C,D),D). % 47.47/47.55 >>>> Starting back demodulation with 364. % 47.47/47.55 >>>> Starting back demodulation with 366. % 47.47/47.55 ** KEPT (pick-wt=19): 461 [copy,367,flip.1] hAPP(hAPP(A,B),C)=c_Com_Ocom_Ocom__case(D,A,E,F,G,H,I,J,c_Com_Ocom_OAss(B,C),K). % 47.47/47.55 Following clause subsumed by 369 during input processing: 0 [copy,369,flip.1] c_Lattices_Oupper__semilattice__class_Osup(A,c_Lattices_Oupper__semilattice__class_Osup(B,C,tc_fun(D,tc_bool)),tc_fun(D,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(B,c_Lattices_Oupper__semilattice__class_Osup(A,C,tc_fun(D,tc_bool)),tc_fun(D,tc_bool)). % 47.47/47.55 >>>> Starting back demodulation with 371. % 47.47/47.55 Following clause subsumed by 428 during input processing: 0 [copy,374,flip.1] c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))=c_Set_Oimage(c_COMBK(B,A,C),c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C,A). % 47.47/47.55 ** KEPT (pick-wt=19): 462 [copy,375,flip.1] hAPP(hAPP(A,B),C)=c_Com_Ocom_Ocom__case(D,E,F,A,G,H,I,J,c_Com_Ocom_OSemi(B,C),K). % 47.47/47.55 Following clause subsumed by 376 during input processing: 0 [copy,376,flip.1] c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(B,A,tc_fun(C,tc_bool)). % 47.47/47.55 ** KEPT (pick-wt=22): 463 [copy,377,flip.1] hAPP(hAPP(hAPP(A,B),C),D)=c_Com_Ocom_Ocom__rec(E,F,G,H,I,J,K,A,c_Com_Ocom_OCall(B,C,D),L). % 47.47/47.55 ** KEPT (pick-wt=17): 464 [copy,378,flip.1] c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B),C,tc_fun(B,tc_bool))=c_Set_Oinsert(A,C,B). % 47.47/47.55 >>>> Starting back demodulation with 380. % 47.47/47.55 >>>> Starting back demodulation with 383. % 47.47/47.55 ** KEPT (pick-wt=19): 465 [copy,384,flip.1] hAPP(hAPP(A,B),C)=c_Com_Ocom_Ocom__rec(D,A,E,F,G,H,I,J,c_Com_Ocom_OAss(B,C),K). % 47.47/47.55 >>>> Starting back demodulation with 387. % 47.47/47.55 >>>> Starting back demodulation with 389. % 47.47/47.55 >>>> Starting back demodulation with 392. % 47.47/47.55 ** KEPT (pick-wt=22): 466 [copy,394,flip.1] hAPP(hAPP(hAPP(A,B),C),D)=c_Com_Ocom_Ocom__case(E,F,A,G,H,I,J,K,c_Com_Ocom_OLocal(B,C,D),L). % 47.47/47.55 ** KEPT (pick-wt=19): 467 [copy,395,flip.1] hAPP(hAPP(A,B),C)=c_Com_Ocom_Ocom__case(D,E,F,G,H,A,I,J,c_Com_Ocom_OWhile(B,C),K). % 47.47/47.55 >>>> Starting back demodulation with 399. % 47.47/47.55 ** KEPT (pick-wt=22): 468 [copy,403,flip.1] hAPP(hAPP(hAPP(A,B),C),D)=c_Com_Ocom_Ocom__case(E,F,G,H,A,I,J,K,c_Com_Ocom_OCond(B,C,D),L). % 47.47/47.55 >>>> Starting back demodulation with 405. % 47.47/47.55 ** KEPT (pick-wt=25): 469 [copy,406,flip.1] c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(A,B,C,D),c_Set_Oimage(A,E,C,D),tc_fun(D,tc_bool))=c_Set_Oimage(A,c_Lattices_Oupper__semilattice__class_Osup(B,E,tc_fun(C,tc_bool)),C,D). % 47.47/47.55 ** KEPT (pick-wt=17): 470 [copy,408,flip.1] hAPP(A,B)=c_Com_Ocom_Ocom__rec(C,D,E,F,G,H,A,I,hAPP(c_Com_Ocom_OBODY,B),J). % 47.47/47.55 >>>> Starting back demodulation with 410. % 47.47/47.55 >>>> Starting back demodulation with 413. % 47.47/47.55 >> back demodulating 252 with 413. % 47.47/47.55 >> back demodulating 237 with 413. % 47.47/47.55 >>>> Starting back demodulation with 416. % 47.47/47.55 >> back demodulating 115 with 416. % 47.47/47.55 >>>> Starting back demodulation with 419. % 47.47/47.55 >>>> Starting back demodulation with 421. % 47.47/47.55 Following clause subsumed by 428 during input processing: 0 [copy,423,flip.1] c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))=c_Set_Oimage(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C,A). % 47.84/47.95 423 back subsumes 374. % 47.84/47.95 >>>> Starting back demodulation with 427. % 47.84/47.95 Following clause subsumed by 423 during input processing: 0 [copy,428,flip.1] c_Set_Oimage(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B,C)=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)). % 47.84/47.95 ** KEPT (pick-wt=17): 473 [copy,429,flip.1] hAPP(A,B)=c_Com_Ocom_Ocom__case(C,D,E,F,G,H,A,I,hAPP(c_Com_Ocom_OBODY,B),J). % 47.84/47.95 430 back subsumes 417. % 47.84/47.95 431 back subsumes 234. % 47.84/47.95 431 back subsumes 221. % 47.84/47.95 ** KEPT (pick-wt=13): 474 [copy,449,flip.1] hAPP(hAPP(A,B),C)=c_COMBC(A,C,B,D,E,F). % 47.84/47.95 Following clause subsumed by 295 during input processing: 0 [copy,451,flip.1] c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))=c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)),C,tc_fun(D,tc_bool)). % 47.84/47.95 Following clause subsumed by 296 during input processing: 0 [copy,452,flip.1] c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))=c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,C,tc_fun(D,tc_bool)),c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)). % 47.84/47.95 Following clause subsumed by 303 during input processing: 0 [copy,453,flip.1] c_HOL_Ominus__class_Ominus(A,A,tc_fun(B,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)). % 47.84/47.95 Following clause subsumed by 325 during input processing: 0 [copy,454,flip.1] c_Lattices_Oupper__semilattice__class_Osup(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))=c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(B,A,D),C,tc_fun(D,tc_bool)). % 47.84/47.95 Following clause subsumed by 361 during input processing: 0 [copy,460,flip.1] c_Com_Ocom_Ocom__case(A,B,C,D,E,F,G,H,c_Com_Ocom_OCall(I,J,K),L)=hAPP(hAPP(hAPP(H,I),J),K). % 47.84/47.95 Following clause subsumed by 367 during input processing: 0 [copy,461,flip.1] c_Com_Ocom_Ocom__case(A,B,C,D,E,F,G,H,c_Com_Ocom_OAss(I,J),K)=hAPP(hAPP(B,I),J). % 47.84/47.95 Following clause subsumed by 375 during input processing: 0 [copy,462,flip.1] c_Com_Ocom_Ocom__case(A,B,C,D,E,F,G,H,c_Com_Ocom_OSemi(I,J),K)=hAPP(hAPP(D,I),J). % 47.84/47.95 Following clause subsumed by 377 during input processing: 0 [copy,463,flip.1] c_Com_Ocom_Ocom__rec(A,B,C,D,E,F,G,H,c_Com_Ocom_OCall(I,J,K),L)=hAPP(hAPP(hAPP(H,I),J),K). % 47.84/47.95 Following clause subsumed by 378 during input processing: 0 [copy,464,flip.1] c_Set_Oinsert(A,B,C)=c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),B,tc_fun(C,tc_bool)). % 47.84/47.95 Following clause subsumed by 384 during input processing: 0 [copy,465,flip.1] c_Com_Ocom_Ocom__rec(A,B,C,D,E,F,G,H,c_Com_Ocom_OAss(I,J),K)=hAPP(hAPP(B,I),J). % 47.84/47.95 Following clause subsumed by 394 during input processing: 0 [copy,466,flip.1] c_Com_Ocom_Ocom__case(A,B,C,D,E,F,G,H,c_Com_Ocom_OLocal(I,J,K),L)=hAPP(hAPP(hAPP(C,I),J),K). % 47.84/47.95 Following clause subsumed by 395 during input processing: 0 [copy,467,flip.1] c_Com_Ocom_Ocom__case(A,B,C,D,E,F,G,H,c_Com_Ocom_OWhile(I,J),K)=hAPP(hAPP(F,I),J). % 47.84/47.95 Following clause subsumed by 403 during input processing: 0 [copy,468,flip.1] c_Com_Ocom_Ocom__case(A,B,C,D,E,F,G,H,c_Com_Ocom_OCond(I,J,K),L)=hAPP(hAPP(hAPP(E,I),J),K). % 47.84/47.95 Following clause subsumed by 406 during input processing: 0 [copy,469,flip.1] c_Set_Oimage(A,c_Lattices_Oupper__semilattice__class_Osup(B,C,tc_fun(D,tc_bool)),D,E)=c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(A,B,D,E),c_Set_Oimage(A,C,D,E),tc_fun(E,tc_bool)). % 47.84/47.95 Following clause subsumed by 408 during input processing: 0 [copy,470,flip.1] c_Com_Ocom_Ocom__rec(A,B,C,D,E,F,G,H,hAPP(c_Com_Ocom_OBODY,I),J)=hAPP(G,I). % 47.84/47.95 Following clause subsumed by 429 during input processing: 0 [copy,473,flip.1] c_Com_Ocom_Ocom__case(A,B,C,D,E,F,G,H,hAPP(c_Com_Ocom_OBODY,I),J)=hAPP(G,I). % 47.84/47.95 Following clause subsumed by 449 during input processing: 0 [copy,474,flip.1] c_COMBC(A,B,C,D,E,F)=hAPP(hAPP(A,C),B). % 47.84/47.95 % 47.84/47.95 ======= end of input processing ======= % 47.84/47.95 % 47.84/47.95 =========== start of search =========== % 47.84/47.95 % 47.84/47.95 % 47.84/47.95 Resetting weight limit to 2. % 47.84/47.95 % 47.84/47.95 % 47.84/47.95 Resetting weight limit to 2. % 47.84/47.95 % 47.84/47.95 sos_size=131 % 47.84/47.95 % 47.84/47.95 Search stopped because sos empty. % 47.84/47.95 % 47.84/47.95 % 47.84/47.95 Search stopped because sos empty. % 47.84/47.95 % 47.84/47.95 ============ end of search ============ % 47.84/47.95 % 47.84/47.95 -------------- statistics ------------- % 47.84/47.95 clauses given 132 % 47.84/47.95 clauses generated 36255 % 47.84/47.95 clauses kept 418 % 47.84/47.95 clauses forward subsumed 123 % 47.84/47.95 clauses back subsumed 11 % 47.84/47.95 Kbytes malloced 8789 % 47.84/47.95 % 47.84/47.95 ----------- times (seconds) ----------- % 47.84/47.95 user CPU time 0.44 (0 hr, 0 min, 0 sec) % 47.84/47.95 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 47.84/47.95 wall-clock time 47 (0 hr, 0 min, 47 sec) % 47.84/47.95 % 47.84/47.95 Process 25012 finished Wed Jul 27 05:39:38 2022 % 47.84/47.95 Otter interrupted % 47.84/47.95 PROOF NOT FOUND %------------------------------------------------------------------------------