%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEV059^5 : TPTP v6.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n106.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32286.75MB % OS : Linux 2.6.32-431.20.3.el6.x86_64 % CPULimit : 300s % DateTime : Thu Jul 17 13:33:40 EDT 2014 % Result : Theorem 12.86s % Output : Proof 12.86s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEV059^5 : TPTP v6.1.0. Released v4.0.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n106.star.cs.uiowa.edu % % Model : x86_64 x86_64 % % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % % Memory : 32286.75MB % % OS : Linux 2.6.32-431.20.3.el6.x86_64 % % CPULimit : 300 % % DateTime : Thu Jul 17 07:49:46 CDT 2014 % % CPUTime : 12.86 % Python 2.7.5 % Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % FOF formula (<kernel.Constant object at 0x8028c0>, <kernel.Type object at 0x8026c8>) of role type named b_type % Using role type % Declaring b:Type % FOF formula (<kernel.Constant object at 0xbda440>, <kernel.Type object at 0x802998>) of role type named a_type % Using role type % Declaring a:Type % FOF formula (<kernel.Constant object at 0x802fc8>, <kernel.DependentProduct object at 0x802518>) of role type named cG % Using role type % Declaring cG:(b->b) % FOF formula (<kernel.Constant object at 0x8026c8>, <kernel.DependentProduct object at 0x802560>) of role type named cA % Using role type % Declaring cA:(b->a) % FOF formula (<kernel.Constant object at 0x8028c0>, <kernel.DependentProduct object at 0x8029e0>) of role type named c_less_ % Using role type % Declaring c_less_:(a->(a->Prop)) % FOF formula (<kernel.Constant object at 0x802518>, <kernel.DependentProduct object at 0x802488>) of role type named cF % Using role type % Declaring cF:(b->b) % FOF formula (((and ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))->(forall (Y:b), ((c_less_ (cA Y)) (cA (cG Y))))) of role conjecture named cTHM89A_pme % Conjecture to prove = (((and ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))->(forall (Y:b), ((c_less_ (cA Y)) (cA (cG Y))))):Prop % Parameter b_DUMMY:b. % Parameter a_DUMMY:a. % We need to prove ['(((and ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))->(forall (Y:b), ((c_less_ (cA Y)) (cA (cG Y)))))'] % Parameter b:Type. % Parameter a:Type. % Parameter cG:(b->b). % Parameter cA:(b->a). % Parameter c_less_:(a->(a->Prop)). % Parameter cF:(b->b). % Trying to prove (((and ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))->(forall (Y:b), ((c_less_ (cA Y)) (cA (cG Y))))) % Found x30:=(x3 Y):((c_less_ (cA Y)) (cA (cF Y))) % Found (x3 Y) as proof of ((c_less_ (cA Y)) Xy) % Found (x3 Y) as proof of ((c_less_ (cA Y)) Xy) % Found (x3 Y) as proof of ((c_less_ (cA Y)) Xy) % Found eq_ref00:=(eq_ref0 (cA (cG Y))):(((eq a) (cA (cG Y))) (cA (cG Y))) % Found (eq_ref0 (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found ((eq_ref a) (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found ((eq_ref a) (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found ((eq_ref a) (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found eq_ref00:=(eq_ref0 (cA (cG Y))):(((eq a) (cA (cG Y))) (cA (cG Y))) % Found (eq_ref0 (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found ((eq_ref a) (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found ((eq_ref a) (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found ((eq_ref a) (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found eq_ref00:=(eq_ref0 a0):(((eq b) a0) a0) % Found (eq_ref0 a0) as proof of (((eq b) a0) (cG Y)) % Found ((eq_ref b) a0) as proof of (((eq b) a0) (cG Y)) % Found ((eq_ref b) a0) as proof of (((eq b) a0) (cG Y)) % Found ((eq_ref b) a0) as proof of (((eq b) a0) (cG Y)) % Found x30:=(x3 Y):((c_less_ (cA Y)) (cA (cF Y))) % Found (x3 Y) as proof of (P b0) % Found (x3 Y) as proof of (P b0) % Found (fun (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of (P b0) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of ((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->(P b0)) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of ((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->(P b0))) % Found (and_rect10 (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P b0) % Found ((and_rect1 (P b0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P b0) % Found (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P b0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P b0) % Found (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P b0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P b0) % Found x30:=(x3 Y):((c_less_ (cA Y)) (cA (cF Y))) % Found (x3 Y) as proof of (P b0) % Found (x3 Y) as proof of (P b0) % Found (fun (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of (P b0) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of ((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->(P b0)) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of ((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->(P b0))) % Found (and_rect10 (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P b0) % Found ((and_rect1 (P b0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P b0) % Found (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P b0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P b0) % Found (fun (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P b0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)))) as proof of (P b0) % Found (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P b0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)))) as proof of ((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->(P b0)) % Found (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P b0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)))) as proof of (((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->(P b0))) % Found (and_rect00 (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P b0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))))) as proof of (P b0) % Found ((and_rect0 (P b0)) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P b0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))))) as proof of (P b0) % Found (((fun (P0:Type) (x0:(((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->P0)))=> (((((and_rect ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))) P0) x0) x)) (P b0)) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P b0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))))) as proof of (P b0) % Found (((fun (P0:Type) (x0:(((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->P0)))=> (((((and_rect ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))) P0) x0) x)) (P b0)) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P b0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))))) as proof of (P b0) % Found eq_ref00:=(eq_ref0 (cA (cG Y))):(((eq a) (cA (cG Y))) (cA (cG Y))) % Found (eq_ref0 (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found ((eq_ref a) (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found ((eq_ref a) (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found ((eq_ref a) (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found x30:=(x3 Y):((c_less_ (cA Y)) (cA (cF Y))) % Found (x3 Y) as proof of (P b0) % Found (x3 Y) as proof of (P b0) % Found (x3 Y) as proof of (P b0) % Found eq_ref00:=(eq_ref0 a0):(((eq b) a0) a0) % Found (eq_ref0 a0) as proof of (((eq b) a0) (cG Y)) % Found ((eq_ref b) a0) as proof of (((eq b) a0) (cG Y)) % Found ((eq_ref b) a0) as proof of (((eq b) a0) (cG Y)) % Found ((eq_ref b) a0) as proof of (((eq b) a0) (cG Y)) % Found eq_ref00:=(eq_ref0 a0):(((eq b) a0) a0) % Found (eq_ref0 a0) as proof of (((eq b) a0) (cG Y)) % Found ((eq_ref b) a0) as proof of (((eq b) a0) (cG Y)) % Found ((eq_ref b) a0) as proof of (((eq b) a0) (cG Y)) % Found ((eq_ref b) a0) as proof of (((eq b) a0) (cG Y)) % Found x30:=(x3 Y):((c_less_ (cA Y)) (cA (cF Y))) % Found (x3 Y) as proof of (P (cA a0)) % Found (x3 Y) as proof of (P (cA a0)) % Found (x3 Y) as proof of (P (cA a0)) % Found x30:=(x3 Y):((c_less_ (cA Y)) (cA (cF Y))) % Found (x3 Y) as proof of (P (cA a0)) % Found (x3 Y) as proof of (P (cA a0)) % Found (fun (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of (P (cA a0)) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of ((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->(P (cA a0))) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of ((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->(P (cA a0)))) % Found (and_rect10 (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P (cA a0)) % Found ((and_rect1 (P (cA a0))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P (cA a0)) % Found (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P (cA a0))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P (cA a0)) % Found (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P (cA a0))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P (cA a0)) % Found x30:=(x3 Y):((c_less_ (cA Y)) (cA (cF Y))) % Found (x3 Y) as proof of (P (cA a0)) % Found (x3 Y) as proof of (P (cA a0)) % Found (fun (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of (P (cA a0)) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of ((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->(P (cA a0))) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of ((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->(P (cA a0)))) % Found (and_rect10 (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P (cA a0)) % Found ((and_rect1 (P (cA a0))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P (cA a0)) % Found (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P (cA a0))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P (cA a0)) % Found (fun (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P (cA a0))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)))) as proof of (P (cA a0)) % Found (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P (cA a0))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)))) as proof of ((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->(P (cA a0))) % Found (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P (cA a0))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)))) as proof of (((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->(P (cA a0)))) % Found (and_rect00 (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P (cA a0))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))))) as proof of (P (cA a0)) % Found ((and_rect0 (P (cA a0))) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P (cA a0))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))))) as proof of (P (cA a0)) % Found (((fun (P0:Type) (x0:(((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->P0)))=> (((((and_rect ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))) P0) x0) x)) (P (cA a0))) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P (cA a0))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))))) as proof of (P (cA a0)) % Found (((fun (P0:Type) (x0:(((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->P0)))=> (((((and_rect ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))) P0) x0) x)) (P (cA a0))) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P (cA a0))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))))) as proof of (P (cA a0)) % Found x30:=(x3 Y):((c_less_ (cA Y)) (cA (cF Y))) % Found (x3 Y) as proof of ((c_less_ (cA Y)) Xy0) % Found (x3 Y) as proof of ((c_less_ (cA Y)) Xy0) % Found (x3 Y) as proof of ((c_less_ (cA Y)) Xy0) % Found eq_ref00:=(eq_ref0 b0):(((eq a) b0) b0) % Found (eq_ref0 b0) as proof of (((eq a) b0) (cA (cG Y))) % Found ((eq_ref a) b0) as proof of (((eq a) b0) (cA (cG Y))) % Found ((eq_ref a) b0) as proof of (((eq a) b0) (cA (cG Y))) % Found ((eq_ref a) b0) as proof of (((eq a) b0) (cA (cG Y))) % Found eq_ref00:=(eq_ref0 a0):(((eq a) a0) a0) % Found (eq_ref0 a0) as proof of (((eq a) a0) b0) % Found ((eq_ref a) a0) as proof of (((eq a) a0) b0) % Found ((eq_ref a) a0) as proof of (((eq a) a0) b0) % Found ((eq_ref a) a0) as proof of (((eq a) a0) b0) % Found eq_ref00:=(eq_ref0 b0):(((eq a) b0) b0) % Found (eq_ref0 b0) as proof of (((eq a) b0) (cA (cG Y))) % Found ((eq_ref a) b0) as proof of (((eq a) b0) (cA (cG Y))) % Found ((eq_ref a) b0) as proof of (((eq a) b0) (cA (cG Y))) % Found ((eq_ref a) b0) as proof of (((eq a) b0) (cA (cG Y))) % Found eq_ref00:=(eq_ref0 a0):(((eq a) a0) a0) % Found (eq_ref0 a0) as proof of (((eq a) a0) b0) % Found ((eq_ref a) a0) as proof of (((eq a) a0) b0) % Found ((eq_ref a) a0) as proof of (((eq a) a0) b0) % Found ((eq_ref a) a0) as proof of (((eq a) a0) b0) % Found x30:=(x3 Y):((c_less_ (cA Y)) (cA (cF Y))) % Found (x3 Y) as proof of (P a0) % Found (x3 Y) as proof of (P a0) % Found (fun (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of (P a0) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of ((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->(P a0)) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of ((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->(P a0))) % Found (and_rect10 (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P a0) % Found ((and_rect1 (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P a0) % Found (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P a0) % Found (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P a0) % Found x30:=(x3 Y):((c_less_ (cA Y)) (cA (cF Y))) % Found (x3 Y) as proof of (P a0) % Found (x3 Y) as proof of (P a0) % Found (fun (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of (P a0) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of ((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->(P a0)) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of ((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->(P a0))) % Found (and_rect10 (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P a0) % Found ((and_rect1 (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P a0) % Found (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P a0) % Found (fun (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)))) as proof of (P a0) % Found (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)))) as proof of ((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->(P a0)) % Found (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)))) as proof of (((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->(P a0))) % Found (and_rect00 (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))))) as proof of (P a0) % Found ((and_rect0 (P a0)) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))))) as proof of (P a0) % Found (((fun (P0:Type) (x0:(((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->P0)))=> (((((and_rect ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))) P0) x0) x)) (P a0)) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))))) as proof of (P a0) % Found (((fun (P0:Type) (x0:(((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->P0)))=> (((((and_rect ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))) P0) x0) x)) (P a0)) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))))) as proof of (P a0) % Found x30:=(x3 Y):((c_less_ (cA Y)) (cA (cF Y))) % Found (x3 Y) as proof of (P a0) % Found (x3 Y) as proof of (P a0) % Found (fun (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of (P a0) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of ((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->(P a0)) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of ((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->(P a0))) % Found (and_rect10 (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P a0) % Found ((and_rect1 (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P a0) % Found (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P a0) % Found (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P a0) % Found x30:=(x3 Y):((c_less_ (cA Y)) (cA (cF Y))) % Found (x3 Y) as proof of (P a0) % Found (x3 Y) as proof of (P a0) % Found (fun (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of (P a0) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of ((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->(P a0)) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)) as proof of ((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->(P a0))) % Found (and_rect10 (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P a0) % Found ((and_rect1 (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P a0) % Found (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))) as proof of (P a0) % Found (fun (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)))) as proof of (P a0) % Found (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)))) as proof of ((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->(P a0)) % Found (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y)))) as proof of (((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->(P a0))) % Found (and_rect00 (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))))) as proof of (P a0) % Found ((and_rect0 (P a0)) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))))) as proof of (P a0) % Found (((fun (P0:Type) (x0:(((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->P0)))=> (((((and_rect ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))) P0) x0) x)) (P a0)) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))))) as proof of (P a0) % Found (((fun (P0:Type) (x0:(((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->P0)))=> (((((and_rect ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))) P0) x0) x)) (P a0)) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P0:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P0)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P0) x2) x0)) (P a0)) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (x3 Y))))) as proof of (P a0) % Found eq_ref00:=(eq_ref0 b0):(((eq a) b0) b0) % Found (eq_ref0 b0) as proof of (((eq a) b0) (cA (cG Y))) % Found ((eq_ref a) b0) as proof of (((eq a) b0) (cA (cG Y))) % Found ((eq_ref a) b0) as proof of (((eq a) b0) (cA (cG Y))) % Found ((eq_ref a) b0) as proof of (((eq a) b0) (cA (cG Y))) % Found eq_ref00:=(eq_ref0 a0):(((eq a) a0) a0) % Found (eq_ref0 a0) as proof of (((eq a) a0) b0) % Found ((eq_ref a) a0) as proof of (((eq a) a0) b0) % Found ((eq_ref a) a0) as proof of (((eq a) a0) b0) % Found ((eq_ref a) a0) as proof of (((eq a) a0) b0) % Found x30:=(x3 Y):((c_less_ (cA Y)) (cA (cF Y))) % Found (x3 Y) as proof of (P a0) % Found (x3 Y) as proof of (P a0) % Found (x3 Y) as proof of (P a0) % Found x30:=(x3 Y):((c_less_ (cA Y)) (cA (cF Y))) % Found (x3 Y) as proof of (P a0) % Found (x3 Y) as proof of (P a0) % Found (x3 Y) as proof of (P a0) % Found eq_ref00:=(eq_ref0 ((c_less_ Xy) (cA (cG Y)))):(((eq Prop) ((c_less_ Xy) (cA (cG Y)))) ((c_less_ Xy) (cA (cG Y)))) % Found (eq_ref0 ((c_less_ Xy) (cA (cG Y)))) as proof of (((eq Prop) ((c_less_ Xy) (cA (cG Y)))) b0) % Found ((eq_ref Prop) ((c_less_ Xy) (cA (cG Y)))) as proof of (((eq Prop) ((c_less_ Xy) (cA (cG Y)))) b0) % Found ((eq_ref Prop) ((c_less_ Xy) (cA (cG Y)))) as proof of (((eq Prop) ((c_less_ Xy) (cA (cG Y)))) b0) % Found ((eq_ref Prop) ((c_less_ Xy) (cA (cG Y)))) as proof of (((eq Prop) ((c_less_ Xy) (cA (cG Y)))) b0) % Found iff_trans:=(fun (A:Prop) (B:Prop) (C:Prop) (AB:((iff A) B)) (BC:((iff B) C))=> ((((conj (A->C)) (C->A)) (fun (x:A)=> ((((proj1 (B->C)) (C->B)) BC) ((((proj1 (A->B)) (B->A)) AB) x)))) (fun (x:C)=> ((((proj2 (A->B)) (B->A)) AB) ((((proj2 (B->C)) (C->B)) BC) x))))):(forall (A:Prop) (B:Prop) (C:Prop), (((iff A) B)->(((iff B) C)->((iff A) C)))) % Instantiate: b0:=(forall (A:Prop) (B:Prop) (C:Prop), (((iff A) B)->(((iff B) C)->((iff A) C)))):Prop % Found iff_trans as proof of b0 % Found x30:=(x3 Y):((c_less_ (cA Y)) (cA (cF Y))) % Found (x3 Y) as proof of ((c_less_ (cA Y)) Xy) % Found (x3 Y) as proof of ((c_less_ (cA Y)) Xy) % Found (x3 Y) as proof of ((c_less_ (cA Y)) Xy) % Found ((conj00 (x3 Y)) iff_trans) as proof of (P b0) % Found (((conj0 b0) (x3 Y)) iff_trans) as proof of (P b0) % Found ((((conj ((c_less_ (cA Y)) Xy)) b0) (x3 Y)) iff_trans) as proof of (P b0) % Found ((((conj ((c_less_ (cA Y)) Xy)) b0) (x3 Y)) iff_trans) as proof of (P b0) % Found eq_ref00:=(eq_ref0 a0):(((eq a) a0) a0) % Found (eq_ref0 a0) as proof of (((eq a) a0) (cA (cG Y))) % Found ((eq_ref a) a0) as proof of (((eq a) a0) (cA (cG Y))) % Found ((eq_ref a) a0) as proof of (((eq a) a0) (cA (cG Y))) % Found ((eq_ref a) a0) as proof of (((eq a) a0) (cA (cG Y))) % Found eq_ref00:=(eq_ref0 a0):(((eq a) a0) a0) % Found (eq_ref0 a0) as proof of (((eq a) a0) (cA (cG Y))) % Found ((eq_ref a) a0) as proof of (((eq a) a0) (cA (cG Y))) % Found ((eq_ref a) a0) as proof of (((eq a) a0) (cA (cG Y))) % Found ((eq_ref a) a0) as proof of (((eq a) a0) (cA (cG Y))) % Found eq_ref00:=(eq_ref0 (cA (cG Y))):(((eq a) (cA (cG Y))) (cA (cG Y))) % Found (eq_ref0 (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found ((eq_ref a) (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found ((eq_ref a) (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found ((eq_ref a) (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found x30:=(x3 (cF Y)):((c_less_ (cA (cF Y))) (cA (cF (cF Y)))) % Found (x3 (cF Y)) as proof of (P b0) % Found (x3 (cF Y)) as proof of (P b0) % Found (x3 (cF Y)) as proof of (P b0) % Found eq_ref00:=(eq_ref0 (cA (cG Y))):(((eq a) (cA (cG Y))) (cA (cG Y))) % Found (eq_ref0 (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found ((eq_ref a) (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found ((eq_ref a) (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found ((eq_ref a) (cA (cG Y))) as proof of (((eq a) (cA (cG Y))) b0) % Found x10:=(x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))):((P0 (cA (cG Y)))->(P0 (cA (cF (cF Y))))) % Found (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))) as proof of ((P0 (cA (cG Y)))->(P0 b0)) % Found (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y)))))) as proof of ((P0 (cA (cG Y)))->(P0 b0)) % Found (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y)))))) as proof of (((eq a) (cA (cG Y))) b0) % Found ((eq_sym0000 (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y))) as proof of ((c_less_ Xy) (cA (cG Y))) % Found ((eq_sym0000 (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y))) as proof of ((c_less_ Xy) (cA (cG Y))) % Found (((fun (x4:(((eq a) (cA (cG Y))) b0))=> ((eq_sym000 x4) (c_less_ Xy))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y))) as proof of ((c_less_ Xy) (cA (cG Y))) % Found (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((eq_sym00 (cA (cF (cF Y)))) x4) (c_less_ Xy))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y))) as proof of ((c_less_ Xy) (cA (cG Y))) % Found (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> ((((eq_sym0 (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ Xy))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y))) as proof of ((c_less_ Xy) (cA (cG Y))) % Found (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ Xy))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y))) as proof of ((c_less_ Xy) (cA (cG Y))) % Found (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ Xy))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y))) as proof of ((c_less_ Xy) (cA (cG Y))) % Found ((conj00 (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ Xy))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y)))) as proof of ((and ((c_less_ (cA Y)) Xy)) ((c_less_ Xy) (cA (cG Y)))) % Found (((conj0 ((c_less_ Xy) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ Xy))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y)))) as proof of ((and ((c_less_ (cA Y)) Xy)) ((c_less_ Xy) (cA (cG Y)))) % Found ((((conj ((c_less_ (cA Y)) Xy)) ((c_less_ Xy) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ Xy))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y)))) as proof of ((and ((c_less_ (cA Y)) Xy)) ((c_less_ Xy) (cA (cG Y)))) % Found ((((conj ((c_less_ (cA Y)) Xy)) ((c_less_ Xy) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ Xy))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y)))) as proof of ((and ((c_less_ (cA Y)) Xy)) ((c_less_ Xy) (cA (cG Y)))) % Found (x2000 ((((conj ((c_less_ (cA Y)) Xy)) ((c_less_ Xy) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ Xy))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y))))) as proof of ((c_less_ (cA Y)) (cA (cG Y))) % Found ((x200 (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y))))) as proof of ((c_less_ (cA Y)) (cA (cG Y))) % Found (((fun (Xy:a)=> ((x20 Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y))))) as proof of ((c_less_ (cA Y)) (cA (cG Y))) % Found (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y))))) as proof of ((c_less_ (cA Y)) (cA (cG Y))) % Found (fun (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y)))))) as proof of ((c_less_ (cA Y)) (cA (cG Y))) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y)))))) as proof of ((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->((c_less_ (cA Y)) (cA (cG Y)))) % Found (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y)))))) as proof of ((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->((c_less_ (cA Y)) (cA (cG Y))))) % Found (and_rect10 (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y))))))) as proof of ((c_less_ (cA Y)) (cA (cG Y))) % Found ((and_rect1 ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y))))))) as proof of ((c_less_ (cA Y)) (cA (cG Y))) % Found (((fun (P:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P) x2) x0)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y))))))) as proof of ((c_less_ (cA Y)) (cA (cG Y))) % Found (fun (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P) x2) x0)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y)))))))) as proof of ((c_less_ (cA Y)) (cA (cG Y))) % Found (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P) x2) x0)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y)))))))) as proof of ((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->((c_less_ (cA Y)) (cA (cG Y)))) % Found (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P) x2) x0)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y)))))))) as proof of (((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->((c_less_ (cA Y)) (cA (cG Y))))) % Found (and_rect00 (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P) x2) x0)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y))))))))) as proof of ((c_less_ (cA Y)) (cA (cG Y))) % Found ((and_rect0 ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P) x2) x0)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y))))))))) as proof of ((c_less_ (cA Y)) (cA (cG Y))) % Found (((fun (P:Type) (x0:(((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->P)))=> (((((and_rect ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))) P) x0) x)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P) x2) x0)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y))))))))) as proof of ((c_less_ (cA Y)) (cA (cG Y))) % Found (fun (Y:b)=> (((fun (P:Type) (x0:(((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->P)))=> (((((and_rect ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))) P) x0) x)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P) x2) x0)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y)))))))))) as proof of ((c_less_ (cA Y)) (cA (cG Y))) % Found (fun (x:((and ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))) (Y:b)=> (((fun (P:Type) (x0:(((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->P)))=> (((((and_rect ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))) P) x0) x)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P) x2) x0)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y)))))))))) as proof of (forall (Y:b), ((c_less_ (cA Y)) (cA (cG Y)))) % Found (fun (x:((and ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))) (Y:b)=> (((fun (P:Type) (x0:(((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->P)))=> (((((and_rect ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))) P) x0) x)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P) x2) x0)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y)))))))))) as proof of (((and ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))->(forall (Y:b), ((c_less_ (cA Y)) (cA (cG Y))))) % Got proof (fun (x:((and ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))) (Y:b)=> (((fun (P:Type) (x0:(((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->P)))=> (((((and_rect ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))) P) x0) x)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P) x2) x0)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y)))))))))) % Time elapsed = 12.432371s % node=2225 cost=2671.000000 depth=32 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (x:((and ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))) (Y:b)=> (((fun (P:Type) (x0:(((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))->((((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))->P)))=> (((((and_rect ((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z))))) P) x0) x)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x0:((and (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))) (x1:(((eq (b->b)) cG) (fun (Z:b)=> (cF (cF Z)))))=> (((fun (P:Type) (x2:((forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))->((forall (X:b), ((c_less_ (cA X)) (cA (cF X))))->P)))=> (((((and_rect (forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (forall (X:b), ((c_less_ (cA X)) (cA (cF X))))) P) x2) x0)) ((c_less_ (cA Y)) (cA (cG Y)))) (fun (x2:(forall (Xx:a) (Xy:a) (Xz:a), (((and ((c_less_ Xx) Xy)) ((c_less_ Xy) Xz))->((c_less_ Xx) Xz)))) (x3:(forall (X:b), ((c_less_ (cA X)) (cA (cF X)))))=> (((fun (Xy:a)=> (((x2 (cA Y)) Xy) (cA (cG Y)))) (cA (cF Y))) ((((conj ((c_less_ (cA Y)) (cA (cF Y)))) ((c_less_ (cA (cF Y))) (cA (cG Y)))) (x3 Y)) (((fun (x4:(((eq a) (cA (cG Y))) (cA (cF (cF Y)))))=> (((((eq_sym a) (cA (cG Y))) (cA (cF (cF Y)))) x4) (c_less_ (cA (cF Y))))) (fun (P0:(a->Prop))=> (x1 (fun (x4:(b->b))=> (P0 (cA (x4 Y))))))) (x3 (cF Y)))))))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------