%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : CAT002-2 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n024.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 : 600s % DateTime : Fri Jul 15 00:04:31 EDT 2022 % Result : Satisfiable 3.22s 3.39s % Output : Saturation 3.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : CAT002-2 : TPTP v8.1.0. Released v1.0.0. % 0.07/0.13 % Command : metis --show proof --show saturation %s % 0.13/0.34 % Computer : n024.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 : 600 % 0.13/0.34 % DateTime : Sun May 29 18:43:21 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 3.22/3.39 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.22/3.39 % 3.22/3.39 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.22/3.39 |- codomain (domain $X) = domain $X % 3.22/3.39 |- domain (codomain $X) = codomain $X % 3.22/3.39 |- compose (domain $X) $X = $X % 3.22/3.39 |- compose $X (codomain $X) = $X % 3.22/3.39 |- ~(codomain $X = domain $Y) \/ domain (compose $X $Y) = domain $X % 3.22/3.39 |- ~(codomain $X = domain $Y) \/ codomain (compose $X $Y) = codomain $Y % 3.22/3.39 |- ~(codomain $X = domain $Y) \/ ~(codomain $Y = domain $Z) \/ % 3.22/3.39 compose $X (compose $Y $Z) = compose (compose $X $Y) $Z % 3.22/3.39 |- codomain a = domain b % 3.22/3.39 |- ~(codomain $X = codomain g) \/ ~(codomain $Z = codomain a) \/ % 3.22/3.39 ~(compose $Z a = compose $X a) \/ $X = $Z % 3.22/3.39 |- ~(codomain $X = codomain g) \/ ~(codomain $Z = codomain a) \/ % 3.22/3.39 ~(compose $Z b = compose $X b) \/ $X = $Z % 3.22/3.39 |- codomain g = domain (compose a b) % 3.22/3.39 |- codomain g = codomain h % 3.22/3.39 |- compose h (compose a b) = compose g (compose a b) % 3.22/3.39 |- ~(codomain $Z = domain $Z) \/ % 3.22/3.39 compose $Z (compose $Z $Z) = compose (compose $Z $Z) $Z % 3.22/3.39 |- ~(h = g) % 3.22/3.39 |- codomain (codomain $_1) = codomain $_1 % 3.22/3.39 |- domain (domain $X) = domain $X % 3.22/3.39 |- compose (codomain a) b = b % 3.22/3.39 |- compose (codomain $X) (codomain $X) = codomain $X % 3.22/3.39 |- compose (codomain g) (compose a b) = compose a b % 3.22/3.39 |- compose (domain $X) (domain $X) = domain $X % 3.22/3.39 |- compose h (codomain g) = h % 3.22/3.39 |- ~(codomain g = domain g) \/ % 3.22/3.39 compose h (compose h h) = compose (compose h h) h % 3.22/3.39 |- ~(codomain b = codomain a) \/ % 3.22/3.39 compose b (compose b b) = compose (compose b b) b % 3.22/3.39 |- ~(codomain b = codomain g) \/ % 3.22/3.39 compose (compose a b) (compose (compose a b) (compose a b)) = % 3.22/3.39 compose (compose (compose a b) (compose a b)) (compose a b) % 3.22/3.39 |- ~(codomain $_1 = domain $_10) \/ % 3.22/3.39 domain (compose (codomain $_1) $_10) = codomain $_1 % 3.22/3.39 |- ~(domain $X = domain $_10) \/ % 3.22/3.39 domain (compose (domain $X) $_10) = domain $X % 3.22/3.39 |- ~(codomain g = domain $_10) \/ domain (compose h $_10) = domain g % 3.22/3.39 |- ~(codomain $_9 = codomain a) \/ domain (compose $_9 b) = domain $_9 % 3.22/3.39 |- ~(codomain $_9 = codomain $X) \/ % 3.22/3.39 domain (compose $_9 (codomain $X)) = domain $_9 % 3.22/3.39 |- ~(codomain $_9 = codomain g) \/ % 3.22/3.39 domain (compose $_9 (compose a b)) = domain $_9 % 3.22/3.39 |- ~(codomain $_9 = domain $X) \/ % 3.22/3.39 domain (compose $_9 (domain $X)) = domain $_9 % 3.22/3.39 |- codomain g = domain a % 3.22/3.39 |- domain (compose g (compose a b)) = domain g % 3.22/3.39 |- ~(codomain $X = codomain g) \/ domain (compose $X a) = domain $X % 3.22/3.39 |- ~(codomain a = codomain g) \/ % 3.22/3.39 compose a (compose a a) = compose (compose a a) a % 3.22/3.39 |- compose (codomain g) a = a % 3.22/3.39 |- domain (compose g a) = domain g % 3.22/3.39 |- ~(codomain $X = domain g) \/ % 3.22/3.39 domain (compose $X (compose g a)) = domain $X % 3.22/3.39 |- compose (domain g) (compose g a) = compose g a % 3.22/3.39 |- ~(codomain $X = domain g) \/ % 3.22/3.39 domain (compose $X (compose g (compose a b))) = domain $X % 3.22/3.39 |- ~(codomain b = domain g) \/ % 3.22/3.39 compose (compose g (compose a b)) % 3.22/3.39 (compose (compose g (compose a b)) (compose g (compose a b))) = % 3.22/3.39 compose (compose (compose g (compose a b)) (compose g (compose a b))) % 3.22/3.39 (compose g (compose a b)) % 3.22/3.39 |- compose (domain g) (compose g (compose a b)) = compose g (compose a b) % 3.24/3.39 |- ~(codomain $_1 = domain $_12) \/ % 3.24/3.39 codomain (compose (codomain $_1) $_12) = codomain $_12 % 3.24/3.39 |- ~(domain $X = domain $_12) \/ % 3.24/3.39 codomain (compose (domain $X) $_12) = codomain $_12 % 3.24/3.39 |- ~(codomain g = domain $_12) \/ codomain (compose h $_12) = codomain $_12 % 3.24/3.39 |- ~(codomain $_11 = codomain g) \/ codomain (compose $_11 a) = codomain a % 3.24/3.39 |- ~(codomain $_11 = codomain a) \/ codomain (compose $_11 b) = codomain b % 3.24/3.39 |- ~(codomain $_11 = codomain $X) \/ % 3.24/3.39 codomain (compose $_11 (codomain $X)) = codomain $X % 3.24/3.39 |- ~(codomain $_11 = codomain g) \/ % 3.24/3.39 codomain (compose $_11 (compose a b)) = codomain b % 3.24/3.39 |- ~(codomain $_11 = domain g) \/ % 3.24/3.39 codomain (compose $_11 (compose g a)) = codomain a % 3.24/3.39 |- ~(codomain $_11 = domain g) \/ % 3.24/3.39 codomain (compose $_11 (compose g (compose a b))) = codomain b % 3.24/3.39 |- ~(codomain $_11 = domain $X) \/ % 3.24/3.39 codomain (compose $_11 (domain $X)) = domain $X % 3.24/3.39 |- codomain (compose g a) = codomain a % 3.24/3.39 |- codomain (compose a b) = codomain b % 3.24/3.40 |- codomain (compose g (compose a b)) = codomain b % 3.24/3.40 |- ~(codomain a = domain $Y) \/ % 3.24/3.40 codomain (compose (compose g a) $Y) = codomain $Y % 3.24/3.40 |- ~(codomain a = domain $Y) \/ % 3.24/3.40 domain (compose (compose g a) $Y) = domain g % 3.24/3.40 |- ~(codomain a = domain g) \/ % 3.24/3.40 compose (compose g a) (compose (compose g a) (compose g a)) = % 3.24/3.40 compose (compose (compose g a) (compose g a)) (compose g a) % 3.24/3.40 |- compose (compose g a) (codomain a) = compose g a % 3.24/3.40 |- ~(codomain b = domain $Y) \/ % 3.24/3.40 codomain (compose (compose a b) $Y) = codomain $Y % 3.24/3.40 |- ~(codomain b = domain $Y) \/ % 3.24/3.40 domain (compose (compose a b) $Y) = codomain g % 3.24/3.40 |- compose (compose a b) (codomain b) = compose a b % 3.24/3.40 |- ~(codomain b = domain $Y) \/ % 3.24/3.40 codomain (compose (compose g (compose a b)) $Y) = codomain $Y % 3.24/3.40 |- ~(codomain b = domain $Y) \/ % 3.24/3.40 domain (compose (compose g (compose a b)) $Y) = domain g % 3.24/3.40 |- compose (compose g (compose a b)) (codomain b) = compose g (compose a b) % 3.24/3.40 |- domain (compose h a) = domain g % 3.24/3.40 |- ~(codomain g = codomain a) \/ domain (compose h b) = domain g % 3.24/3.40 |- ~(codomain g = codomain $X) \/ % 3.24/3.40 domain (compose h (codomain $X)) = domain g % 3.24/3.40 |- domain g = domain h % 3.24/3.40 |- ~(codomain g = domain g) \/ % 3.24/3.40 domain (compose h (compose g a)) = codomain g % 3.24/3.40 |- ~(codomain g = domain g) \/ % 3.24/3.40 domain (compose h (compose g (compose a b))) = codomain g % 3.24/3.40 |- ~(codomain $X = domain g) \/ codomain (compose $X h) = codomain g % 3.24/3.40 |- ~(codomain $X = domain g) \/ domain (compose $X h) = domain $X % 3.24/3.40 |- compose (domain g) h = h % 3.24/3.40 |- ~(codomain $X = domain g) \/ % 3.24/3.40 codomain (compose $X (compose h a)) = codomain a % 3.24/3.40 |- ~(codomain $X = domain g) \/ % 3.24/3.40 domain (compose $X (compose h a)) = domain $X % 3.24/3.40 |- compose (domain g) (compose h a) = compose h a % 3.24/3.40 |- ~(codomain $_1 = codomain a) \/ % 3.24/3.40 domain (compose (codomain $_1) b) = codomain $_1 % 3.24/3.40 |- ~(codomain b = codomain a) \/ % 3.24/3.40 domain (compose (compose a b) b) = codomain g % 3.24/3.40 |- ~(codomain b = codomain a) \/ % 3.24/3.40 domain (compose (compose g (compose a b)) b) = domain g % 3.24/3.40 |- codomain (compose h a) = codomain a % 3.24/3.40 |- ~(codomain g = codomain a) \/ codomain (compose h b) = codomain b % 3.24/3.40 |- ~(codomain g = codomain $X) \/ % 3.24/3.40 codomain (compose h (codomain $X)) = codomain $X % 3.24/3.40 |- ~(codomain g = domain g) \/ % 3.24/3.40 codomain (compose h (compose g a)) = codomain a % 3.24/3.40 |- ~(codomain g = domain g) \/ % 3.24/3.40 codomain (compose h (compose g (compose a b))) = codomain b % 3.24/3.40 |- ~(codomain g = domain g) \/ % 3.24/3.40 codomain (compose h (compose h a)) = codomain a % 3.24/3.40 |- ~(codomain g = domain g) \/ codomain (compose h h) = codomain g % 3.24/3.40 |- ~(codomain a = domain $Y) \/ % 3.24/3.40 codomain (compose (compose h a) $Y) = codomain $Y % 3.24/3.40 |- ~(codomain a = domain $Y) \/ % 3.24/3.40 domain (compose (compose h a) $Y) = domain g % 3.24/3.40 |- ~(codomain a = domain g) \/ % 3.24/3.40 compose (compose h a) (compose (compose h a) (compose h a)) = % 3.24/3.40 compose (compose (compose h a) (compose h a)) (compose h a) % 3.24/3.40 |- compose (compose h a) (codomain a) = compose h a % 3.24/3.40 |- ~(codomain $_1 = codomain g) \/ % 3.24/3.40 codomain (compose (codomain $_1) a) = codomain a % 3.24/3.40 |- ~(codomain b = codomain g) \/ % 3.24/3.40 codomain (compose (compose a b) a) = codomain a % 3.24/3.40 |- ~(codomain a = codomain g) \/ % 3.24/3.40 codomain (compose (compose g a) a) = codomain a % 3.24/3.40 |- ~(codomain b = codomain g) \/ % 3.24/3.40 codomain (compose (compose g (compose a b)) a) = codomain a % 3.24/3.40 |- ~(codomain a = codomain g) \/ % 3.24/3.40 codomain (compose (compose h a) a) = codomain a % 3.24/3.40 |- ~(codomain $_1 = codomain a) \/ % 3.24/3.40 codomain (compose (codomain $_1) b) = codomain b % 3.24/3.40 |- ~(codomain b = codomain a) \/ % 3.24/3.40 codomain (compose (compose a b) b) = codomain a % 3.24/3.40 |- ~(codomain b = codomain a) \/ % 3.24/3.40 codomain (compose (compose g (compose a b)) b) = codomain a % 3.24/3.40 |- ~(codomain $_1 = codomain g) \/ % 3.24/3.40 domain (compose (codomain $_1) (compose a b)) = codomain $_1 % 3.24/3.40 |- ~(codomain b = codomain g) \/ % 3.24/3.40 domain (compose (compose a b) (compose a b)) = codomain b % 3.24/3.40 |- ~(codomain a = codomain g) \/ % 3.24/3.40 domain (compose (compose g a) (compose a b)) = domain g % 3.24/3.40 |- ~(codomain b = codomain g) \/ % 3.24/3.40 domain (compose (compose g (compose a b)) (compose a b)) = domain g % 3.24/3.40 |- ~(codomain a = codomain g) \/ % 3.24/3.40 domain (compose (compose h a) (compose a b)) = domain g % 3.24/3.40 |- ~(codomain $_1 = codomain g) \/ % 3.24/3.40 codomain (compose (codomain $_1) (compose a b)) = codomain b % 3.24/3.40 |- ~(codomain b = codomain g) \/ % 3.24/3.40 codomain (compose (compose a b) (compose a b)) = codomain b % 3.24/3.40 |- ~(codomain a = codomain g) \/ % 3.24/3.40 codomain (compose (compose g a) (compose a b)) = codomain b % 3.24/3.40 |- ~(codomain b = codomain g) \/ % 3.24/3.40 codomain (compose (compose g (compose a b)) (compose a b)) = codomain b % 3.24/3.40 |- ~(codomain a = codomain g) \/ % 3.24/3.40 codomain (compose (compose h a) (compose a b)) = codomain b % 3.24/3.40 |- ~(codomain $_1 = domain g) \/ % 3.24/3.40 codomain (compose (codomain $_1) (compose g a)) = codomain a % 3.24/3.40 |- ~(codomain b = domain g) \/ % 3.24/3.40 codomain (compose (compose a b) (compose g a)) = codomain a % 3.24/3.40 |- ~(codomain a = domain g) \/ % 3.24/3.40 codomain (compose (compose g a) (compose g a)) = codomain a % 3.24/3.40 |- ~(codomain b = domain g) \/ % 3.24/3.40 codomain (compose (compose g (compose a b)) (compose g a)) = codomain a % 3.24/3.40 |- ~(codomain a = domain g) \/ % 3.24/3.40 codomain (compose (compose h a) (compose g a)) = codomain a % 3.24/3.40 |- ~(codomain b = codomain g) \/ % 3.24/3.40 domain (compose (compose a b) a) = codomain b % 3.24/3.40 |- ~(codomain a = codomain g) \/ % 3.24/3.40 domain (compose (compose g a) a) = domain g % 3.24/3.40 |- ~(codomain b = codomain g) \/ % 3.24/3.40 domain (compose (compose g (compose a b)) a) = domain g % 3.24/3.40 |- ~(codomain a = codomain g) \/ % 3.24/3.40 domain (compose (compose h a) a) = domain g % 3.24/3.40 |- ~(codomain g = domain g) \/ % 3.24/3.40 domain (compose h (compose h a)) = codomain g % 3.24/3.40 |- ~(codomain g = domain g) \/ domain (compose h h) = codomain g % 3.24/3.40 |- ~(codomain $_1 = domain g) \/ % 3.24/3.40 codomain (compose (codomain $_1) (compose g (compose a b))) = codomain b % 3.24/3.40 |- ~(codomain b = domain g) \/ % 3.24/3.40 codomain (compose (compose a b) (compose g (compose a b))) = codomain b % 3.24/3.40 |- ~(codomain a = domain g) \/ % 3.24/3.40 codomain (compose (compose g a) (compose g (compose a b))) = codomain b % 3.24/3.40 |- ~(codomain b = domain g) \/ % 3.24/3.40 codomain (compose (compose g (compose a b)) (compose g (compose a b))) = % 3.24/3.40 codomain b % 3.24/3.40 |- ~(codomain a = domain g) \/ % 3.24/3.40 codomain (compose (compose h a) (compose g (compose a b))) = codomain b % 3.24/3.40 |- ~(codomain a = domain g) \/ % 3.24/3.40 codomain (compose (compose g a) (compose h a)) = codomain a % 3.24/3.40 |- ~(codomain a = domain g) \/ % 3.24/3.40 codomain (compose (compose g a) h) = codomain g % 3.24/3.40 |- ~(codomain a = domain g) \/ % 3.24/3.40 domain (compose (compose g a) (compose g a)) = codomain a % 3.24/3.40 |- ~(codomain a = domain g) \/ % 3.24/3.40 domain (compose (compose g a) (compose g (compose a b))) = codomain a % 3.24/3.40 |- ~(codomain a = domain g) \/ % 3.24/3.40 domain (compose (compose g a) (compose h a)) = codomain a % 3.24/3.40 |- ~(codomain a = domain g) \/ % 3.24/3.40 domain (compose (compose g a) h) = codomain a % 3.24/3.40 |- ~(codomain b = domain g) \/ % 3.24/3.40 domain (compose (compose a b) (compose g (compose a b))) = codomain g % 3.24/3.40 |- ~(codomain b = domain g) \/ % 3.24/3.40 domain (compose (compose g (compose a b)) (compose g (compose a b))) = % 3.24/3.40 codomain b % 3.24/3.40 |- ~(codomain a = domain g) \/ % 3.24/3.40 domain (compose (compose h a) (compose g (compose a b))) = codomain a % 3.24/3.40 |- ~(codomain b = domain g) \/ % 3.24/3.40 codomain (compose (compose a b) (compose h a)) = codomain a % 3.24/3.40 |- ~(codomain b = domain g) \/ % 3.24/3.40 codomain (compose (compose a b) h) = codomain g % 3.24/3.40 |- ~(codomain b = domain g) \/ % 3.24/3.40 domain (compose (compose a b) (compose g a)) = codomain g % 3.24/3.40 |- ~(codomain b = domain g) \/ % 3.24/3.40 domain (compose (compose a b) (compose h a)) = codomain g % 3.24/3.40 |- ~(codomain b = domain g) \/ % 3.24/3.40 domain (compose (compose a b) h) = codomain g % 3.24/3.40 |- ~(codomain b = domain g) \/ % 3.24/3.40 codomain (compose (compose g (compose a b)) h) = codomain g % 3.24/3.40 |- ~(codomain a = domain g) \/ % 3.24/3.40 codomain (compose (compose h a) h) = codomain g % 3.24/3.40 |- ~(codomain b = domain g) \/ % 3.24/3.40 domain (compose (compose g (compose a b)) h) = codomain b % 3.24/3.40 |- ~(codomain a = domain g) \/ % 3.24/3.40 domain (compose (compose h a) h) = codomain a % 3.24/3.40 |- ~(codomain $_36 = codomain g) \/ % 3.24/3.40 domain (compose (codomain $_36) a) = codomain $_36 % 3.24/3.40 |- ~(codomain $_36 = domain g) \/ % 3.24/3.40 domain (compose (codomain $_36) (compose g a)) = codomain $_36 % 3.24/3.40 |- ~(codomain $_36 = domain g) \/ % 3.24/3.40 domain (compose (codomain $_36) (compose g (compose a b))) = % 3.24/3.40 codomain $_36 % 3.24/3.40 |- ~(codomain $_36 = domain g) \/ % 3.24/3.40 domain (compose (codomain $_36) (compose h a)) = codomain $_36 % 3.24/3.40 |- ~(codomain $_36 = domain g) \/ % 3.24/3.40 domain (compose (codomain $_36) h) = codomain $_36 % 3.24/3.40 |- ~(domain $X = domain g) \/ domain (compose (domain $X) h) = domain $X % 3.24/3.40 |- ~(domain $_41 = domain g) \/ % 3.24/3.40 domain (compose (domain $_41) (compose g a)) = domain $_41 % 3.24/3.40 |- ~(domain $_41 = domain g) \/ % 3.24/3.40 domain (compose (domain $_41) (compose g (compose a b))) = domain $_41 % 3.24/3.40 |- ~(domain $_41 = domain g) \/ % 3.24/3.40 domain (compose (domain $_41) (compose h a)) = domain $_41 % 3.24/3.40 |- ~(codomain b = codomain $_43) \/ % 3.24/3.40 domain (compose (compose a b) (codomain $_43)) = codomain g % 3.24/3.40 |- ~(codomain a = codomain $_43) \/ % 3.24/3.40 domain (compose (compose g a) (codomain $_43)) = domain g % 3.24/3.40 |- ~(codomain b = codomain $_43) \/ % 3.24/3.40 domain (compose (compose g (compose a b)) (codomain $_43)) = domain g % 3.24/3.40 |- ~(codomain a = codomain $_43) \/ % 3.24/3.40 domain (compose (compose h a) (codomain $_43)) = domain g % 3.24/3.40 |- ~(codomain $_1 = domain $_45) \/ % 3.24/3.40 domain (compose (codomain $_1) (domain $_45)) = codomain $_1 % 3.24/3.41 |- ~(domain $X = domain $_45) \/ % 3.24/3.41 domain (compose (domain $X) (domain $_45)) = domain $X % 3.24/3.41 |- ~(codomain b = domain g) \/ % 3.24/3.41 domain (compose (compose g (compose a b)) (compose g a)) = codomain b % 3.24/3.41 |- ~(codomain a = domain g) \/ % 3.24/3.41 domain (compose (compose h a) (compose g a)) = codomain a % 3.24/3.41 |- ~(codomain b = domain g) \/ % 3.24/3.41 codomain (compose (compose g (compose a b)) (compose h a)) = codomain a % 3.24/3.41 |- ~(codomain b = domain g) \/ % 3.24/3.41 domain (compose (compose g (compose a b)) (compose h a)) = codomain b % 3.24/3.41 |- ~(codomain $_60 = domain g) \/ % 3.24/3.41 codomain (compose (codomain $_60) (compose h a)) = codomain a % 3.24/3.41 |- ~(codomain $_60 = domain g) \/ % 3.24/3.41 codomain (compose (codomain $_60) h) = codomain g % 3.24/3.41 |- ~(domain $X = domain g) \/ codomain (compose (domain $X) h) = codomain g % 3.24/3.41 |- ~(domain $_64 = codomain $X) \/ % 3.24/3.41 codomain (compose (domain $_64) (codomain $X)) = codomain $X % 3.24/3.41 |- ~(domain $_64 = domain g) \/ % 3.24/3.41 codomain (compose (domain $_64) (compose g a)) = codomain a % 3.24/3.41 |- ~(domain $_64 = domain g) \/ % 3.24/3.41 codomain (compose (domain $_64) (compose g (compose a b))) = codomain b % 3.24/3.41 |- ~(domain $_64 = domain g) \/ % 3.24/3.41 codomain (compose (domain $_64) (compose h a)) = codomain a % 3.24/3.41 |- ~(codomain b = codomain $_66) \/ % 3.24/3.41 codomain (compose (compose a b) (codomain $_66)) = codomain $_66 % 3.24/3.41 |- ~(codomain a = codomain $_66) \/ % 3.24/3.41 codomain (compose (compose g a) (codomain $_66)) = codomain $_66 % 3.24/3.41 |- ~(codomain b = codomain $_66) \/ % 3.24/3.41 codomain (compose (compose g (compose a b)) (codomain $_66)) = % 3.24/3.41 codomain $_66 % 3.24/3.41 |- ~(codomain a = codomain $_66) \/ % 3.24/3.41 codomain (compose (compose h a) (codomain $_66)) = codomain $_66 % 3.24/3.41 |- ~(codomain $_1 = domain $_68) \/ % 3.24/3.41 codomain (compose (codomain $_1) (domain $_68)) = domain $_68 % 3.24/3.41 |- ~(domain $X = domain $_68) \/ % 3.24/3.41 codomain (compose (domain $X) (domain $_68)) = domain $_68 % 3.24/3.41 |- ~(codomain $_70 = codomain $X) \/ % 3.24/3.41 codomain (compose (codomain $_70) (codomain $X)) = codomain $X % 3.24/3.41 |- ~(codomain a = domain g) \/ % 3.24/3.41 domain (compose (compose h a) (compose h a)) = codomain a % 3.24/3.41 |- ~(domain $_101 = codomain $X) \/ % 3.24/3.41 domain (compose (domain $_101) (codomain $X)) = domain $_101 % 3.24/3.41 |- ~(codomain $X = codomain $_103) \/ % 3.24/3.41 domain (compose (codomain $X) (codomain $_103)) = codomain $X % 3.24/3.41 |- ~(codomain a = domain g) \/ % 3.24/3.41 codomain (compose (compose h a) (compose h a)) = codomain a % 3.24/3.41 |- ~(a = compose $_129 a) \/ ~(codomain $_129 = codomain a) \/ % 3.24/3.41 ~(codomain g = codomain a) \/ $_129 = codomain a % 3.24/3.41 |- ~(codomain $_130 = codomain a) \/ ~(compose $_130 a = a) \/ % 3.24/3.41 codomain g = $_130 % 3.24/3.41 |- ~(b = compose $_133 b) \/ ~(codomain $_133 = codomain g) \/ % 3.24/3.41 $_133 = codomain a % 3.24/3.41 |- ~(codomain $_134 = codomain a) \/ ~(codomain a = codomain g) \/ % 3.24/3.41 ~(compose $_134 b = b) \/ codomain a = $_134 % 3.24/3.41 |- ~(codomain $_1 = domain $_139) \/ ~(codomain $_137 = codomain $_1) \/ % 3.24/3.41 compose $_137 (compose (codomain $_1) $_139) = % 3.24/3.41 compose (compose $_137 (codomain $_1)) $_139 % 3.24/3.41 |- ~(codomain $_137 = codomain g) \/ ~(codomain b = domain $_139) \/ % 3.24/3.41 compose $_137 (compose (compose a b) $_139) = % 3.24/3.41 compose (compose $_137 (compose a b)) $_139 % 3.24/3.41 |- ~(codomain $_137 = domain g) \/ ~(codomain b = domain $_139) \/ % 3.24/3.41 compose $_137 (compose (compose g (compose a b)) $_139) = % 3.24/3.41 compose (compose $_137 (compose g (compose a b))) $_139 % 3.24/3.41 |- ~(codomain $_137 = domain g) \/ ~(codomain a = domain $_139) \/ % 3.24/3.41 compose $_137 (compose (compose g a) $_139) = % 3.24/3.41 compose (compose $_137 (compose g a)) $_139 % 3.24/3.41 |- ~(codomain $_137 = domain g) \/ ~(codomain a = domain $_139) \/ % 3.24/3.41 compose $_137 (compose (compose h a) $_139) = % 3.24/3.41 compose (compose $_137 (compose h a)) $_139 % 3.24/3.41 |- ~(codomain $_137 = domain $X) \/ ~(domain $X = domain $_139) \/ % 3.24/3.41 compose $_137 (compose (domain $X) $_139) = % 3.24/3.41 compose (compose $_137 (domain $X)) $_139 % 3.24/3.41 |- ~(codomain $_137 = domain g) \/ ~(codomain g = domain $_139) \/ % 3.24/3.41 compose $_137 (compose h $_139) = compose (compose $_137 h) $_139 % 3.24/3.41 |- ~(codomain $_137 = domain $_138) \/ ~(codomain $_138 = codomain g) \/ % 3.24/3.41 compose $_137 (compose $_138 a) = compose (compose $_137 $_138) a % 3.24/3.41 |- ~(codomain $_137 = domain $_138) \/ ~(codomain $_138 = codomain a) \/ % 3.24/3.41 compose $_137 (compose $_138 b) = compose (compose $_137 $_138) b % 3.24/3.41 |- ~(codomain $_137 = domain $_138) \/ ~(codomain $_138 = codomain $X) \/ % 3.24/3.41 compose $_137 (compose $_138 (codomain $X)) = % 3.24/3.41 compose (compose $_137 $_138) (codomain $X) % 3.24/3.41 |- ~(codomain $_137 = domain $_138) \/ ~(codomain $_138 = codomain g) \/ % 3.24/3.41 compose $_137 (compose $_138 (compose a b)) = % 3.24/3.41 compose (compose $_137 $_138) (compose a b) % 3.24/3.41 |- ~(codomain $_137 = domain $_138) \/ ~(codomain $_138 = domain g) \/ % 3.24/3.41 compose $_137 (compose $_138 (compose g (compose a b))) = % 3.24/3.41 compose (compose $_137 $_138) (compose g (compose a b)) % 3.24/3.41 |- ~(codomain $_137 = domain $_138) \/ ~(codomain $_138 = domain g) \/ % 3.24/3.41 compose $_137 (compose $_138 (compose g a)) = % 3.24/3.41 compose (compose $_137 $_138) (compose g a) % 3.24/3.41 |- ~(codomain $_137 = domain $_138) \/ ~(codomain $_138 = domain g) \/ % 3.24/3.41 compose $_137 (compose $_138 (compose h a)) = % 3.24/3.41 compose (compose $_137 $_138) (compose h a) % 3.24/3.41 |- ~(codomain $_137 = domain $_138) \/ ~(codomain $_138 = domain $X) \/ % 3.24/3.41 compose $_137 (compose $_138 (domain $X)) = % 3.24/3.41 compose (compose $_137 $_138) (domain $X) % 3.24/3.41 |- ~(codomain $_137 = domain $_138) \/ ~(codomain $_138 = domain g) \/ % 3.24/3.41 compose $_137 (compose $_138 h) = compose (compose $_137 $_138) h % 3.24/3.41 |- ~(codomain $_1 = domain $_138) \/ ~(codomain $_138 = domain $_139) \/ % 3.24/3.41 compose (codomain $_1) (compose $_138 $_139) = % 3.24/3.41 compose (compose (codomain $_1) $_138) $_139 % 3.24/3.41 |- ~(codomain $_138 = domain $_139) \/ ~(codomain b = domain $_138) \/ % 3.24/3.41 compose (compose a b) (compose $_138 $_139) = % 3.24/3.41 compose (compose (compose a b) $_138) $_139 % 3.24/3.41 |- ~(codomain $_138 = domain $_139) \/ ~(codomain b = domain $_138) \/ % 3.24/3.41 compose (compose g (compose a b)) (compose $_138 $_139) = % 3.24/3.41 compose (compose (compose g (compose a b)) $_138) $_139 % 3.24/3.41 |- ~(codomain $_138 = domain $_139) \/ ~(codomain a = domain $_138) \/ % 3.24/3.41 compose (compose g a) (compose $_138 $_139) = % 3.24/3.41 compose (compose (compose g a) $_138) $_139 % 3.24/3.41 |- ~(codomain $_138 = domain $_139) \/ ~(codomain a = domain $_138) \/ % 3.24/3.41 compose (compose h a) (compose $_138 $_139) = % 3.24/3.41 compose (compose (compose h a) $_138) $_139 % 3.24/3.41 |- ~(codomain $_138 = domain $_139) \/ ~(domain $X = domain $_138) \/ % 3.24/3.41 compose (domain $X) (compose $_138 $_139) = % 3.24/3.41 compose (compose (domain $X) $_138) $_139 % 3.24/3.41 |- ~(codomain $_138 = domain $_139) \/ ~(codomain g = domain $_138) \/ % 3.24/3.41 compose h (compose $_138 $_139) = compose (compose h $_138) $_139 % 3.24/3.41 |- ~(codomain $_137 = codomain g) \/ ~(codomain a = domain $_139) \/ % 3.24/3.41 compose $_137 (compose a $_139) = compose (compose $_137 a) $_139 % 3.24/3.41 |- ~(codomain $_137 = codomain a) \/ ~(codomain b = domain $_139) \/ % 3.24/3.41 compose $_137 (compose b $_139) = compose (compose $_137 b) $_139 % 3.24/3.41 |- ~(codomain $_1 = domain $_139) \/ % 3.24/3.41 compose $_1 (compose (codomain $_1) $_139) = compose $_1 $_139 % 3.24/3.41 |- ~(codomain b = domain $_139) \/ % 3.24/3.41 compose g (compose (compose a b) $_139) = % 3.24/3.41 compose (compose g (compose a b)) $_139 % 3.24/3.41 |- ~(codomain a = domain g) \/ % 3.24/3.41 compose a (compose (compose g a) g) = % 3.24/3.41 compose (compose a (compose g a)) g % 3.24/3.41 |- ~(codomain b = domain g) \/ % 3.24/3.41 compose b (compose (compose g (compose a b)) g) = % 3.24/3.41 compose (compose b (compose g (compose a b))) g % 3.24/3.41 |- ~(codomain a = domain g) \/ % 3.24/3.41 compose a (compose (compose h a) g) = % 3.24/3.41 compose (compose a (compose h a)) g % 3.24/3.41 |- ~(codomain $_137 = domain $_139) \/ % 3.24/3.41 compose $_137 $_139 = compose (compose $_137 (domain $_139)) $_139 % 3.24/3.41 |- ~(codomain g = domain g) \/ % 3.24/3.41 compose g (compose h g) = compose (compose g h) g % 3.24/3.41 |- ~(codomain $_137 = domain $X) \/ % 3.24/3.41 compose $_137 $X = compose (compose $_137 $X) (codomain $X) % 3.24/3.41 |- ~(codomain g = domain g) \/ % 3.24/3.41 compose g (compose g (compose g a)) = % 3.24/3.41 compose (compose g g) (compose g a) % 3.24/3.41 |- ~(codomain g = domain g) \/ % 3.24/3.41 compose g (compose g (compose g (compose a b))) = % 3.24/3.41 compose (compose g g) (compose g (compose a b)) % 3.24/3.41 |- ~(codomain g = domain g) \/ % 3.24/3.41 compose g (compose g (compose h a)) = % 3.24/3.41 compose (compose g g) (compose h a) % 3.24/3.41 |- ~(codomain g = domain g) \/ % 3.24/3.41 compose g (compose g h) = compose (compose g g) h % 3.24/3.41 |- ~(codomain $_139 = domain $_139) \/ % 3.24/3.41 compose (codomain $_139) (compose $_139 $_139) = % 3.24/3.41 compose (compose (codomain $_139) $_139) $_139 % 3.24/3.41 |- ~(codomain b = codomain a) \/ % 3.24/3.41 compose (compose a b) (compose b b) = % 3.24/3.41 compose (compose (compose a b) b) b % 3.24/3.41 |- ~(codomain a = codomain g) \/ % 3.24/3.41 compose (compose g a) (compose a a) = % 3.24/3.41 compose (compose (compose g a) a) a % 3.24/3.41 |- ~(codomain b = codomain a) \/ % 3.24/3.41 compose (compose g (compose a b)) (compose b b) = % 3.24/3.41 compose (compose (compose g (compose a b)) b) b % 3.24/3.41 |- ~(codomain a = codomain g) \/ % 3.24/3.41 compose (compose h a) (compose a a) = % 3.24/3.41 compose (compose (compose h a) a) a % 3.24/3.41 |- ~(codomain $_138 = domain $_139) \/ % 3.24/3.41 compose (domain $_138) (compose $_138 $_139) = compose $_138 $_139 % 3.24/3.41 |- ~(codomain g = domain g) \/ % 3.24/3.41 compose h (compose g g) = compose (compose h g) g % 3.24/3.41 |- ~(codomain a = domain $_139) \/ % 3.24/3.41 compose g (compose a $_139) = compose (compose g a) $_139 % 3.24/3.41 |- ~(codomain b = domain $_139) \/ % 3.24/3.41 compose a (compose b $_139) = compose (compose a b) $_139 % 3.24/3.41 |- ~(codomain a = codomain g) \/ % 3.24/3.41 compose g (compose a a) = compose (compose g a) a % 3.24/3.41 |- compose g (compose a b) = compose (compose g a) b % 3.24/3.41 |- ~(codomain a = codomain $X) \/ % 3.24/3.41 compose g (compose a (codomain $X)) = % 3.24/3.41 compose (compose g a) (codomain $X) % 3.24/3.41 |- ~(codomain a = codomain g) \/ % 3.24/3.41 compose g (compose a (compose a b)) = % 3.24/3.41 compose (compose g a) (compose a b) % 3.24/3.41 |- ~(codomain a = domain g) \/ % 3.24/3.41 compose g (compose a (compose g (compose a b))) = % 3.24/3.41 compose (compose g a) (compose g (compose a b)) % 3.24/3.41 |- ~(codomain a = domain g) \/ % 3.24/3.41 compose g (compose a (compose g a)) = % 3.24/3.41 compose (compose g a) (compose g a) % 3.24/3.41 |- ~(codomain a = domain g) \/ % 3.24/3.41 compose g (compose a (compose h a)) = % 3.24/3.41 compose (compose g a) (compose h a) % 3.24/3.41 |- ~(codomain a = domain g) \/ % 3.24/3.41 compose g (compose a h) = compose (compose g a) h % 3.24/3.41 |- ~(b = compose g (compose a b)) \/ ~(codomain a = codomain g) \/ % 3.24/3.41 compose g a = codomain a % 3.24/3.41 |- ~(codomain $Z = codomain a) \/ ~(codomain a = codomain g) \/ % 3.24/3.41 ~(compose $Z b = compose g (compose a b)) \/ compose g a = $Z % 3.24/3.41 |- ~(codomain $X = codomain g) \/ % 3.24/3.41 ~(compose g (compose a b) = compose $X b) \/ $X = compose g a % 3.24/3.41 |- ~(codomain b = codomain g) \/ % 3.24/3.41 compose a (compose b a) = compose (compose a b) a % 3.24/3.41 |- ~(codomain b = codomain a) \/ % 3.24/3.41 compose a (compose b b) = compose (compose a b) b % 3.24/3.41 |- ~(codomain b = codomain $X) \/ % 3.24/3.41 compose a (compose b (codomain $X)) = % 3.24/3.41 compose (compose a b) (codomain $X) % 3.24/3.41 |- ~(codomain b = codomain g) \/ % 3.24/3.41 compose a (compose b (compose a b)) = % 3.24/3.41 compose (compose a b) (compose a b) % 3.24/3.41 |- ~(codomain b = domain g) \/ % 3.24/3.41 compose a (compose b (compose g a)) = % 3.24/3.41 compose (compose a b) (compose g a) % 3.24/3.41 |- ~(codomain b = domain g) \/ % 3.24/3.41 compose a (compose b (compose g (compose a b))) = % 3.24/3.41 compose (compose a b) (compose g (compose a b)) % 3.24/3.41 |- ~(codomain b = domain g) \/ % 3.24/3.41 compose a (compose b (compose h a)) = % 3.24/3.41 compose (compose a b) (compose h a) % 3.24/3.41 |- ~(codomain b = domain g) \/ % 3.24/3.41 compose a (compose b h) = compose (compose a b) h % 3.24/3.41 |- ~(codomain b = codomain g) \/ % 3.24/3.41 compose (codomain b) (compose (compose a b) (compose a b)) = % 3.24/3.41 compose (compose (codomain b) (compose a b)) (compose a b) % 3.24/3.41 |- ~(codomain a = domain g) \/ % 3.24/3.41 compose (codomain a) (compose (compose g a) (compose g a)) = % 3.24/3.41 compose (compose (codomain a) (compose g a)) (compose g a) % 3.24/3.41 |- ~(codomain b = domain g) \/ % 3.24/3.41 compose (codomain b) % 3.24/3.41 (compose (compose g (compose a b)) (compose g (compose a b))) = % 3.24/3.41 compose (compose (codomain b) (compose g (compose a b))) % 3.24/3.41 (compose g (compose a b)) % 3.24/3.41 |- ~(codomain a = domain g) \/ % 3.24/3.41 compose (codomain a) (compose (compose h a) (compose h a)) = % 3.24/3.41 compose (compose (codomain a) (compose h a)) (compose h a) % 3.24/3.41 |- ~(codomain g = domain g) \/ % 3.24/3.41 compose (codomain g) (compose h h) = compose (compose (codomain g) h) h % 3.24/3.41 |- ~(codomain a = codomain g) \/ % 3.24/3.41 compose (codomain a) (compose a a) = compose (compose (codomain a) a) a % 3.24/3.41 |- ~(codomain b = codomain a) \/ % 3.24/3.41 compose (codomain a) (compose b b) = compose b b % 3.24/3.41 |- ~(codomain b = codomain g) \/ % 3.24/3.41 compose g (compose (compose a b) a) = % 3.24/3.41 compose (compose g (compose a b)) a % 3.25/3.41 |- ~(codomain b = codomain a) \/ % 3.25/3.41 compose g (compose (compose a b) b) = % 3.25/3.41 compose (compose g (compose a b)) b % 3.25/3.41 |- ~(codomain b = codomain $X) \/ % 3.25/3.41 compose g (compose (compose a b) (codomain $X)) = % 3.25/3.41 compose (compose g (compose a b)) (codomain $X) % 3.25/3.42 |- ~(codomain b = codomain g) \/ % 3.25/3.42 compose g (compose (compose a b) (compose a b)) = % 3.25/3.42 compose (compose g (compose a b)) (compose a b) % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose g (compose (compose a b) (compose g a)) = % 3.25/3.42 compose (compose g (compose a b)) (compose g a) % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose g (compose (compose a b) (compose g (compose a b))) = % 3.25/3.42 compose (compose g (compose a b)) (compose g (compose a b)) % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose g (compose (compose a b) (compose h a)) = % 3.25/3.42 compose (compose g (compose a b)) (compose h a) % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose g (compose (compose a b) h) = % 3.25/3.42 compose (compose g (compose a b)) h % 3.25/3.42 |- ~(codomain $_1 = domain $_145) \/ % 3.25/3.42 compose (codomain $_1) (compose (codomain $_1) $_145) = % 3.25/3.42 compose (codomain $_1) $_145 % 3.25/3.42 |- ~(codomain b = domain $_145) \/ % 3.25/3.42 compose (compose a b) (compose (codomain b) $_145) = % 3.25/3.42 compose (compose a b) $_145 % 3.25/3.42 |- ~(codomain a = domain $_145) \/ % 3.25/3.42 compose (compose g a) (compose (codomain a) $_145) = % 3.25/3.42 compose (compose g a) $_145 % 3.25/3.42 |- ~(codomain b = domain $_145) \/ % 3.25/3.42 compose (compose g (compose a b)) (compose (codomain b) $_145) = % 3.25/3.42 compose (compose g (compose a b)) $_145 % 3.25/3.42 |- ~(codomain a = domain $_145) \/ % 3.25/3.42 compose (compose h a) (compose (codomain a) $_145) = % 3.25/3.42 compose (compose h a) $_145 % 3.25/3.42 |- ~(domain $X = domain $_145) \/ % 3.25/3.42 compose (domain $X) (compose (domain $X) $_145) = % 3.25/3.42 compose (domain $X) $_145 % 3.25/3.42 |- ~(codomain g = domain $_145) \/ % 3.25/3.42 compose h (compose (codomain g) $_145) = compose h $_145 % 3.25/3.42 |- ~(codomain $_144 = codomain g) \/ % 3.25/3.42 compose $_144 (compose (codomain $_144) a) = compose $_144 a % 3.25/3.42 |- ~(codomain $_144 = codomain a) \/ % 3.25/3.42 compose $_144 (compose (codomain $_144) b) = compose $_144 b % 3.25/3.42 |- ~(codomain $_144 = codomain $X) \/ % 3.25/3.42 compose $_144 (compose (codomain $_144) (codomain $X)) = % 3.25/3.42 compose $_144 (codomain $X) % 3.25/3.42 |- ~(codomain $_144 = codomain g) \/ % 3.25/3.42 compose $_144 (compose (codomain $_144) (compose a b)) = % 3.25/3.42 compose $_144 (compose a b) % 3.25/3.42 |- ~(codomain $_144 = domain g) \/ % 3.25/3.42 compose $_144 (compose (codomain $_144) (compose g a)) = % 3.25/3.42 compose $_144 (compose g a) % 3.25/3.42 |- ~(codomain $_144 = domain g) \/ % 3.25/3.42 compose $_144 (compose (codomain $_144) (compose g (compose a b))) = % 3.25/3.42 compose $_144 (compose g (compose a b)) % 3.25/3.42 |- ~(codomain $_144 = domain g) \/ % 3.25/3.42 compose $_144 (compose (codomain $_144) (compose h a)) = % 3.25/3.42 compose $_144 (compose h a) % 3.25/3.42 |- ~(codomain $_144 = domain $X) \/ % 3.25/3.42 compose $_144 (compose (codomain $_144) (domain $X)) = % 3.25/3.42 compose $_144 (domain $X) % 3.25/3.42 |- ~(codomain $_144 = domain g) \/ % 3.25/3.42 compose $_144 (compose (codomain $_144) h) = compose $_144 h % 3.25/3.42 |- ~(codomain $_1 = codomain a) \/ % 3.25/3.42 compose (codomain $_1) (compose (codomain $_1) b) = % 3.25/3.42 compose (codomain $_1) b % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose (compose a b) (compose (codomain b) h) = compose (compose a b) h % 3.25/3.42 |- ~(codomain a = domain g) \/ % 3.25/3.42 compose (compose g a) (compose (codomain a) h) = compose (compose g a) h % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose (compose g (compose a b)) (compose (codomain b) h) = % 3.25/3.42 compose (compose g (compose a b)) h % 3.25/3.42 |- ~(codomain a = domain g) \/ % 3.25/3.42 compose (compose h a) (compose (codomain a) h) = compose (compose h a) h % 3.25/3.42 |- ~(codomain g = domain g) \/ % 3.25/3.42 compose h (compose (codomain g) h) = compose h h % 3.25/3.42 |- ~(codomain g = codomain $X) \/ % 3.25/3.42 compose h (compose (codomain g) (codomain $X)) = compose h (codomain $X) % 3.25/3.42 |- ~(codomain g = domain g) \/ % 3.25/3.42 compose h (compose (codomain g) (compose g a)) = compose h (compose g a) % 3.25/3.42 |- ~(codomain g = domain g) \/ % 3.25/3.42 compose h (compose (codomain g) (compose g (compose a b))) = % 3.25/3.42 compose h (compose g (compose a b)) % 3.25/3.42 |- ~(codomain g = domain g) \/ % 3.25/3.42 compose h (compose (codomain g) (compose h a)) = compose h (compose h a) % 3.25/3.42 |- ~(codomain $_1 = codomain g) \/ % 3.25/3.42 compose (codomain $_1) (compose (codomain $_1) a) = % 3.25/3.42 compose (codomain $_1) a % 3.25/3.42 |- ~(codomain b = codomain g) \/ % 3.25/3.42 compose (compose a b) (compose (codomain b) a) = compose (compose a b) a % 3.25/3.42 |- ~(codomain a = codomain g) \/ % 3.25/3.42 compose (compose g a) (compose (codomain a) a) = compose (compose g a) a % 3.25/3.42 |- ~(codomain b = codomain g) \/ % 3.25/3.42 compose (compose g (compose a b)) (compose (codomain b) a) = % 3.25/3.42 compose (compose g (compose a b)) a % 3.25/3.42 |- ~(codomain a = codomain g) \/ % 3.25/3.42 compose (compose h a) (compose (codomain a) a) = compose (compose h a) a % 3.25/3.42 |- ~(codomain $_1 = domain $_151) \/ % 3.25/3.42 compose (codomain $_1) $_151 = % 3.25/3.42 compose (compose (codomain $_1) (domain $_151)) $_151 % 3.25/3.42 |- ~(domain $X = domain $_151) \/ % 3.25/3.42 compose (domain $X) $_151 = % 3.25/3.42 compose (compose (domain $X) (domain $_151)) $_151 % 3.25/3.42 |- ~(codomain $_150 = codomain g) \/ % 3.25/3.42 compose $_150 a = compose (compose $_150 (codomain g)) a % 3.25/3.42 |- ~(codomain $_150 = codomain a) \/ % 3.25/3.42 compose $_150 b = compose (compose $_150 (codomain a)) b % 3.25/3.42 |- ~(codomain $_150 = codomain $X) \/ % 3.25/3.42 compose $_150 (codomain $X) = % 3.25/3.42 compose (compose $_150 (codomain $X)) (codomain $X) % 3.25/3.42 |- ~(codomain $_150 = codomain g) \/ % 3.25/3.42 compose $_150 (compose a b) = % 3.25/3.42 compose (compose $_150 (codomain g)) (compose a b) % 3.25/3.42 |- ~(codomain $_150 = domain g) \/ % 3.25/3.42 compose $_150 (compose g a) = % 3.25/3.42 compose (compose $_150 (domain g)) (compose g a) % 3.25/3.42 |- ~(codomain $_150 = domain g) \/ % 3.25/3.42 compose $_150 (compose g (compose a b)) = % 3.25/3.42 compose (compose $_150 (domain g)) (compose g (compose a b)) % 3.25/3.42 |- ~(codomain $_150 = domain g) \/ % 3.25/3.42 compose $_150 (compose h a) = % 3.25/3.42 compose (compose $_150 (domain g)) (compose h a) % 3.25/3.42 |- ~(codomain $_150 = domain $X) \/ % 3.25/3.42 compose $_150 (domain $X) = % 3.25/3.42 compose (compose $_150 (domain $X)) (domain $X) % 3.25/3.42 |- ~(codomain $_150 = domain g) \/ % 3.25/3.42 compose $_150 h = compose (compose $_150 (domain g)) h % 3.25/3.42 |- ~(codomain $_1 = codomain g) \/ % 3.25/3.42 compose (codomain $_1) a = % 3.25/3.42 compose (compose (codomain $_1) (codomain g)) a % 3.25/3.42 |- ~(codomain $_1 = codomain a) \/ % 3.25/3.42 compose (codomain $_1) b = % 3.25/3.42 compose (compose (codomain $_1) (codomain a)) b % 3.25/3.42 |- ~(codomain b = codomain a) \/ % 3.25/3.42 compose (compose a b) b = compose (compose (compose a b) (codomain a)) b % 3.25/3.42 |- ~(codomain b = codomain a) \/ % 3.25/3.42 compose (compose g (compose a b)) b = % 3.25/3.42 compose (compose (compose g (compose a b)) (codomain a)) b % 3.25/3.42 |- ~(codomain g = codomain a) \/ % 3.25/3.42 compose h b = compose (compose h (codomain a)) b % 3.25/3.42 |- ~(codomain $_1 = domain g) \/ % 3.25/3.42 compose (codomain $_1) h = compose (compose (codomain $_1) (domain g)) h % 3.25/3.42 |- ~(domain $X = domain g) \/ % 3.25/3.42 compose (domain $X) h = compose (compose (domain $X) (domain g)) h % 3.25/3.42 |- ~(codomain $_1 = domain $_155) \/ % 3.25/3.42 compose (codomain $_1) $_155 = % 3.25/3.42 compose (compose (codomain $_1) $_155) (codomain $_155) % 3.25/3.42 |- ~(codomain b = domain $_155) \/ % 3.25/3.42 compose (compose a b) $_155 = % 3.25/3.42 compose (compose (compose a b) $_155) (codomain $_155) % 3.25/3.42 |- ~(codomain a = domain $_155) \/ % 3.25/3.42 compose (compose g a) $_155 = % 3.25/3.42 compose (compose (compose g a) $_155) (codomain $_155) % 3.25/3.42 |- ~(codomain b = domain $_155) \/ % 3.25/3.42 compose (compose g (compose a b)) $_155 = % 3.25/3.42 compose (compose (compose g (compose a b)) $_155) (codomain $_155) % 3.25/3.42 |- ~(codomain a = domain $_155) \/ % 3.25/3.42 compose (compose h a) $_155 = % 3.25/3.42 compose (compose (compose h a) $_155) (codomain $_155) % 3.25/3.42 |- ~(domain $X = domain $_155) \/ % 3.25/3.42 compose (domain $X) $_155 = % 3.25/3.42 compose (compose (domain $X) $_155) (codomain $_155) % 3.25/3.42 |- ~(codomain g = domain $_155) \/ % 3.25/3.42 compose h $_155 = compose (compose h $_155) (codomain $_155) % 3.25/3.42 |- ~(codomain $_156 = codomain g) \/ % 3.25/3.42 compose $_156 a = compose (compose $_156 a) (codomain a) % 3.25/3.42 |- ~(codomain $_156 = codomain a) \/ % 3.25/3.42 compose $_156 b = compose (compose $_156 b) (codomain b) % 3.25/3.42 |- ~(codomain $_156 = codomain g) \/ % 3.25/3.42 compose $_156 (compose a b) = % 3.25/3.42 compose (compose $_156 (compose a b)) (codomain b) % 3.25/3.42 |- ~(codomain $_156 = domain g) \/ % 3.25/3.42 compose $_156 (compose g a) = % 3.25/3.42 compose (compose $_156 (compose g a)) (codomain a) % 3.25/3.42 |- ~(codomain $_156 = domain g) \/ % 3.25/3.42 compose $_156 (compose g (compose a b)) = % 3.25/3.42 compose (compose $_156 (compose g (compose a b))) (codomain b) % 3.25/3.42 |- ~(codomain $_156 = domain g) \/ % 3.25/3.42 compose $_156 (compose h a) = % 3.25/3.42 compose (compose $_156 (compose h a)) (codomain a) % 3.25/3.42 |- ~(codomain $_156 = domain g) \/ % 3.25/3.42 compose $_156 h = compose (compose $_156 h) (codomain g) % 3.25/3.42 |- ~(codomain $_1 = codomain a) \/ % 3.25/3.42 compose (codomain $_1) b = % 3.25/3.42 compose (compose (codomain $_1) b) (codomain b) % 3.25/3.42 |- ~(codomain b = codomain a) \/ % 3.25/3.42 compose (compose a b) b = compose (compose (compose a b) b) (codomain a) % 3.25/3.42 |- ~(codomain b = codomain a) \/ % 3.25/3.42 compose (compose g (compose a b)) b = % 3.25/3.42 compose (compose (compose g (compose a b)) b) (codomain a) % 3.25/3.42 |- ~(codomain g = codomain a) \/ % 3.25/3.42 compose h b = compose (compose h b) (codomain b) % 3.25/3.42 |- ~(codomain $_1 = domain g) \/ % 3.25/3.42 compose (codomain $_1) h = % 3.25/3.42 compose (compose (codomain $_1) h) (codomain g) % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose (compose a b) h = compose (compose (compose a b) h) (codomain g) % 3.25/3.42 |- ~(codomain a = domain g) \/ % 3.25/3.42 compose (compose g a) h = compose (compose (compose g a) h) (codomain g) % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose (compose g (compose a b)) h = % 3.25/3.42 compose (compose (compose g (compose a b)) h) (codomain g) % 3.25/3.42 |- ~(codomain a = domain g) \/ % 3.25/3.42 compose (compose h a) h = compose (compose (compose h a) h) (codomain g) % 3.25/3.42 |- ~(domain $X = domain g) \/ % 3.25/3.42 compose (domain $X) h = compose (compose (domain $X) h) (codomain g) % 3.25/3.42 |- ~(codomain g = domain g) \/ % 3.25/3.42 compose h h = compose (compose h h) (codomain g) % 3.25/3.42 |- ~(codomain g = codomain $X) \/ % 3.25/3.42 compose h (codomain $X) = % 3.25/3.42 compose (compose h (codomain $X)) (codomain $X) % 3.25/3.42 |- ~(codomain g = domain g) \/ % 3.25/3.42 compose h (compose g a) = compose (compose h (compose g a)) (codomain a) % 3.25/3.42 |- ~(codomain g = domain g) \/ % 3.25/3.42 compose h (compose g (compose a b)) = % 3.25/3.42 compose (compose h (compose g (compose a b))) (codomain b) % 3.25/3.42 |- ~(codomain g = domain g) \/ % 3.25/3.42 compose h (compose h a) = compose (compose h (compose h a)) (codomain a) % 3.25/3.42 |- ~(codomain $_1 = codomain g) \/ % 3.25/3.42 compose (codomain $_1) a = % 3.25/3.42 compose (compose (codomain $_1) a) (codomain a) % 3.25/3.42 |- ~(codomain b = codomain g) \/ % 3.25/3.42 compose (compose a b) a = compose (compose (compose a b) a) (codomain a) % 3.25/3.42 |- ~(codomain a = codomain g) \/ % 3.25/3.42 compose (compose g a) a = compose (compose (compose g a) a) (codomain a) % 3.25/3.42 |- ~(codomain b = codomain g) \/ % 3.25/3.42 compose (compose g (compose a b)) a = % 3.25/3.42 compose (compose (compose g (compose a b)) a) (codomain a) % 3.25/3.42 |- ~(codomain a = codomain g) \/ % 3.25/3.42 compose (compose h a) a = compose (compose (compose h a) a) (codomain a) % 3.25/3.42 |- ~(codomain b = domain $_162) \/ % 3.25/3.42 compose (codomain g) (compose (compose a b) $_162) = % 3.25/3.42 compose (compose a b) $_162 % 3.25/3.42 |- ~(codomain a = domain $_162) \/ % 3.25/3.42 compose (domain g) (compose (compose g a) $_162) = % 3.25/3.42 compose (compose g a) $_162 % 3.25/3.42 |- ~(codomain b = domain $_162) \/ % 3.25/3.42 compose (domain g) (compose (compose g (compose a b)) $_162) = % 3.25/3.42 compose (compose g (compose a b)) $_162 % 3.25/3.42 |- ~(codomain a = domain $_162) \/ % 3.25/3.42 compose (domain g) (compose (compose h a) $_162) = % 3.25/3.42 compose (compose h a) $_162 % 3.25/3.42 |- ~(codomain g = domain $_162) \/ % 3.25/3.42 compose (domain g) (compose h $_162) = compose h $_162 % 3.25/3.42 |- ~(codomain $_161 = codomain g) \/ % 3.25/3.42 compose (domain $_161) (compose $_161 a) = compose $_161 a % 3.25/3.42 |- ~(codomain $_161 = codomain a) \/ % 3.25/3.42 compose (domain $_161) (compose $_161 b) = compose $_161 b % 3.25/3.42 |- ~(codomain $_161 = codomain $X) \/ % 3.25/3.42 compose (domain $_161) (compose $_161 (codomain $X)) = % 3.25/3.42 compose $_161 (codomain $X) % 3.25/3.42 |- ~(codomain $_161 = codomain g) \/ % 3.25/3.42 compose (domain $_161) (compose $_161 (compose a b)) = % 3.25/3.42 compose $_161 (compose a b) % 3.25/3.42 |- ~(codomain $_161 = domain g) \/ % 3.25/3.42 compose (domain $_161) (compose $_161 (compose g a)) = % 3.25/3.42 compose $_161 (compose g a) % 3.25/3.42 |- ~(codomain $_161 = domain g) \/ % 3.25/3.42 compose (domain $_161) (compose $_161 (compose g (compose a b))) = % 3.25/3.42 compose $_161 (compose g (compose a b)) % 3.25/3.42 |- ~(codomain $_161 = domain g) \/ % 3.25/3.42 compose (domain $_161) (compose $_161 (compose h a)) = % 3.25/3.42 compose $_161 (compose h a) % 3.25/3.42 |- ~(codomain $_161 = domain $X) \/ % 3.25/3.42 compose (domain $_161) (compose $_161 (domain $X)) = % 3.25/3.42 compose $_161 (domain $X) % 3.25/3.42 |- ~(codomain $_161 = domain g) \/ % 3.25/3.42 compose (domain $_161) (compose $_161 h) = compose $_161 h % 3.25/3.42 |- ~(codomain g = codomain a) \/ % 3.25/3.42 compose (domain g) (compose h b) = compose h b % 3.25/3.42 |- ~(codomain g = codomain $X) \/ % 3.25/3.42 compose (domain g) (compose h (codomain $X)) = compose h (codomain $X) % 3.25/3.42 |- ~(codomain g = domain g) \/ % 3.25/3.42 compose (codomain g) (compose h (compose g a)) = compose h (compose g a) % 3.25/3.42 |- ~(codomain g = domain g) \/ % 3.25/3.42 compose (codomain g) (compose h (compose g (compose a b))) = % 3.25/3.42 compose h (compose g (compose a b)) % 3.25/3.42 |- ~(codomain g = domain g) \/ % 3.25/3.42 compose (codomain g) (compose h (compose h a)) = compose h (compose h a) % 3.25/3.42 |- ~(codomain g = domain g) \/ % 3.25/3.42 compose (codomain g) (compose h h) = compose h h % 3.25/3.42 |- ~(codomain b = codomain g) \/ % 3.25/3.42 compose (codomain b) (compose (compose a b) a) = compose (compose a b) a % 3.25/3.42 |- ~(codomain a = codomain g) \/ % 3.25/3.42 compose (domain g) (compose (compose g a) a) = compose (compose g a) a % 3.25/3.42 |- ~(codomain b = codomain g) \/ % 3.25/3.42 compose (domain g) (compose (compose g (compose a b)) a) = % 3.25/3.42 compose (compose g (compose a b)) a % 3.25/3.42 |- ~(codomain a = codomain g) \/ % 3.25/3.42 compose (domain g) (compose (compose h a) a) = compose (compose h a) a % 3.25/3.42 |- ~(codomain b = codomain a) \/ % 3.25/3.42 compose (codomain g) (compose (compose a b) b) = compose (compose a b) b % 3.25/3.42 |- ~(codomain b = codomain a) \/ % 3.25/3.42 compose (domain g) (compose (compose g (compose a b)) b) = % 3.25/3.42 compose (compose g (compose a b)) b % 3.25/3.42 |- ~(codomain $_1 = domain g) \/ % 3.25/3.42 compose (codomain $_1) (compose (codomain $_1) h) = % 3.25/3.42 compose (codomain $_1) h % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose (codomain g) (compose (compose a b) h) = compose (compose a b) h % 3.25/3.42 |- ~(codomain a = domain g) \/ % 3.25/3.42 compose (codomain a) (compose (compose g a) h) = compose (compose g a) h % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose (codomain b) (compose (compose g (compose a b)) h) = % 3.25/3.42 compose (compose g (compose a b)) h % 3.25/3.42 |- ~(codomain a = domain g) \/ % 3.25/3.42 compose (codomain a) (compose (compose h a) h) = compose (compose h a) h % 3.25/3.42 |- ~(domain $X = domain g) \/ % 3.25/3.42 compose (domain $X) (compose (domain $X) h) = compose (domain $X) h % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose (compose a b) (compose (codomain b) (compose g a)) = % 3.25/3.42 compose (compose a b) (compose g a) % 3.25/3.42 |- ~(codomain a = domain g) \/ % 3.25/3.42 compose (compose g a) (compose (codomain a) (compose g a)) = % 3.25/3.42 compose (compose g a) (compose g a) % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose (compose g (compose a b)) (compose (codomain b) (compose g a)) = % 3.25/3.42 compose (compose g (compose a b)) (compose g a) % 3.25/3.42 |- ~(codomain a = domain g) \/ % 3.25/3.42 compose (compose h a) (compose (codomain a) (compose g a)) = % 3.25/3.42 compose (compose h a) (compose g a) % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose (compose a b) (compose (codomain b) (compose h a)) = % 3.25/3.42 compose (compose a b) (compose h a) % 3.25/3.42 |- ~(codomain a = domain g) \/ % 3.25/3.42 compose (compose g a) (compose (codomain a) (compose h a)) = % 3.25/3.42 compose (compose g a) (compose h a) % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose (compose g (compose a b)) (compose (codomain b) (compose h a)) = % 3.25/3.42 compose (compose g (compose a b)) (compose h a) % 3.25/3.42 |- ~(codomain a = domain g) \/ % 3.25/3.42 compose (compose h a) (compose (codomain a) (compose h a)) = % 3.25/3.42 compose (compose h a) (compose h a) % 3.25/3.42 |- ~(codomain $_1 = domain g) \/ % 3.25/3.42 compose (codomain $_1) (compose g a) = % 3.25/3.42 compose (compose (codomain $_1) (compose g a)) (codomain a) % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose (compose a b) (compose g a) = % 3.25/3.42 compose (compose (compose a b) (compose g a)) (codomain a) % 3.25/3.42 |- ~(codomain a = domain g) \/ % 3.25/3.42 compose (compose g a) (compose g a) = % 3.25/3.42 compose (compose (compose g a) (compose g a)) (codomain a) % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose (compose g (compose a b)) (compose g a) = % 3.25/3.42 compose (compose (compose g (compose a b)) (compose g a)) (codomain a) % 3.25/3.42 |- ~(codomain a = domain g) \/ % 3.25/3.42 compose (compose h a) (compose g a) = % 3.25/3.42 compose (compose (compose h a) (compose g a)) (codomain a) % 3.25/3.42 |- ~(domain $X = domain g) \/ % 3.25/3.42 compose (domain $X) (compose g a) = % 3.25/3.42 compose (compose (domain $X) (compose g a)) (codomain a) % 3.25/3.42 |- ~(codomain $_1 = domain g) \/ % 3.25/3.42 compose (codomain $_1) (compose h a) = % 3.25/3.42 compose (compose (codomain $_1) (compose h a)) (codomain a) % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose (compose a b) (compose h a) = % 3.25/3.42 compose (compose (compose a b) (compose h a)) (codomain a) % 3.25/3.42 |- ~(codomain a = domain g) \/ % 3.25/3.42 compose (compose g a) (compose h a) = % 3.25/3.42 compose (compose (compose g a) (compose h a)) (codomain a) % 3.25/3.42 |- ~(codomain b = domain g) \/ % 3.25/3.42 compose (compose g (compose a b)) (compose h a) = % 3.25/3.42 compose (compose (compose g (compose a b)) (compose h a)) (codomain a) % 3.25/3.43 |- ~(codomain a = domain g) \/ % 3.25/3.43 compose (compose h a) (compose h a) = % 3.25/3.43 compose (compose (compose h a) (compose h a)) (codomain a) % 3.25/3.43 |- ~(domain $X = domain g) \/ % 3.25/3.43 compose (domain $X) (compose h a) = % 3.25/3.43 compose (compose (domain $X) (compose h a)) (codomain a) % 3.25/3.43 |- ~(codomain a = codomain $X) \/ % 3.25/3.43 compose (domain g) (compose (compose g a) (codomain $X)) = % 3.25/3.43 compose (compose g a) (codomain $X) % 3.25/3.43 |- ~(codomain a = codomain g) \/ % 3.25/3.43 compose (domain g) (compose (compose g a) (compose a b)) = % 3.25/3.43 compose (compose g a) (compose a b) % 3.25/3.43 |- ~(codomain a = domain g) \/ % 3.25/3.43 compose (codomain a) (compose (compose g a) (compose g a)) = % 3.25/3.43 compose (compose g a) (compose g a) % 3.25/3.43 |- ~(codomain a = domain g) \/ % 3.25/3.43 compose (codomain a) (compose (compose g a) (compose g (compose a b))) = % 3.25/3.43 compose (compose g a) (compose g (compose a b)) % 3.25/3.43 |- ~(codomain a = domain g) \/ % 3.25/3.43 compose (codomain a) (compose (compose g a) (compose h a)) = % 3.25/3.43 compose (compose g a) (compose h a) % 3.25/3.43 |- ~(codomain a = codomain $X) \/ % 3.25/3.43 compose (domain g) (compose (compose h a) (codomain $X)) = % 3.25/3.43 compose (compose h a) (codomain $X) % 3.25/3.43 |- ~(codomain a = codomain g) \/ % 3.25/3.43 compose (domain g) (compose (compose h a) (compose a b)) = % 3.25/3.43 compose (compose h a) (compose a b) % 3.25/3.43 |- ~(codomain a = domain g) \/ % 3.25/3.43 compose (codomain a) (compose (compose h a) (compose g a)) = % 3.25/3.43 compose (compose h a) (compose g a) % 3.25/3.43 |- ~(codomain a = domain g) \/ % 3.25/3.43 compose (codomain a) (compose (compose h a) (compose g (compose a b))) = % 3.25/3.43 compose (compose h a) (compose g (compose a b)) % 3.25/3.43 |- ~(codomain a = domain g) \/ % 3.25/3.43 compose (codomain a) (compose (compose h a) (compose h a)) = % 3.25/3.43 compose (compose h a) (compose h a) % 3.25/3.43 |- ~(codomain $_1 = codomain g) \/ % 3.25/3.43 compose (codomain $_1) (compose a b) = % 3.25/3.43 compose (compose (codomain $_1) (codomain g)) (compose a b) % 3.25/3.43 |- ~(codomain $_1 = domain g) \/ % 3.25/3.43 compose (codomain $_1) (compose g a) = % 3.25/3.43 compose (compose (codomain $_1) (domain g)) (compose g a) % 3.25/3.43 |- ~(domain $X = domain g) \/ % 3.25/3.43 compose (domain $X) (compose g a) = % 3.25/3.43 compose (compose (domain $X) (domain g)) (compose g a) % 3.25/3.43 |- ~(codomain $_1 = domain g) \/ % 3.25/3.43 compose (codomain $_1) (compose h a) = % 3.25/3.43 compose (compose (codomain $_1) (domain g)) (compose h a) % 3.25/3.43 |- ~(domain $X = domain g) \/ % 3.25/3.43 compose (domain $X) (compose h a) = % 3.25/3.43 compose (compose (domain $X) (domain g)) (compose h a) % 3.25/3.43 |- ~(codomain a = codomain $X) \/ % 3.25/3.43 compose (compose g a) (compose (codomain a) (codomain $X)) = % 3.25/3.43 compose (compose g a) (codomain $X) % 3.25/3.43 |- ~(codomain a = codomain g) \/ % 3.25/3.43 compose (compose g a) (compose (codomain a) (compose a b)) = % 3.25/3.43 compose (compose g a) (compose a b) % 3.25/3.43 |- ~(codomain a = domain g) \/ % 3.25/3.43 compose (compose g a) (compose (codomain a) (compose g (compose a b))) = % 3.25/3.43 compose (compose g a) (compose g (compose a b)) % 3.25/3.43 |- ~(codomain a = codomain $X) \/ % 3.25/3.43 compose (compose h a) (compose (codomain a) (codomain $X)) = % 3.25/3.43 compose (compose h a) (codomain $X) % 3.25/3.43 |- ~(codomain a = codomain g) \/ % 3.25/3.43 compose (compose h a) (compose (codomain a) (compose a b)) = % 3.25/3.43 compose (compose h a) (compose a b) % 3.25/3.43 |- ~(codomain a = domain g) \/ % 3.25/3.43 compose (compose h a) (compose (codomain a) (compose g (compose a b))) = % 3.25/3.43 compose (compose h a) (compose g (compose a b)) % 3.25/3.43 |- ~(codomain a = codomain $X) \/ % 3.25/3.43 compose (compose g a) (codomain $X) = % 3.25/3.43 compose (compose (compose g a) (codomain $X)) (codomain $X) % 3.25/3.43 |- ~(codomain a = codomain g) \/ % 3.25/3.43 compose (compose g a) (compose a b) = % 3.25/3.43 compose (compose (compose g a) (compose a b)) (codomain b) % 3.25/3.43 |- ~(codomain a = domain g) \/ % 3.25/3.43 compose (compose g a) (compose g (compose a b)) = % 3.25/3.43 compose (compose (compose g a) (compose g (compose a b))) (codomain b) % 3.25/3.43 |- ~(codomain a = codomain $X) \/ % 3.25/3.43 compose (compose h a) (codomain $X) = % 3.25/3.43 compose (compose (compose h a) (codomain $X)) (codomain $X) % 3.25/3.43 |- ~(codomain a = codomain g) \/ % 3.25/3.43 compose (compose h a) (compose a b) = % 3.25/3.43 compose (compose (compose h a) (compose a b)) (codomain b) % 3.25/3.43 |- ~(codomain a = domain g) \/ % 3.25/3.43 compose (compose h a) (compose g (compose a b)) = % 3.25/3.43 compose (compose (compose h a) (compose g (compose a b))) (codomain b) % 3.25/3.43 |- ~(codomain $_1 = codomain g) \/ % 3.25/3.43 compose (codomain $_1) (compose a b) = % 3.25/3.43 compose (compose (codomain $_1) (compose a b)) (codomain b) % 3.25/3.43 |- ~(codomain b = codomain g) \/ % 3.25/3.43 compose (compose a b) (compose a b) = % 3.25/3.43 compose (compose (compose a b) (compose a b)) (codomain b) % 3.25/3.43 |- ~(codomain b = codomain g) \/ % 3.25/3.43 compose (compose g (compose a b)) (compose a b) = % 3.25/3.43 compose (compose (compose g (compose a b)) (compose a b)) (codomain b) % 3.27/3.43 |- ~(codomain b = codomain g) \/ % 3.27/3.43 compose (codomain b) (compose (compose a b) (compose a b)) = % 3.27/3.43 compose (compose a b) (compose a b) % 3.27/3.43 |- ~(codomain b = codomain g) \/ % 3.27/3.43 compose (domain g) (compose (compose g (compose a b)) (compose a b)) = % 3.27/3.43 compose (compose g (compose a b)) (compose a b) % 3.27/3.43 |- ~(codomain $_1 = domain g) \/ % 3.27/3.43 compose (codomain $_1) (compose (codomain $_1) (compose g a)) = % 3.27/3.43 compose (codomain $_1) (compose g a) % 3.27/3.43 |- ~(codomain b = domain g) \/ % 3.27/3.43 compose (codomain g) (compose (compose a b) (compose g a)) = % 3.27/3.43 compose (compose a b) (compose g a) % 3.27/3.43 |- ~(codomain b = domain g) \/ % 3.27/3.43 compose (codomain b) (compose (compose g (compose a b)) (compose g a)) = % 3.27/3.43 compose (compose g (compose a b)) (compose g a) % 3.27/3.43 |- ~(domain $X = domain g) \/ % 3.27/3.43 compose (domain $X) (compose (domain $X) (compose g a)) = % 3.27/3.43 compose (domain $X) (compose g a) % 3.27/3.43 |- ~(codomain $_1 = domain g) \/ % 3.27/3.43 compose (codomain $_1) (compose (codomain $_1) (compose h a)) = % 3.27/3.43 compose (codomain $_1) (compose h a) % 3.27/3.43 |- ~(codomain b = domain g) \/ % 3.27/3.43 compose (codomain g) (compose (compose a b) (compose h a)) = % 3.27/3.43 compose (compose a b) (compose h a) % 3.27/3.43 |- ~(codomain b = domain g) \/ % 3.27/3.43 compose (codomain b) (compose (compose g (compose a b)) (compose h a)) = % 3.27/3.43 compose (compose g (compose a b)) (compose h a) % 3.27/3.43 |- ~(domain $X = domain g) \/ % 3.27/3.43 compose (domain $X) (compose (domain $X) (compose h a)) = % 3.27/3.43 compose (domain $X) (compose h a) % 3.27/3.43 |- ~(codomain b = codomain $X) \/ % 3.27/3.43 compose (compose a b) (compose (codomain b) (codomain $X)) = % 3.27/3.43 compose (compose a b) (codomain $X) % 3.27/3.43 |- ~(codomain b = codomain g) \/ % 3.27/3.43 compose (compose a b) (compose (codomain b) (compose a b)) = % 3.27/3.43 compose (compose a b) (compose a b) % 3.27/3.43 |- ~(codomain b = domain g) \/ % 3.27/3.43 compose (compose a b) (compose (codomain b) (compose g (compose a b))) = % 3.27/3.43 compose (compose a b) (compose g (compose a b)) % 3.27/3.43 |- ~(codomain $_1 = codomain g) \/ % 3.27/3.43 compose (codomain $_1) (compose (codomain $_1) (compose a b)) = % 3.27/3.43 compose (codomain $_1) (compose a b) % 3.27/3.43 |- ~(codomain b = codomain g) \/ % 3.27/3.43 compose (compose g (compose a b)) (compose (codomain b) (compose a b)) = % 3.27/3.43 compose (compose g (compose a b)) (compose a b) % 3.27/3.43 |- ~(codomain b = codomain $X) \/ % 3.27/3.43 compose (compose a b) (codomain $X) = % 3.27/3.43 compose (compose (compose a b) (codomain $X)) (codomain $X) % 3.27/3.43 |- ~(codomain b = domain g) \/ % 3.27/3.43 compose (compose a b) (compose g (compose a b)) = % 3.27/3.43 compose (compose (compose a b) (compose g (compose a b))) (codomain b) % 3.27/3.43 |- ~(codomain b = codomain $X) \/ % 3.27/3.43 compose (codomain g) (compose (compose a b) (codomain $X)) = % 3.27/3.43 compose (compose a b) (codomain $X) % 3.27/3.43 |- ~(codomain b = domain g) \/ % 3.27/3.43 compose (codomain g) (compose (compose a b) (compose g (compose a b))) = % 3.27/3.43 compose (compose a b) (compose g (compose a b)) % 3.27/3.43 |- ~(codomain b = codomain a) \/ b = compose b (codomain a) % 3.27/3.43 |- ~(codomain b = domain g) \/ % 3.27/3.43 compose (compose g (compose a b)) % 3.27/3.43 (compose (codomain b) (compose g (compose a b))) = % 3.27/3.43 compose (compose g (compose a b)) (compose g (compose a b)) % 3.27/3.43 |- ~(codomain $_1 = domain g) \/ % 3.27/3.43 compose (codomain $_1) (compose g (compose a b)) = % 3.27/3.43 compose (compose (codomain $_1) (compose g (compose a b))) (codomain b) % 3.27/3.43 |- ~(codomain b = domain g) \/ % 3.27/3.43 compose (compose g (compose a b)) (compose g (compose a b)) = % 3.27/3.43 compose (compose (compose g (compose a b)) (compose g (compose a b))) % 3.27/3.43 (codomain b) % 3.27/3.43 |- ~(domain $X = domain g) \/ % 3.27/3.43 compose (domain $X) (compose g (compose a b)) = % 3.27/3.43 compose (compose (domain $X) (compose g (compose a b))) (codomain b) % 3.27/3.43 |- ~(codomain b = codomain $X) \/ % 3.27/3.43 compose (domain g) (compose (compose g (compose a b)) (codomain $X)) = % 3.27/3.43 compose (compose g (compose a b)) (codomain $X) % 3.27/3.43 |- ~(codomain b = domain g) \/ % 3.27/3.43 compose (codomain b) % 3.27/3.43 (compose (compose g (compose a b)) (compose g (compose a b))) = % 3.27/3.43 compose (compose g (compose a b)) (compose g (compose a b)) % 3.27/3.43 |- ~(codomain $_1 = domain g) \/ % 3.27/3.43 compose (codomain $_1) (compose g (compose a b)) = % 3.27/3.43 compose (compose (codomain $_1) (domain g)) (compose g (compose a b)) % 3.27/3.43 |- ~(domain $X = domain g) \/ % 3.27/3.43 compose (domain $X) (compose g (compose a b)) = % 3.27/3.43 compose (compose (domain $X) (domain g)) (compose g (compose a b)) % 3.27/3.43 |- ~(codomain b = codomain $X) \/ % 3.27/3.43 compose (compose g (compose a b)) (compose (codomain b) (codomain $X)) = % 3.27/3.43 compose (compose g (compose a b)) (codomain $X) % 3.27/3.43 |- ~(codomain b = codomain $X) \/ % 3.27/3.43 compose (compose g (compose a b)) (codomain $X) = % 3.27/3.43 compose (compose (compose g (compose a b)) (codomain $X)) (codomain $X) % 3.27/3.43 |- ~(codomain $_1 = domain g) \/ % 3.27/3.43 compose (codomain $_1) % 3.27/3.43 (compose (codomain $_1) (compose g (compose a b))) = % 3.27/3.43 compose (codomain $_1) (compose g (compose a b)) % 3.27/3.43 |- ~(domain $X = domain g) \/ % 3.27/3.43 compose (domain $X) (compose (domain $X) (compose g (compose a b))) = % 3.27/3.43 compose (domain $X) (compose g (compose a b)) % 3.27/3.43 |- ~(codomain b = codomain g) \/ % 3.27/3.43 compose (codomain b) (compose a b) = compose a b % 3.27/3.43 |- ~(codomain $_240 = codomain $X) \/ % 3.27/3.43 compose (codomain $_240) (codomain $X) = % 3.27/3.43 compose (compose (codomain $_240) (codomain $X)) (codomain $X) % 3.27/3.43 |- ~(codomain $_1 = domain $_246) \/ % 3.27/3.43 compose (codomain $_1) (domain $_246) = % 3.27/3.43 compose (compose (codomain $_1) (domain $_246)) (domain $_246) % 3.27/3.43 |- ~(domain $X = domain $_246) \/ % 3.27/3.43 compose (domain $X) (domain $_246) = % 3.27/3.43 compose (compose (domain $X) (domain $_246)) (domain $_246) % 3.27/3.43 |- ~(codomain $_1 = codomain $_264) \/ % 3.27/3.43 compose (codomain $_1) (compose (codomain $_1) (codomain $_264)) = % 3.27/3.43 compose (codomain $_1) (codomain $_264) % 3.27/3.43 |- ~(codomain $_1 = domain $_266) \/ % 3.27/3.43 compose (codomain $_1) (compose (codomain $_1) (domain $_266)) = % 3.27/3.43 compose (codomain $_1) (domain $_266) % 3.27/3.43 |- ~(domain $X = domain $_278) \/ % 3.27/3.43 compose (domain $X) (compose (domain $X) (domain $_278)) = % 3.27/3.43 compose (domain $X) (domain $_278) % 3.27/3.43 |- ~(domain $_289 = codomain $X) \/ % 3.27/3.43 compose (domain $_289) (compose (domain $_289) (codomain $X)) = % 3.27/3.43 compose (domain $_289) (codomain $X) % 3.27/3.43 |- ~(domain $_301 = codomain $X) \/ % 3.27/3.43 compose (domain $_301) (codomain $X) = % 3.27/3.43 compose (compose (domain $_301) (codomain $X)) (codomain $X) % 3.27/3.43 |- ~(codomain $_312 = domain g) \/ % 3.27/3.43 compose $_312 (compose g (compose a b)) = % 3.27/3.43 compose (compose $_312 h) (compose a b) % 3.27/3.43 |- ~(codomain $_312 = codomain g) \/ ~(codomain g = domain g) \/ % 3.27/3.43 compose $_312 (compose h (compose g a)) = % 3.27/3.43 compose (compose $_312 h) (compose g a) % 3.27/3.43 |- ~(codomain $_312 = codomain g) \/ ~(codomain g = domain g) \/ % 3.27/3.43 compose $_312 (compose h (compose g (compose a b))) = % 3.27/3.43 compose (compose $_312 h) (compose g (compose a b)) % 3.27/3.43 |- ~(codomain $_312 = codomain g) \/ ~(codomain g = domain g) \/ % 3.27/3.43 compose $_312 (compose h (compose h a)) = % 3.27/3.43 compose (compose $_312 h) (compose h a) % 3.27/3.43 |- ~(codomain $_312 = codomain g) \/ ~(codomain g = domain g) \/ % 3.27/3.43 compose $_312 (compose h h) = compose (compose $_312 h) h % 3.27/3.43 |- ~(codomain b = domain g) \/ ~(codomain g = domain $_313) \/ % 3.27/3.43 compose (compose a b) (compose h $_313) = % 3.27/3.43 compose (compose (compose a b) h) $_313 % 3.27/3.43 |- ~(codomain a = domain g) \/ ~(codomain g = domain $_313) \/ % 3.27/3.43 compose (compose g a) (compose h $_313) = % 3.27/3.43 compose (compose (compose g a) h) $_313 % 3.27/3.43 |- ~(codomain b = domain g) \/ ~(codomain g = domain $_313) \/ % 3.27/3.43 compose (compose g (compose a b)) (compose h $_313) = % 3.27/3.43 compose (compose (compose g (compose a b)) h) $_313 % 3.27/3.43 |- ~(codomain a = domain g) \/ ~(codomain g = domain $_313) \/ % 3.27/3.43 compose (compose h a) (compose h $_313) = % 3.27/3.43 compose (compose (compose h a) h) $_313 % 3.27/3.43 |- ~(codomain g = domain $_313) \/ ~(codomain g = domain g) \/ % 3.27/3.43 compose h (compose h $_313) = compose (compose h h) $_313 % 3.27/3.43 |- ~(codomain g = domain g) \/ % 3.27/3.43 compose g (compose h (compose g a)) = % 3.27/3.43 compose (compose g h) (compose g a) % 3.27/3.43 |- ~(codomain g = domain g) \/ % 3.27/3.43 compose g (compose h (compose g (compose a b))) = % 3.27/3.43 compose (compose g h) (compose g (compose a b)) % 3.27/3.43 |- ~(codomain g = domain g) \/ % 3.27/3.43 compose g (compose h (compose h a)) = % 3.27/3.43 compose (compose g h) (compose h a) % 3.27/3.43 |- ~(codomain g = domain g) \/ % 3.27/3.43 compose g (compose h h) = compose (compose g h) h % 3.27/3.43 |- ~(codomain g = domain g) \/ % 3.27/3.43 compose (codomain g) (compose h g) = compose (compose (codomain g) h) g % 3.27/3.43 |- ~(codomain g = domain g) \/ % 3.27/3.43 compose h (compose h g) = compose (compose h h) g % 3.27/3.43 |- ~(codomain $_1 = domain g) \/ % 3.27/3.43 compose (codomain $_1) (compose g (compose a b)) = % 3.27/3.43 compose (compose (codomain $_1) h) (compose a b) % 3.27/3.43 |- ~(codomain b = domain g) \/ % 3.27/3.43 compose (compose a b) (compose g (compose a b)) = % 3.27/3.43 compose (compose (compose a b) h) (compose a b) % 3.27/3.43 |- ~(codomain a = domain g) \/ % 3.27/3.43 compose (compose g a) (compose g (compose a b)) = % 3.27/3.43 compose (compose (compose g a) h) (compose a b) % 3.27/3.44 |- ~(codomain b = domain g) \/ % 3.27/3.44 compose (compose g (compose a b)) (compose g (compose a b)) = % 3.27/3.44 compose (compose (compose g (compose a b)) h) (compose a b) % 3.27/3.44 |- ~(codomain a = domain g) \/ % 3.27/3.44 compose (compose h a) (compose g (compose a b)) = % 3.27/3.44 compose (compose (compose h a) h) (compose a b) % 3.27/3.44 |- ~(domain $X = domain g) \/ % 3.27/3.44 compose (domain $X) (compose g (compose a b)) = % 3.27/3.44 compose (compose (domain $X) h) (compose a b) % 3.27/3.44 |- ~(codomain g = domain g) \/ % 3.27/3.44 compose h (compose g (compose a b)) = % 3.27/3.44 compose (compose h h) (compose a b) % 3.27/3.44 |- ~(codomain $_1 = codomain g) \/ ~(codomain g = domain g) \/ % 3.27/3.44 compose (codomain $_1) (compose h h) = % 3.27/3.44 compose (compose (codomain $_1) h) h % 3.27/3.44 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.44 compose (compose a b) (compose h h) = % 3.27/3.44 compose (compose (compose a b) h) h % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.44 compose (compose g a) (compose h h) = % 3.27/3.44 compose (compose (compose g a) h) h % 3.27/3.44 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.44 compose (compose g (compose a b)) (compose h h) = % 3.27/3.44 compose (compose (compose g (compose a b)) h) h % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.44 compose (compose h a) (compose h h) = % 3.27/3.44 compose (compose (compose h a) h) h % 3.27/3.44 |- ~(codomain g = codomain $X) \/ ~(codomain g = domain g) \/ % 3.27/3.44 compose h (compose h (codomain $X)) = % 3.27/3.44 compose (compose h h) (codomain $X) % 3.27/3.44 |- ~(codomain g = domain g) \/ % 3.27/3.44 compose h (compose h (compose g a)) = % 3.27/3.44 compose (compose h h) (compose g a) % 3.27/3.44 |- ~(codomain g = domain g) \/ % 3.27/3.44 compose h (compose h (compose g (compose a b))) = % 3.27/3.44 compose (compose h h) (compose g (compose a b)) % 3.27/3.44 |- ~(codomain g = domain g) \/ % 3.27/3.44 compose h (compose h (compose h a)) = % 3.27/3.44 compose (compose h h) (compose h a) % 3.27/3.44 |- ~(codomain $_1 = codomain g) \/ ~(codomain g = domain g) \/ % 3.27/3.44 compose (codomain $_1) (compose h (compose g a)) = % 3.27/3.44 compose (compose (codomain $_1) h) (compose g a) % 3.27/3.44 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.44 compose (compose a b) (compose h (compose g a)) = % 3.27/3.44 compose (compose (compose a b) h) (compose g a) % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.44 compose (compose g a) (compose h (compose g a)) = % 3.27/3.44 compose (compose (compose g a) h) (compose g a) % 3.27/3.44 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.44 compose (compose g (compose a b)) (compose h (compose g a)) = % 3.27/3.44 compose (compose (compose g (compose a b)) h) (compose g a) % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.44 compose (compose h a) (compose h (compose g a)) = % 3.27/3.44 compose (compose (compose h a) h) (compose g a) % 3.27/3.44 |- ~(codomain g = domain g) \/ % 3.27/3.44 compose (codomain g) (compose h (compose g a)) = % 3.27/3.44 compose (compose (codomain g) h) (compose g a) % 3.27/3.44 |- ~(codomain $_1 = codomain g) \/ ~(codomain g = domain g) \/ % 3.27/3.44 compose (codomain $_1) (compose h (compose h a)) = % 3.27/3.44 compose (compose (codomain $_1) h) (compose h a) % 3.27/3.44 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.44 compose (compose a b) (compose h (compose h a)) = % 3.27/3.44 compose (compose (compose a b) h) (compose h a) % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.44 compose (compose g a) (compose h (compose h a)) = % 3.27/3.44 compose (compose (compose g a) h) (compose h a) % 3.27/3.44 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.44 compose (compose g (compose a b)) (compose h (compose h a)) = % 3.27/3.44 compose (compose (compose g (compose a b)) h) (compose h a) % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.44 compose (compose h a) (compose h (compose h a)) = % 3.27/3.44 compose (compose (compose h a) h) (compose h a) % 3.27/3.44 |- ~(codomain g = domain g) \/ % 3.27/3.44 compose (codomain g) (compose h (compose h a)) = % 3.27/3.44 compose (compose (codomain g) h) (compose h a) % 3.27/3.44 |- ~(codomain $_1 = domain $_322) \/ ~(codomain $_322 = codomain g) \/ % 3.27/3.44 compose (codomain $_1) (compose $_322 a) = % 3.27/3.44 compose (compose (codomain $_1) $_322) a % 3.27/3.44 |- ~(codomain $_322 = codomain g) \/ ~(codomain b = domain $_322) \/ % 3.27/3.44 compose (compose a b) (compose $_322 a) = % 3.27/3.44 compose (compose (compose a b) $_322) a % 3.27/3.44 |- ~(codomain $_322 = codomain g) \/ ~(codomain a = domain $_322) \/ % 3.27/3.44 compose (compose g a) (compose $_322 a) = % 3.27/3.44 compose (compose (compose g a) $_322) a % 3.27/3.44 |- ~(codomain $_322 = codomain g) \/ ~(codomain b = domain $_322) \/ % 3.27/3.44 compose (compose g (compose a b)) (compose $_322 a) = % 3.27/3.44 compose (compose (compose g (compose a b)) $_322) a % 3.27/3.44 |- ~(codomain $_322 = codomain g) \/ ~(codomain a = domain $_322) \/ % 3.27/3.44 compose (compose h a) (compose $_322 a) = % 3.27/3.44 compose (compose (compose h a) $_322) a % 3.27/3.44 |- ~(codomain $_322 = codomain g) \/ ~(codomain g = domain $_322) \/ % 3.27/3.44 compose h (compose $_322 a) = compose (compose h $_322) a % 3.27/3.44 |- ~(codomain $_321 = codomain a) \/ ~(codomain a = codomain g) \/ % 3.27/3.44 compose $_321 (compose a a) = compose (compose $_321 a) a % 3.27/3.44 |- ~(codomain $_321 = codomain a) \/ ~(codomain b = codomain g) \/ % 3.27/3.44 compose $_321 (compose b a) = compose (compose $_321 b) a % 3.27/3.44 |- ~(codomain $X = codomain g) \/ ~(codomain $_321 = codomain $X) \/ % 3.27/3.44 compose $_321 (compose (codomain $X) a) = % 3.27/3.44 compose (compose $_321 (codomain $X)) a % 3.27/3.44 |- ~(codomain $_321 = codomain b) \/ ~(codomain b = codomain g) \/ % 3.27/3.44 compose $_321 (compose (compose a b) a) = % 3.27/3.44 compose (compose $_321 (compose a b)) a % 3.27/3.44 |- ~(codomain $_321 = domain g) \/ ~(codomain b = codomain g) \/ % 3.27/3.44 compose $_321 (compose (compose g (compose a b)) a) = % 3.27/3.44 compose (compose $_321 (compose g (compose a b))) a % 3.27/3.44 |- ~(codomain $_321 = domain g) \/ ~(codomain a = codomain g) \/ % 3.27/3.44 compose $_321 (compose (compose g a) a) = % 3.27/3.44 compose (compose $_321 (compose g a)) a % 3.27/3.44 |- ~(codomain $_321 = domain g) \/ ~(codomain a = codomain g) \/ % 3.27/3.44 compose $_321 (compose (compose h a) a) = % 3.27/3.44 compose (compose $_321 (compose h a)) a % 3.27/3.44 |- ~(codomain $_321 = domain g) \/ % 3.27/3.44 compose $_321 (compose h a) = compose (compose $_321 h) a % 3.27/3.44 |- ~(codomain $X = codomain g) \/ % 3.27/3.44 compose g (compose (codomain $X) a) = % 3.27/3.44 compose (compose g (codomain $X)) a % 3.27/3.44 |- ~(codomain b = codomain g) \/ % 3.27/3.44 compose b (compose (compose a b) a) = % 3.27/3.44 compose (compose b (compose a b)) a % 3.27/3.44 |- ~(codomain $_1 = domain g) \/ % 3.27/3.44 compose (codomain $_1) (compose h a) = % 3.27/3.44 compose (compose (codomain $_1) h) a % 3.27/3.44 |- ~(codomain b = domain g) \/ % 3.27/3.44 compose (compose a b) (compose h a) = % 3.27/3.44 compose (compose (compose a b) h) a % 3.27/3.44 |- ~(codomain a = domain g) \/ % 3.27/3.44 compose (compose g a) (compose h a) = % 3.27/3.44 compose (compose (compose g a) h) a % 3.27/3.44 |- ~(codomain b = domain g) \/ % 3.27/3.44 compose (compose g (compose a b)) (compose h a) = % 3.27/3.44 compose (compose (compose g (compose a b)) h) a % 3.27/3.44 |- ~(codomain a = domain g) \/ % 3.27/3.44 compose (compose h a) (compose h a) = % 3.27/3.44 compose (compose (compose h a) h) a % 3.27/3.44 |- ~(domain $X = domain g) \/ % 3.27/3.44 compose (domain $X) (compose h a) = compose (compose (domain $X) h) a % 3.27/3.44 |- ~(codomain g = domain g) \/ % 3.27/3.44 compose h (compose h a) = compose (compose h h) a % 3.27/3.44 |- ~(codomain $_1 = codomain a) \/ ~(codomain b = codomain g) \/ % 3.27/3.44 compose (codomain $_1) (compose b a) = % 3.27/3.44 compose (compose (codomain $_1) b) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.44 compose (compose a b) (compose b a) = % 3.27/3.44 compose (compose (compose a b) b) a % 3.27/3.44 |- ~(codomain b = codomain g) \/ % 3.27/3.44 compose (compose g a) (compose b a) = % 3.27/3.44 compose (compose g (compose a b)) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.44 compose (compose g (compose a b)) (compose b a) = % 3.27/3.44 compose (compose (compose g (compose a b)) b) a % 3.27/3.44 |- ~(codomain b = codomain g) \/ % 3.27/3.44 compose (compose h a) (compose b a) = % 3.27/3.44 compose (compose g (compose a b)) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.44 compose h (compose b a) = compose (compose h b) a % 3.27/3.44 |- ~(codomain b = codomain g) \/ % 3.27/3.44 compose (codomain a) (compose b a) = compose b a % 3.27/3.44 |- ~(codomain a = codomain g) \/ % 3.27/3.44 compose h (compose a a) = compose (compose h a) a % 3.27/3.44 |- ~(codomain $X = codomain g) \/ % 3.27/3.44 compose h (compose (codomain $X) a) = % 3.27/3.44 compose (compose h (codomain $X)) a % 3.27/3.44 |- ~(codomain b = codomain g) \/ % 3.27/3.44 compose h (compose (compose a b) a) = % 3.27/3.44 compose (compose g (compose a b)) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.44 compose h (compose (compose g a) a) = % 3.27/3.44 compose (compose h (compose g a)) a % 3.27/3.44 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.44 compose h (compose (compose g (compose a b)) a) = % 3.27/3.44 compose (compose h (compose g (compose a b))) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.44 compose h (compose (compose h a) a) = % 3.27/3.44 compose (compose h (compose h a)) a % 3.27/3.44 |- ~(codomain $_1 = codomain a) \/ ~(codomain a = codomain g) \/ % 3.27/3.44 compose (codomain $_1) (compose a a) = % 3.27/3.44 compose (compose (codomain $_1) a) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.44 compose (compose a b) (compose a a) = % 3.27/3.44 compose (compose (compose a b) a) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.44 compose (compose g (compose a b)) (compose a a) = % 3.27/3.44 compose (compose (compose g (compose a b)) a) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ % 3.27/3.44 compose (codomain a) (compose a a) = compose a a % 3.27/3.44 |- ~(codomain $_1 = domain g) \/ ~(codomain a = codomain g) \/ % 3.27/3.44 compose (codomain $_1) (compose (compose g a) a) = % 3.27/3.44 compose (compose (codomain $_1) (compose g a)) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.44 compose (compose a b) (compose (compose g a) a) = % 3.27/3.44 compose (compose (compose a b) (compose g a)) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.44 compose (compose g a) (compose (compose g a) a) = % 3.27/3.44 compose (compose (compose g a) (compose g a)) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.44 compose (compose g (compose a b)) (compose (compose g a) a) = % 3.27/3.44 compose (compose (compose g (compose a b)) (compose g a)) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.44 compose (compose h a) (compose (compose g a) a) = % 3.27/3.44 compose (compose (compose h a) (compose g a)) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(domain $X = domain g) \/ % 3.27/3.44 compose (domain $X) (compose (compose g a) a) = % 3.27/3.44 compose (compose (domain $X) (compose g a)) a % 3.27/3.44 |- ~(codomain $_1 = domain g) \/ ~(codomain a = codomain g) \/ % 3.27/3.44 compose (codomain $_1) (compose (compose h a) a) = % 3.27/3.44 compose (compose (codomain $_1) (compose h a)) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.44 compose (compose a b) (compose (compose h a) a) = % 3.27/3.44 compose (compose (compose a b) (compose h a)) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.44 compose (compose g a) (compose (compose h a) a) = % 3.27/3.44 compose (compose (compose g a) (compose h a)) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.44 compose (compose g (compose a b)) (compose (compose h a) a) = % 3.27/3.44 compose (compose (compose g (compose a b)) (compose h a)) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.44 compose (compose h a) (compose (compose h a) a) = % 3.27/3.44 compose (compose (compose h a) (compose h a)) a % 3.27/3.44 |- ~(codomain a = codomain g) \/ ~(domain $X = domain g) \/ % 3.27/3.44 compose (domain $X) (compose (compose h a) a) = % 3.27/3.44 compose (compose (domain $X) (compose h a)) a % 3.27/3.44 |- ~(codomain $_1 = domain $_334) \/ ~(codomain $_334 = codomain a) \/ % 3.27/3.44 compose (codomain $_1) (compose $_334 b) = % 3.27/3.44 compose (compose (codomain $_1) $_334) b % 3.27/3.44 |- ~(codomain $_334 = codomain a) \/ ~(codomain b = domain $_334) \/ % 3.27/3.44 compose (compose a b) (compose $_334 b) = % 3.27/3.44 compose (compose (compose a b) $_334) b % 3.27/3.44 |- ~(codomain $_334 = codomain a) \/ ~(codomain b = domain $_334) \/ % 3.27/3.44 compose (compose g (compose a b)) (compose $_334 b) = % 3.27/3.44 compose (compose (compose g (compose a b)) $_334) b % 3.27/3.44 |- ~(codomain $_334 = codomain a) \/ ~(codomain a = domain $_334) \/ % 3.27/3.44 compose (compose g a) (compose $_334 b) = % 3.27/3.44 compose (compose (compose g a) $_334) b % 3.27/3.44 |- ~(codomain $_334 = codomain a) \/ ~(codomain a = domain $_334) \/ % 3.27/3.44 compose (compose h a) (compose $_334 b) = % 3.27/3.44 compose (compose (compose h a) $_334) b % 3.27/3.44 |- ~(codomain $_334 = codomain a) \/ ~(codomain g = domain $_334) \/ % 3.27/3.44 compose h (compose $_334 b) = compose (compose h $_334) b % 3.27/3.44 |- ~(codomain $_333 = codomain g) \/ % 3.27/3.44 compose $_333 (compose a b) = compose (compose $_333 a) b % 3.27/3.44 |- ~(codomain $_333 = codomain a) \/ ~(codomain b = codomain a) \/ % 3.27/3.44 compose $_333 (compose b b) = compose (compose $_333 b) b % 3.27/3.44 |- ~(codomain $X = codomain a) \/ ~(codomain $_333 = codomain $X) \/ % 3.27/3.44 compose $_333 (compose (codomain $X) b) = % 3.27/3.44 compose (compose $_333 (codomain $X)) b % 3.27/3.44 |- ~(codomain $_333 = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.44 compose $_333 (compose (compose a b) b) = % 3.27/3.44 compose (compose $_333 (compose a b)) b % 3.27/3.44 |- ~(codomain $_333 = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.44 compose $_333 (compose (compose g (compose a b)) b) = % 3.27/3.44 compose (compose $_333 (compose g (compose a b))) b % 3.27/3.44 |- ~(codomain $_333 = domain g) \/ % 3.27/3.44 compose $_333 (compose g (compose a b)) = % 3.27/3.44 compose (compose $_333 (compose g a)) b % 3.27/3.44 |- ~(codomain $_333 = domain g) \/ % 3.27/3.44 compose $_333 (compose g (compose a b)) = % 3.27/3.44 compose (compose $_333 (compose h a)) b % 3.27/3.44 |- ~(codomain $_333 = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.44 compose $_333 (compose h b) = compose (compose $_333 h) b % 3.27/3.44 |- ~(codomain $X = codomain a) \/ % 3.27/3.44 compose a (compose (codomain $X) b) = % 3.27/3.44 compose (compose a (codomain $X)) b % 3.27/3.44 |- ~(codomain $_1 = codomain g) \/ % 3.27/3.44 compose (codomain $_1) (compose a b) = % 3.27/3.44 compose (compose (codomain $_1) a) b % 3.27/3.44 |- ~(codomain b = codomain g) \/ % 3.27/3.44 compose (compose a b) (compose a b) = % 3.27/3.44 compose (compose (compose a b) a) b % 3.27/3.44 |- ~(codomain b = codomain g) \/ % 3.27/3.44 compose (compose g (compose a b)) (compose a b) = % 3.27/3.44 compose (compose (compose g (compose a b)) a) b % 3.27/3.44 |- ~(codomain a = codomain g) \/ % 3.27/3.44 compose (compose g a) (compose a b) = % 3.27/3.44 compose (compose (compose g a) a) b % 3.27/3.44 |- ~(codomain a = codomain g) \/ % 3.27/3.44 compose (compose h a) (compose a b) = % 3.27/3.44 compose (compose (compose h a) a) b % 3.27/3.45 |- compose g (compose a b) = compose (compose h a) b % 3.27/3.45 |- ~(codomain a = codomain g) \/ compose h a = compose g a % 3.27/3.45 |- ~(b = compose g (compose a b)) \/ ~(codomain a = codomain g) \/ % 3.27/3.45 compose h a = codomain a % 3.27/3.45 |- ~(codomain $Z = codomain a) \/ ~(codomain a = codomain g) \/ % 3.27/3.45 ~(compose $Z b = compose g (compose a b)) \/ compose h a = $Z % 3.27/3.45 |- ~(codomain $X = codomain g) \/ % 3.27/3.45 ~(compose g (compose a b) = compose $X b) \/ $X = compose h a % 3.27/3.45 |- ~(codomain $_1 = domain g) \/ % 3.27/3.45 compose (codomain $_1) (compose g (compose a b)) = % 3.27/3.45 compose (compose (codomain $_1) (compose g a)) b % 3.27/3.45 |- ~(codomain b = domain g) \/ % 3.27/3.45 compose (compose a b) (compose g (compose a b)) = % 3.27/3.45 compose (compose (compose a b) (compose g a)) b % 3.27/3.45 |- ~(codomain a = domain g) \/ % 3.27/3.45 compose (compose g a) (compose g (compose a b)) = % 3.27/3.45 compose (compose (compose g a) (compose g a)) b % 3.27/3.45 |- ~(codomain b = domain g) \/ % 3.27/3.45 compose (compose g (compose a b)) (compose g (compose a b)) = % 3.27/3.45 compose (compose (compose g (compose a b)) (compose g a)) b % 3.27/3.45 |- ~(codomain a = domain g) \/ % 3.27/3.45 compose (compose h a) (compose g (compose a b)) = % 3.27/3.45 compose (compose (compose h a) (compose g a)) b % 3.27/3.45 |- ~(domain $X = domain g) \/ % 3.27/3.45 compose (domain $X) (compose g (compose a b)) = % 3.27/3.45 compose (compose (domain $X) (compose g a)) b % 3.27/3.45 |- ~(codomain g = domain g) \/ % 3.27/3.45 compose h (compose g (compose a b)) = % 3.27/3.45 compose (compose h (compose g a)) b % 3.27/3.45 |- ~(codomain $_1 = domain g) \/ % 3.27/3.45 compose (codomain $_1) (compose g (compose a b)) = % 3.27/3.45 compose (compose (codomain $_1) (compose h a)) b % 3.27/3.45 |- ~(codomain b = domain g) \/ % 3.27/3.45 compose (compose a b) (compose g (compose a b)) = % 3.27/3.45 compose (compose (compose a b) (compose h a)) b % 3.27/3.45 |- ~(codomain a = domain g) \/ % 3.27/3.45 compose (compose g a) (compose g (compose a b)) = % 3.27/3.45 compose (compose (compose g a) (compose h a)) b % 3.27/3.45 |- ~(codomain b = domain g) \/ % 3.27/3.45 compose (compose g (compose a b)) (compose g (compose a b)) = % 3.27/3.45 compose (compose (compose g (compose a b)) (compose h a)) b % 3.27/3.45 |- ~(codomain a = domain g) \/ % 3.27/3.45 compose (compose h a) (compose g (compose a b)) = % 3.27/3.45 compose (compose (compose h a) (compose h a)) b % 3.27/3.45 |- ~(domain $X = domain g) \/ % 3.27/3.45 compose (domain $X) (compose g (compose a b)) = % 3.27/3.45 compose (compose (domain $X) (compose h a)) b % 3.27/3.45 |- ~(codomain g = domain g) \/ % 3.27/3.45 compose h (compose g (compose a b)) = % 3.27/3.45 compose (compose h (compose h a)) b % 3.27/3.45 |- ~(codomain $_1 = codomain a) \/ ~(codomain b = codomain a) \/ % 3.27/3.45 compose (codomain $_1) (compose b b) = % 3.27/3.45 compose (compose (codomain $_1) b) b % 3.27/3.45 |- ~(codomain b = codomain a) \/ % 3.27/3.45 compose (compose g a) (compose b b) = % 3.27/3.45 compose (compose g (compose a b)) b % 3.27/3.45 |- ~(codomain b = codomain a) \/ % 3.27/3.45 compose (compose h a) (compose b b) = % 3.27/3.45 compose (compose g (compose a b)) b % 3.27/3.45 |- ~(codomain b = codomain a) \/ ~(codomain g = codomain a) \/ % 3.27/3.45 compose h (compose b b) = compose (compose h b) b % 3.27/3.45 |- ~(codomain $_1 = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.45 compose (codomain $_1) (compose h b) = % 3.27/3.45 compose (compose (codomain $_1) h) b % 3.27/3.45 |- ~(codomain b = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.45 compose (compose a b) (compose h b) = % 3.27/3.45 compose (compose (compose a b) h) b % 3.27/3.45 |- ~(codomain a = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.45 compose (compose g a) (compose h b) = % 3.27/3.45 compose (compose (compose g a) h) b % 3.27/3.45 |- ~(codomain b = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.45 compose (compose g (compose a b)) (compose h b) = % 3.27/3.45 compose (compose (compose g (compose a b)) h) b % 3.27/3.45 |- ~(codomain a = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.45 compose (compose h a) (compose h b) = % 3.27/3.45 compose (compose (compose h a) h) b % 3.27/3.45 |- ~(codomain g = codomain a) \/ ~(domain $X = domain g) \/ % 3.27/3.45 compose (domain $X) (compose h b) = compose (compose (domain $X) h) b % 3.27/3.45 |- ~(codomain a = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.45 compose h (compose h b) = compose (compose h h) b % 3.27/3.45 |- ~(codomain $X = codomain a) \/ ~(codomain g = codomain $X) \/ % 3.27/3.45 compose h (compose (codomain $X) b) = % 3.27/3.45 compose (compose h (codomain $X)) b % 3.27/3.45 |- ~(codomain b = codomain a) \/ % 3.27/3.45 compose h (compose (compose a b) b) = % 3.27/3.45 compose (compose g (compose a b)) b % 3.27/3.45 |- ~(codomain b = codomain a) \/ ~(codomain g = domain g) \/ % 3.27/3.45 compose h (compose (compose g (compose a b)) b) = % 3.27/3.45 compose (compose h (compose g (compose a b))) b % 3.27/3.45 |- ~(codomain $X = codomain a) \/ % 3.27/3.45 compose (compose g a) (compose (codomain $X) b) = % 3.27/3.45 compose (compose (compose g a) (codomain $X)) b % 3.27/3.45 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.45 compose (compose g a) (compose (compose a b) b) = % 3.27/3.45 compose (compose (compose g a) (compose a b)) b % 3.27/3.45 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.45 compose (compose g a) (compose (compose g (compose a b)) b) = % 3.27/3.45 compose (compose (compose g a) (compose g (compose a b))) b % 3.27/3.45 |- ~(codomain $X = codomain a) \/ % 3.27/3.45 compose (compose h a) (compose (codomain $X) b) = % 3.27/3.45 compose (compose (compose h a) (codomain $X)) b % 3.27/3.45 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.45 compose (compose h a) (compose (compose a b) b) = % 3.27/3.45 compose (compose (compose h a) (compose a b)) b % 3.27/3.45 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.45 compose (compose h a) (compose (compose g (compose a b)) b) = % 3.27/3.45 compose (compose (compose h a) (compose g (compose a b))) b % 3.27/3.45 |- ~(codomain $_1 = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.45 compose (codomain $_1) (compose (compose a b) b) = % 3.27/3.45 compose (compose (codomain $_1) (compose a b)) b % 3.27/3.45 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.45 compose (compose a b) (compose (compose a b) b) = % 3.27/3.45 compose (compose (compose a b) (compose a b)) b % 3.27/3.45 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.45 compose (compose g (compose a b)) (compose (compose a b) b) = % 3.27/3.45 compose (compose (compose g (compose a b)) (compose a b)) b % 3.27/3.45 |- ~(codomain $_355 = domain g) \/ ~(codomain b = domain $_355) \/ % 3.27/3.45 compose (compose a b) (compose $_355 h) = % 3.27/3.45 compose (compose (compose a b) $_355) h % 3.27/3.45 |- ~(codomain $_355 = domain g) \/ ~(codomain a = domain $_355) \/ % 3.27/3.45 compose (compose g a) (compose $_355 h) = % 3.27/3.45 compose (compose (compose g a) $_355) h % 3.27/3.45 |- ~(codomain $_355 = domain g) \/ ~(codomain b = domain $_355) \/ % 3.27/3.45 compose (compose g (compose a b)) (compose $_355 h) = % 3.27/3.45 compose (compose (compose g (compose a b)) $_355) h % 3.27/3.45 |- ~(codomain $_355 = domain g) \/ ~(codomain a = domain $_355) \/ % 3.27/3.45 compose (compose h a) (compose $_355 h) = % 3.27/3.45 compose (compose (compose h a) $_355) h % 3.27/3.45 |- ~(codomain $_355 = domain g) \/ ~(codomain g = domain $_355) \/ % 3.27/3.45 compose h (compose $_355 h) = compose (compose h $_355) h % 3.27/3.45 |- ~(codomain $_354 = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.45 compose $_354 (compose a h) = compose (compose $_354 a) h % 3.27/3.45 |- ~(codomain $_354 = codomain a) \/ ~(codomain b = domain g) \/ % 3.27/3.45 compose $_354 (compose b h) = compose (compose $_354 b) h % 3.27/3.45 |- ~(codomain $_354 = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.45 compose $_354 (compose (compose a b) h) = % 3.27/3.45 compose (compose $_354 (compose a b)) h % 3.27/3.45 |- ~(codomain $_354 = codomain a) \/ ~(codomain a = domain g) \/ % 3.27/3.45 compose $_354 (compose (compose g a) h) = % 3.27/3.45 compose (compose $_354 (compose g a)) h % 3.27/3.45 |- ~(codomain $_354 = codomain b) \/ ~(codomain b = domain g) \/ % 3.27/3.45 compose $_354 (compose (compose g (compose a b)) h) = % 3.27/3.45 compose (compose $_354 (compose g (compose a b))) h % 3.27/3.45 |- ~(codomain $_354 = codomain a) \/ ~(codomain a = domain g) \/ % 3.27/3.45 compose $_354 (compose (compose h a) h) = % 3.27/3.45 compose (compose $_354 (compose h a)) h % 3.27/3.45 |- ~(codomain g = domain g) \/ % 3.27/3.45 compose (codomain g) (compose g h) = compose (compose (codomain g) g) h % 3.27/3.45 |- ~(codomain g = domain g) \/ % 3.27/3.45 compose h (compose g h) = compose (compose h g) h % 3.27/3.45 |- ~(codomain a = domain g) \/ % 3.27/3.45 compose a (compose (compose g a) h) = % 3.27/3.45 compose (compose a (compose g a)) h % 3.27/3.45 |- ~(codomain b = domain g) \/ % 3.27/3.45 compose b (compose (compose g (compose a b)) h) = % 3.27/3.45 compose (compose b (compose g (compose a b))) h % 3.27/3.45 |- ~(codomain a = domain g) \/ % 3.27/3.45 compose a (compose (compose h a) h) = % 3.27/3.45 compose (compose a (compose h a)) h % 3.27/3.45 |- ~(codomain $_1 = codomain a) \/ ~(codomain b = domain g) \/ % 3.27/3.45 compose (codomain $_1) (compose b h) = % 3.27/3.45 compose (compose (codomain $_1) b) h % 3.27/3.45 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.45 compose (compose a b) (compose b h) = % 3.27/3.45 compose (compose (compose a b) b) h % 3.27/3.45 |- ~(codomain b = domain g) \/ % 3.27/3.45 compose (compose g a) (compose b h) = % 3.27/3.45 compose (compose g (compose a b)) h % 3.27/3.45 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.45 compose (compose g (compose a b)) (compose b h) = % 3.27/3.45 compose (compose (compose g (compose a b)) b) h % 3.27/3.45 |- ~(codomain b = domain g) \/ % 3.27/3.45 compose (compose h a) (compose b h) = % 3.27/3.45 compose (compose g (compose a b)) h % 3.27/3.45 |- ~(codomain b = domain g) \/ % 3.27/3.45 compose (codomain a) (compose b h) = compose b h % 3.27/3.45 |- ~(codomain $X = domain g) \/ ~(codomain g = codomain $X) \/ % 3.27/3.45 compose h (compose (codomain $X) h) = % 3.27/3.45 compose (compose h (codomain $X)) h % 3.27/3.45 |- ~(codomain b = domain g) \/ % 3.27/3.45 compose h (compose (compose a b) h) = % 3.27/3.45 compose (compose g (compose a b)) h % 3.27/3.45 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.45 compose h (compose (compose g a) h) = % 3.27/3.45 compose (compose h (compose g a)) h % 3.27/3.45 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.45 compose h (compose (compose g (compose a b)) h) = % 3.27/3.45 compose (compose h (compose g (compose a b))) h % 3.27/3.45 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.45 compose h (compose (compose h a) h) = % 3.27/3.45 compose (compose h (compose h a)) h % 3.27/3.45 |- ~(codomain $_1 = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.45 compose (codomain $_1) (compose a h) = % 3.27/3.45 compose (compose (codomain $_1) a) h % 3.27/3.45 |- ~(codomain a = domain g) \/ ~(codomain b = codomain g) \/ % 3.27/3.45 compose (compose a b) (compose a h) = % 3.27/3.45 compose (compose (compose a b) a) h % 3.27/3.45 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.45 compose (compose g a) (compose a h) = % 3.27/3.45 compose (compose (compose g a) a) h % 3.27/3.45 |- ~(codomain a = domain g) \/ ~(codomain b = codomain g) \/ % 3.27/3.45 compose (compose g (compose a b)) (compose a h) = % 3.27/3.45 compose (compose (compose g (compose a b)) a) h % 3.27/3.45 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.45 compose (compose h a) (compose a h) = % 3.27/3.45 compose (compose (compose h a) a) h % 3.27/3.45 |- ~(codomain a = domain g) \/ % 3.27/3.45 compose (codomain g) (compose a h) = compose a h % 3.27/3.45 |- ~(codomain $_1 = codomain a) \/ ~(codomain a = domain g) \/ % 3.27/3.45 compose (codomain $_1) (compose (compose g a) h) = % 3.27/3.45 compose (compose (codomain $_1) (compose g a)) h % 3.27/3.45 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.45 compose (compose a b) (compose (compose g a) h) = % 3.27/3.45 compose (compose (compose a b) (compose g a)) h % 3.27/3.45 |- ~(codomain a = domain g) \/ % 3.27/3.45 compose (compose g a) (compose (compose g a) h) = % 3.27/3.45 compose (compose (compose g a) (compose g a)) h % 3.27/3.45 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.45 compose (compose g (compose a b)) (compose (compose g a) h) = % 3.27/3.45 compose (compose (compose g (compose a b)) (compose g a)) h % 3.27/3.45 |- ~(codomain a = domain g) \/ % 3.27/3.45 compose (compose h a) (compose (compose g a) h) = % 3.27/3.45 compose (compose (compose h a) (compose g a)) h % 3.27/3.45 |- ~(codomain a = domain g) \/ % 3.27/3.45 compose (codomain a) (compose (compose g a) h) = % 3.27/3.45 compose (compose (codomain a) (compose g a)) h % 3.27/3.45 |- ~(codomain $_1 = codomain a) \/ ~(codomain a = domain g) \/ % 3.27/3.45 compose (codomain $_1) (compose (compose h a) h) = % 3.27/3.45 compose (compose (codomain $_1) (compose h a)) h % 3.27/3.45 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.45 compose (compose a b) (compose (compose h a) h) = % 3.27/3.45 compose (compose (compose a b) (compose h a)) h % 3.27/3.45 |- ~(codomain a = domain g) \/ % 3.27/3.45 compose (compose g a) (compose (compose h a) h) = % 3.27/3.45 compose (compose (compose g a) (compose h a)) h % 3.27/3.45 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.45 compose (compose g (compose a b)) (compose (compose h a) h) = % 3.27/3.45 compose (compose (compose g (compose a b)) (compose h a)) h % 3.27/3.45 |- ~(codomain a = domain g) \/ % 3.27/3.45 compose (compose h a) (compose (compose h a) h) = % 3.27/3.45 compose (compose (compose h a) (compose h a)) h % 3.27/3.45 |- ~(codomain a = domain g) \/ % 3.27/3.45 compose (codomain a) (compose (compose h a) h) = % 3.27/3.45 compose (compose (codomain a) (compose h a)) h % 3.27/3.45 |- ~(codomain a = domain $_363) \/ % 3.27/3.45 compose h (compose a $_363) = compose (compose h a) $_363 % 3.27/3.45 |- ~(codomain b = domain $_363) \/ ~(codomain g = codomain a) \/ % 3.27/3.45 compose h (compose b $_363) = compose (compose h b) $_363 % 3.27/3.46 |- ~(codomain $X = domain $_363) \/ ~(codomain g = codomain $X) \/ % 3.27/3.46 compose h (compose (codomain $X) $_363) = % 3.27/3.46 compose (compose h (codomain $X)) $_363 % 3.27/3.46 |- ~(codomain b = domain $_363) \/ % 3.27/3.46 compose h (compose (compose a b) $_363) = % 3.27/3.46 compose (compose g (compose a b)) $_363 % 3.27/3.46 |- ~(codomain a = domain $_363) \/ ~(codomain g = domain g) \/ % 3.27/3.46 compose h (compose (compose g a) $_363) = % 3.27/3.46 compose (compose h (compose g a)) $_363 % 3.27/3.46 |- ~(codomain b = domain $_363) \/ ~(codomain g = domain g) \/ % 3.27/3.46 compose h (compose (compose g (compose a b)) $_363) = % 3.27/3.46 compose (compose h (compose g (compose a b))) $_363 % 3.27/3.46 |- ~(codomain a = domain $_363) \/ ~(codomain g = domain g) \/ % 3.27/3.46 compose h (compose (compose h a) $_363) = % 3.27/3.46 compose (compose h (compose h a)) $_363 % 3.27/3.46 |- ~(codomain $_362 = codomain $X) \/ ~(codomain g = domain $_362) \/ % 3.27/3.46 compose h (compose $_362 (codomain $X)) = % 3.27/3.46 compose (compose h $_362) (codomain $X) % 3.27/3.46 |- ~(codomain $_362 = codomain g) \/ ~(codomain g = domain $_362) \/ % 3.27/3.46 compose h (compose $_362 (compose a b)) = % 3.27/3.46 compose (compose h $_362) (compose a b) % 3.27/3.46 |- ~(codomain $_362 = domain g) \/ ~(codomain g = domain $_362) \/ % 3.27/3.46 compose h (compose $_362 (compose g a)) = % 3.27/3.46 compose (compose h $_362) (compose g a) % 3.27/3.46 |- ~(codomain $_362 = domain g) \/ ~(codomain g = domain $_362) \/ % 3.27/3.46 compose h (compose $_362 (compose g (compose a b))) = % 3.27/3.46 compose (compose h $_362) (compose g (compose a b)) % 3.27/3.46 |- ~(codomain $_362 = domain g) \/ ~(codomain g = domain $_362) \/ % 3.27/3.46 compose h (compose $_362 (compose h a)) = % 3.27/3.46 compose (compose h $_362) (compose h a) % 3.27/3.46 |- ~(codomain g = domain g) \/ % 3.27/3.46 compose h (compose g (compose g a)) = % 3.27/3.46 compose (compose h g) (compose g a) % 3.27/3.46 |- ~(codomain g = domain g) \/ % 3.27/3.46 compose h (compose g (compose g (compose a b))) = % 3.27/3.46 compose (compose h g) (compose g (compose a b)) % 3.27/3.46 |- ~(codomain g = domain g) \/ % 3.27/3.46 compose h (compose g (compose h a)) = % 3.27/3.46 compose (compose h g) (compose h a) % 3.27/3.46 |- ~(codomain a = codomain $X) \/ % 3.27/3.46 compose h (compose a (codomain $X)) = % 3.27/3.46 compose (compose h a) (codomain $X) % 3.27/3.46 |- ~(codomain a = codomain g) \/ % 3.27/3.46 compose h (compose a (compose a b)) = % 3.27/3.46 compose (compose h a) (compose a b) % 3.27/3.46 |- ~(codomain a = domain g) \/ % 3.27/3.46 compose h (compose a (compose g a)) = % 3.27/3.46 compose (compose h a) (compose g a) % 3.27/3.46 |- ~(codomain a = domain g) \/ % 3.27/3.46 compose h (compose a (compose g (compose a b))) = % 3.27/3.46 compose (compose h a) (compose g (compose a b)) % 3.27/3.46 |- ~(codomain a = domain g) \/ % 3.27/3.46 compose h (compose a (compose h a)) = % 3.27/3.46 compose (compose h a) (compose h a) % 3.27/3.46 |- ~(codomain a = domain g) \/ % 3.27/3.46 compose h (compose a h) = compose (compose h a) h % 3.27/3.46 |- ~(codomain b = codomain $X) \/ % 3.27/3.46 compose h (compose (compose a b) (codomain $X)) = % 3.27/3.46 compose (compose g (compose a b)) (codomain $X) % 3.27/3.46 |- ~(codomain b = codomain g) \/ % 3.27/3.46 compose h (compose (compose a b) (compose a b)) = % 3.27/3.46 compose (compose g (compose a b)) (compose a b) % 3.27/3.46 |- ~(codomain b = domain g) \/ % 3.27/3.46 compose h (compose (compose a b) (compose g a)) = % 3.27/3.46 compose (compose g (compose a b)) (compose g a) % 3.27/3.46 |- ~(codomain b = domain g) \/ % 3.27/3.46 compose h (compose (compose a b) (compose g (compose a b))) = % 3.27/3.46 compose (compose g (compose a b)) (compose g (compose a b)) % 3.27/3.46 |- ~(codomain b = domain g) \/ % 3.27/3.46 compose h (compose (compose a b) (compose h a)) = % 3.27/3.46 compose (compose g (compose a b)) (compose h a) % 3.27/3.46 |- ~(codomain b = codomain $X) \/ ~(codomain g = codomain a) \/ % 3.27/3.46 compose h (compose b (codomain $X)) = % 3.27/3.46 compose (compose h b) (codomain $X) % 3.27/3.46 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.46 compose h (compose b (compose a b)) = % 3.27/3.46 compose (compose h b) (compose a b) % 3.27/3.46 |- ~(codomain b = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.46 compose h (compose b (compose g a)) = % 3.27/3.46 compose (compose h b) (compose g a) % 3.27/3.46 |- ~(codomain b = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.46 compose h (compose b (compose g (compose a b))) = % 3.27/3.46 compose (compose h b) (compose g (compose a b)) % 3.27/3.46 |- ~(codomain b = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.46 compose h (compose b (compose h a)) = % 3.27/3.46 compose (compose h b) (compose h a) % 3.27/3.46 |- ~(codomain b = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.46 compose h (compose b h) = compose (compose h b) h % 3.27/3.46 |- ~(codomain a = codomain $X) \/ ~(codomain g = domain g) \/ % 3.27/3.46 compose h (compose (compose g a) (codomain $X)) = % 3.27/3.46 compose (compose h (compose g a)) (codomain $X) % 3.27/3.46 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.46 compose h (compose (compose g a) (compose a b)) = % 3.27/3.46 compose (compose h (compose g a)) (compose a b) % 3.27/3.46 |- ~(codomain a = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.46 compose h (compose (compose g a) (compose g a)) = % 3.27/3.46 compose (compose h (compose g a)) (compose g a) % 3.27/3.46 |- ~(codomain a = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.46 compose h (compose (compose g a) (compose g (compose a b))) = % 3.27/3.46 compose (compose h (compose g a)) (compose g (compose a b)) % 3.27/3.46 |- ~(codomain a = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.46 compose h (compose (compose g a) (compose h a)) = % 3.27/3.46 compose (compose h (compose g a)) (compose h a) % 3.27/3.46 |- ~(codomain a = codomain $X) \/ ~(codomain g = domain g) \/ % 3.27/3.46 compose h (compose (compose h a) (codomain $X)) = % 3.27/3.46 compose (compose h (compose h a)) (codomain $X) % 3.27/3.46 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.46 compose h (compose (compose h a) (compose a b)) = % 3.27/3.46 compose (compose h (compose h a)) (compose a b) % 3.27/3.46 |- ~(codomain a = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.46 compose h (compose (compose h a) (compose g a)) = % 3.27/3.46 compose (compose h (compose h a)) (compose g a) % 3.27/3.46 |- ~(codomain a = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.46 compose h (compose (compose h a) (compose g (compose a b))) = % 3.27/3.46 compose (compose h (compose h a)) (compose g (compose a b)) % 3.27/3.46 |- ~(codomain a = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.46 compose h (compose (compose h a) (compose h a)) = % 3.27/3.46 compose (compose h (compose h a)) (compose h a) % 3.27/3.46 |- ~(codomain $X = domain g) \/ ~(codomain g = codomain $X) \/ % 3.27/3.46 compose h (compose (codomain $X) (compose g a)) = % 3.27/3.46 compose (compose h (codomain $X)) (compose g a) % 3.27/3.46 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.46 compose h (compose (compose g (compose a b)) (compose g a)) = % 3.27/3.46 compose (compose h (compose g (compose a b))) (compose g a) % 3.27/3.46 |- ~(codomain $X = domain g) \/ ~(codomain g = codomain $X) \/ % 3.27/3.46 compose h (compose (codomain $X) (compose h a)) = % 3.27/3.46 compose (compose h (codomain $X)) (compose h a) % 3.27/3.46 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.46 compose h (compose (compose g (compose a b)) (compose h a)) = % 3.27/3.46 compose (compose h (compose g (compose a b))) (compose h a) % 3.27/3.46 |- ~(codomain $_374 = codomain g) \/ ~(codomain a = codomain $X) \/ % 3.27/3.46 compose $_374 (compose a (codomain $X)) = % 3.27/3.46 compose (compose $_374 a) (codomain $X) % 3.27/3.46 |- ~(codomain $_374 = codomain a) \/ ~(codomain a = codomain g) \/ % 3.27/3.46 compose $_374 (compose a (compose a b)) = % 3.27/3.46 compose (compose $_374 a) (compose a b) % 3.27/3.46 |- ~(codomain $_374 = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.46 compose $_374 (compose a (compose g a)) = % 3.27/3.46 compose (compose $_374 a) (compose g a) % 3.27/3.46 |- ~(codomain $_374 = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.46 compose $_374 (compose a (compose g (compose a b))) = % 3.27/3.46 compose (compose $_374 a) (compose g (compose a b)) % 3.27/3.46 |- ~(codomain $_374 = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.46 compose $_374 (compose a (compose h a)) = % 3.27/3.46 compose (compose $_374 a) (compose h a) % 3.27/3.46 |- ~(codomain $_1 = codomain g) \/ ~(codomain a = domain $_375) \/ % 3.27/3.46 compose (codomain $_1) (compose a $_375) = % 3.27/3.46 compose (compose (codomain $_1) a) $_375 % 3.27/3.46 |- ~(codomain a = domain $_375) \/ ~(codomain b = codomain g) \/ % 3.27/3.46 compose (compose a b) (compose a $_375) = % 3.27/3.46 compose (compose (compose a b) a) $_375 % 3.27/3.46 |- ~(codomain a = codomain g) \/ ~(codomain a = domain $_375) \/ % 3.27/3.46 compose (compose g a) (compose a $_375) = % 3.27/3.46 compose (compose (compose g a) a) $_375 % 3.27/3.46 |- ~(codomain a = domain $_375) \/ ~(codomain b = codomain g) \/ % 3.27/3.46 compose (compose g (compose a b)) (compose a $_375) = % 3.27/3.46 compose (compose (compose g (compose a b)) a) $_375 % 3.27/3.46 |- ~(codomain a = codomain g) \/ ~(codomain a = domain $_375) \/ % 3.27/3.46 compose (compose h a) (compose a $_375) = % 3.27/3.46 compose (compose (compose h a) a) $_375 % 3.27/3.46 |- ~(codomain a = codomain g) \/ % 3.27/3.46 compose a (compose a (compose a b)) = % 3.27/3.46 compose (compose a a) (compose a b) % 3.27/3.46 |- ~(codomain a = domain $_375) \/ % 3.27/3.46 compose (codomain g) (compose a $_375) = compose a $_375 % 3.27/3.46 |- ~(codomain a = codomain $X) \/ % 3.27/3.46 compose (codomain g) (compose a (codomain $X)) = compose a (codomain $X) % 3.27/3.46 |- ~(codomain a = codomain g) \/ % 3.27/3.46 compose (codomain a) (compose a (compose a b)) = compose a (compose a b) % 3.27/3.46 |- ~(codomain a = domain g) \/ % 3.27/3.46 compose (codomain g) (compose a (compose g a)) = compose a (compose g a) % 3.27/3.46 |- ~(codomain a = domain g) \/ % 3.27/3.46 compose (codomain g) (compose a (compose g (compose a b))) = % 3.27/3.46 compose a (compose g (compose a b)) % 3.27/3.46 |- ~(codomain a = domain g) \/ % 3.27/3.46 compose (codomain g) (compose a (compose h a)) = compose a (compose h a) % 3.27/3.46 |- ~(codomain a = codomain g) \/ compose (codomain a) a = a % 3.27/3.46 |- ~(codomain $_1 = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.46 compose (codomain $_1) (compose a (compose g a)) = % 3.27/3.46 compose (compose (codomain $_1) a) (compose g a) % 3.27/3.46 |- ~(codomain a = domain g) \/ ~(codomain b = codomain g) \/ % 3.27/3.46 compose (compose a b) (compose a (compose g a)) = % 3.27/3.46 compose (compose (compose a b) a) (compose g a) % 3.27/3.46 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.46 compose (compose g a) (compose a (compose g a)) = % 3.27/3.46 compose (compose (compose g a) a) (compose g a) % 3.27/3.46 |- ~(codomain a = domain g) \/ ~(codomain b = codomain g) \/ % 3.27/3.46 compose (compose g (compose a b)) (compose a (compose g a)) = % 3.27/3.46 compose (compose (compose g (compose a b)) a) (compose g a) % 3.27/3.46 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.46 compose (compose h a) (compose a (compose g a)) = % 3.27/3.46 compose (compose (compose h a) a) (compose g a) % 3.27/3.46 |- ~(codomain $_1 = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.46 compose (codomain $_1) (compose a (compose h a)) = % 3.27/3.46 compose (compose (codomain $_1) a) (compose h a) % 3.27/3.46 |- ~(codomain a = domain g) \/ ~(codomain b = codomain g) \/ % 3.27/3.46 compose (compose a b) (compose a (compose h a)) = % 3.27/3.46 compose (compose (compose a b) a) (compose h a) % 3.27/3.46 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.46 compose (compose g a) (compose a (compose h a)) = % 3.27/3.46 compose (compose (compose g a) a) (compose h a) % 3.27/3.46 |- ~(codomain a = domain g) \/ ~(codomain b = codomain g) \/ % 3.27/3.46 compose (compose g (compose a b)) (compose a (compose h a)) = % 3.27/3.46 compose (compose (compose g (compose a b)) a) (compose h a) % 3.27/3.46 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.46 compose (compose h a) (compose a (compose h a)) = % 3.27/3.46 compose (compose (compose h a) a) (compose h a) % 3.27/3.46 |- ~(codomain $_380 = codomain a) \/ ~(codomain b = codomain $X) \/ % 3.27/3.46 compose $_380 (compose b (codomain $X)) = % 3.27/3.46 compose (compose $_380 b) (codomain $X) % 3.27/3.46 |- ~(codomain $_380 = codomain a) \/ ~(codomain b = codomain g) \/ % 3.27/3.46 compose $_380 (compose b (compose a b)) = % 3.27/3.46 compose (compose $_380 b) (compose a b) % 3.27/3.46 |- ~(codomain $_380 = codomain a) \/ ~(codomain b = domain g) \/ % 3.27/3.46 compose $_380 (compose b (compose g a)) = % 3.27/3.46 compose (compose $_380 b) (compose g a) % 3.27/3.46 |- ~(codomain $_380 = codomain a) \/ ~(codomain b = domain g) \/ % 3.27/3.46 compose $_380 (compose b (compose g (compose a b))) = % 3.27/3.46 compose (compose $_380 b) (compose g (compose a b)) % 3.27/3.46 |- ~(codomain $_380 = codomain a) \/ ~(codomain b = domain g) \/ % 3.27/3.46 compose $_380 (compose b (compose h a)) = % 3.27/3.46 compose (compose $_380 b) (compose h a) % 3.27/3.46 |- ~(codomain $_1 = codomain a) \/ ~(codomain b = domain $_381) \/ % 3.27/3.46 compose (codomain $_1) (compose b $_381) = % 3.27/3.46 compose (compose (codomain $_1) b) $_381 % 3.27/3.46 |- ~(codomain a = domain $_381) \/ ~(codomain b = codomain a) \/ % 3.27/3.46 compose (compose a b) (compose b $_381) = % 3.27/3.46 compose (compose (compose a b) b) $_381 % 3.27/3.47 |- ~(codomain b = domain $_381) \/ % 3.27/3.47 compose (compose g a) (compose b $_381) = % 3.27/3.47 compose (compose g (compose a b)) $_381 % 3.27/3.47 |- ~(codomain a = domain $_381) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose g (compose a b)) (compose b $_381) = % 3.27/3.47 compose (compose (compose g (compose a b)) b) $_381 % 3.27/3.47 |- ~(codomain b = domain $_381) \/ % 3.27/3.47 compose (compose h a) (compose b $_381) = % 3.27/3.47 compose (compose g (compose a b)) $_381 % 3.27/3.47 |- ~(codomain b = codomain a) \/ % 3.27/3.47 compose b (compose b (codomain a)) = compose (compose b b) (codomain a) % 3.27/3.47 |- ~(codomain b = domain $_381) \/ % 3.27/3.47 compose (codomain a) (compose b $_381) = compose b $_381 % 3.27/3.47 |- ~(codomain b = codomain $X) \/ % 3.27/3.47 compose (codomain a) (compose b (codomain $X)) = compose b (codomain $X) % 3.27/3.47 |- ~(codomain b = codomain g) \/ % 3.27/3.47 compose (codomain a) (compose b (compose a b)) = compose b (compose a b) % 3.27/3.47 |- ~(codomain b = domain g) \/ % 3.27/3.47 compose (codomain a) (compose b (compose g a)) = compose b (compose g a) % 3.27/3.47 |- ~(codomain b = domain g) \/ % 3.27/3.47 compose (codomain a) (compose b (compose g (compose a b))) = % 3.27/3.47 compose b (compose g (compose a b)) % 3.27/3.47 |- ~(codomain b = domain g) \/ % 3.27/3.47 compose (codomain a) (compose b (compose h a)) = compose b (compose h a) % 3.27/3.47 |- ~(codomain b = codomain $X) \/ % 3.27/3.47 compose (compose g a) (compose b (codomain $X)) = % 3.27/3.47 compose (compose g (compose a b)) (codomain $X) % 3.27/3.47 |- ~(codomain b = codomain g) \/ % 3.27/3.47 compose (compose g a) (compose b (compose a b)) = % 3.27/3.47 compose (compose g (compose a b)) (compose a b) % 3.27/3.47 |- ~(codomain b = domain g) \/ % 3.27/3.47 compose (compose g a) (compose b (compose g a)) = % 3.27/3.47 compose (compose g (compose a b)) (compose g a) % 3.27/3.47 |- ~(codomain b = domain g) \/ % 3.27/3.47 compose (compose g a) (compose b (compose g (compose a b))) = % 3.27/3.47 compose (compose g (compose a b)) (compose g (compose a b)) % 3.27/3.47 |- ~(codomain b = domain g) \/ % 3.27/3.47 compose (compose g a) (compose b (compose h a)) = % 3.27/3.47 compose (compose g (compose a b)) (compose h a) % 3.27/3.47 |- ~(codomain b = codomain $X) \/ % 3.27/3.47 compose (compose h a) (compose b (codomain $X)) = % 3.27/3.47 compose (compose g (compose a b)) (codomain $X) % 3.27/3.47 |- ~(codomain b = codomain g) \/ % 3.27/3.47 compose (compose h a) (compose b (compose a b)) = % 3.27/3.47 compose (compose g (compose a b)) (compose a b) % 3.27/3.47 |- ~(codomain b = domain g) \/ % 3.27/3.47 compose (compose h a) (compose b (compose g a)) = % 3.27/3.47 compose (compose g (compose a b)) (compose g a) % 3.27/3.47 |- ~(codomain b = domain g) \/ % 3.27/3.47 compose (compose h a) (compose b (compose g (compose a b))) = % 3.27/3.47 compose (compose g (compose a b)) (compose g (compose a b)) % 3.27/3.47 |- ~(codomain b = domain g) \/ % 3.27/3.47 compose (compose h a) (compose b (compose h a)) = % 3.27/3.47 compose (compose g (compose a b)) (compose h a) % 3.27/3.47 |- ~(codomain $_1 = codomain a) \/ ~(codomain b = domain g) \/ % 3.27/3.47 compose (codomain $_1) (compose b (compose g a)) = % 3.27/3.47 compose (compose (codomain $_1) b) (compose g a) % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose a b) (compose b (compose g a)) = % 3.27/3.47 compose (compose (compose a b) b) (compose g a) % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose g (compose a b)) (compose b (compose g a)) = % 3.27/3.47 compose (compose (compose g (compose a b)) b) (compose g a) % 3.27/3.47 |- ~(codomain $_1 = codomain a) \/ ~(codomain b = domain g) \/ % 3.27/3.47 compose (codomain $_1) (compose b (compose h a)) = % 3.27/3.47 compose (compose (codomain $_1) b) (compose h a) % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose a b) (compose b (compose h a)) = % 3.27/3.47 compose (compose (compose a b) b) (compose h a) % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose g (compose a b)) (compose b (compose h a)) = % 3.27/3.47 compose (compose (compose g (compose a b)) b) (compose h a) % 3.27/3.47 |- ~(codomain $_1 = codomain a) \/ ~(codomain b = codomain g) \/ % 3.27/3.47 compose (codomain $_1) (compose b (compose a b)) = % 3.27/3.47 compose (compose (codomain $_1) b) (compose a b) % 3.27/3.47 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose a b) (compose b (compose a b)) = % 3.27/3.47 compose (compose (compose a b) b) (compose a b) % 3.27/3.47 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose g (compose a b)) (compose b (compose a b)) = % 3.27/3.47 compose (compose (compose g (compose a b)) b) (compose a b) % 3.27/3.47 |- ~(codomain $X = domain g) \/ ~(codomain a = codomain $X) \/ % 3.27/3.47 compose (compose g a) (compose (codomain $X) h) = % 3.27/3.47 compose (compose (compose g a) (codomain $X)) h % 3.27/3.47 |- ~(codomain a = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.47 compose (compose g a) (compose (compose a b) h) = % 3.27/3.47 compose (compose (compose g a) (compose a b)) h % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose g a) (compose (compose g (compose a b)) h) = % 3.27/3.47 compose (compose (compose g a) (compose g (compose a b))) h % 3.27/3.47 |- ~(codomain $X = domain g) \/ ~(codomain a = codomain $X) \/ % 3.27/3.47 compose (compose h a) (compose (codomain $X) h) = % 3.27/3.47 compose (compose (compose h a) (codomain $X)) h % 3.27/3.47 |- ~(codomain a = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.47 compose (compose h a) (compose (compose a b) h) = % 3.27/3.47 compose (compose (compose h a) (compose a b)) h % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose h a) (compose (compose g (compose a b)) h) = % 3.27/3.47 compose (compose (compose h a) (compose g (compose a b))) h % 3.27/3.47 |- ~(codomain $_1 = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.47 compose (codomain $_1) (compose (compose a b) h) = % 3.27/3.47 compose (compose (codomain $_1) (compose a b)) h % 3.27/3.47 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.47 compose (compose a b) (compose (compose a b) h) = % 3.27/3.47 compose (compose (compose a b) (compose a b)) h % 3.27/3.47 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.47 compose (compose g (compose a b)) (compose (compose a b) h) = % 3.27/3.47 compose (compose (compose g (compose a b)) (compose a b)) h % 3.27/3.47 |- ~(codomain b = domain g) \/ ~(codomain g = codomain b) \/ % 3.27/3.47 compose h (compose h (codomain b)) = compose (compose h h) (codomain b) % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.47 compose h (compose h (codomain a)) = compose (compose h h) (codomain a) % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain g = codomain $X) \/ % 3.27/3.47 compose (compose g a) (compose h (codomain $X)) = % 3.27/3.47 compose (compose (compose g a) h) (codomain $X) % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.47 compose (compose g a) (compose h (compose g (compose a b))) = % 3.27/3.47 compose (compose (compose g a) h) (compose g (compose a b)) % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain g = codomain $X) \/ % 3.27/3.47 compose (compose h a) (compose h (codomain $X)) = % 3.27/3.47 compose (compose (compose h a) h) (codomain $X) % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain g = codomain a) \/ % 3.27/3.47 compose (compose h a) (compose h (compose g (compose a b))) = % 3.27/3.47 compose (compose (compose h a) h) (compose g (compose a b)) % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (codomain a) (compose b h) = compose b h % 3.27/3.47 |- ~(codomain $_1 = codomain a) \/ ~(codomain a = codomain g) \/ % 3.27/3.47 compose (codomain $_1) (compose a (compose a b)) = % 3.27/3.47 compose (compose (codomain $_1) a) (compose a b) % 3.27/3.47 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose a b) (compose a (compose a b)) = % 3.27/3.47 compose (compose (compose a b) a) (compose a b) % 3.27/3.47 |- ~(codomain a = codomain g) \/ % 3.27/3.47 compose (compose g a) (compose a (compose a b)) = % 3.27/3.47 compose (compose (compose g a) a) (compose a b) % 3.27/3.47 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose g (compose a b)) (compose a (compose a b)) = % 3.27/3.47 compose (compose (compose g (compose a b)) a) (compose a b) % 3.27/3.47 |- ~(codomain a = codomain g) \/ % 3.27/3.47 compose (compose h a) (compose a (compose a b)) = % 3.27/3.47 compose (compose (compose h a) a) (compose a b) % 3.27/3.47 |- ~(codomain a = codomain g) \/ % 3.27/3.47 compose (codomain a) (compose a (compose a b)) = % 3.27/3.47 compose (compose (codomain a) a) (compose a b) % 3.27/3.47 |- ~(codomain a = codomain $X) \/ ~(codomain a = codomain g) \/ % 3.27/3.47 compose (compose g a) (compose a (codomain $X)) = % 3.27/3.47 compose (compose (compose g a) a) (codomain $X) % 3.27/3.47 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.47 compose (compose g a) (compose a (compose g (compose a b))) = % 3.27/3.47 compose (compose (compose g a) a) (compose g (compose a b)) % 3.27/3.47 |- ~(codomain a = codomain $X) \/ ~(codomain a = codomain g) \/ % 3.27/3.47 compose (compose h a) (compose a (codomain $X)) = % 3.27/3.47 compose (compose (compose h a) a) (codomain $X) % 3.27/3.47 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.47 compose (compose h a) (compose a (compose g (compose a b))) = % 3.27/3.47 compose (compose (compose h a) a) (compose g (compose a b)) % 3.27/3.47 |- ~(codomain a = codomain $X) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose a b) (compose b (codomain $X)) = % 3.27/3.47 compose (compose (compose a b) b) (codomain $X) % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose a b) (compose b (compose g (compose a b))) = % 3.27/3.47 compose (compose (compose a b) b) (compose g (compose a b)) % 3.27/3.47 |- ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose a b) (compose b (codomain a)) = % 3.27/3.47 compose (compose (compose a b) b) (codomain a) % 3.27/3.47 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.47 compose (codomain b) (compose h h) = compose (compose (codomain b) h) h % 3.27/3.47 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.47 compose (codomain a) (compose h h) = compose (compose (codomain a) h) h % 3.27/3.47 |- ~(codomain $_1 = codomain a) \/ ~(codomain b = domain g) \/ % 3.27/3.47 compose (codomain $_1) (compose b (compose g (compose a b))) = % 3.27/3.47 compose (compose (codomain $_1) b) (compose g (compose a b)) % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose g (compose a b)) % 3.27/3.47 (compose b (compose g (compose a b))) = % 3.27/3.47 compose (compose (compose g (compose a b)) b) (compose g (compose a b)) % 3.27/3.47 |- ~(codomain $X = codomain g) \/ % 3.27/3.47 compose h (compose (codomain $X) (compose a b)) = % 3.27/3.47 compose (compose h (codomain $X)) (compose a b) % 3.27/3.47 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.47 compose h (compose (compose g (compose a b)) (compose a b)) = % 3.27/3.47 compose (compose h (compose g (compose a b))) (compose a b) % 3.27/3.47 |- ~(codomain $X = codomain a) \/ ~(codomain b = codomain $X) \/ % 3.27/3.47 compose (compose a b) (compose (codomain $X) b) = % 3.27/3.47 compose (compose (compose a b) (codomain $X)) b % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose a b) (compose (compose g (compose a b)) b) = % 3.27/3.47 compose (compose (compose a b) (compose g (compose a b))) b % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (codomain a) (compose b (compose g a)) = compose b (compose g a) % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (codomain a) (compose b (compose h a)) = compose b (compose h a) % 3.27/3.47 |- ~(codomain $_1 = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (codomain $_1) (compose (compose g (compose a b)) b) = % 3.27/3.47 compose (compose (codomain $_1) (compose g (compose a b))) b % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose g (compose a b)) % 3.27/3.47 (compose (compose g (compose a b)) b) = % 3.27/3.47 compose (compose (compose g (compose a b)) (compose g (compose a b))) b % 3.27/3.47 |- ~(codomain b = codomain a) \/ ~(domain $X = domain g) \/ % 3.27/3.47 compose (domain $X) (compose (compose g (compose a b)) b) = % 3.27/3.47 compose (compose (domain $X) (compose g (compose a b))) b % 3.27/3.47 |- ~(codomain $X = codomain g) \/ ~(codomain a = codomain $X) \/ % 3.27/3.47 compose (compose g a) (compose (codomain $X) a) = % 3.27/3.47 compose (compose (compose g a) (codomain $X)) a % 3.27/3.47 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose g a) (compose (compose a b) a) = % 3.27/3.47 compose (compose (compose g a) (compose a b)) a % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain b = codomain g) \/ % 3.27/3.47 compose (compose g a) (compose (compose g (compose a b)) a) = % 3.27/3.47 compose (compose (compose g a) (compose g (compose a b))) a % 3.27/3.47 |- ~(codomain $X = codomain g) \/ ~(codomain a = codomain $X) \/ % 3.27/3.47 compose (compose h a) (compose (codomain $X) a) = % 3.27/3.47 compose (compose (compose h a) (codomain $X)) a % 3.27/3.47 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.47 compose (compose h a) (compose (compose a b) a) = % 3.27/3.47 compose (compose (compose h a) (compose a b)) a % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain b = codomain g) \/ % 3.27/3.47 compose (compose h a) (compose (compose g (compose a b)) a) = % 3.27/3.47 compose (compose (compose h a) (compose g (compose a b))) a % 3.27/3.47 |- ~(codomain $_1 = codomain b) \/ ~(codomain b = codomain g) \/ % 3.27/3.47 compose (codomain $_1) (compose (compose a b) a) = % 3.27/3.47 compose (compose (codomain $_1) (compose a b)) a % 3.27/3.47 |- ~(codomain b = codomain g) \/ % 3.27/3.47 compose (compose a b) (compose (compose a b) a) = % 3.27/3.47 compose (compose (compose a b) (compose a b)) a % 3.27/3.47 |- ~(codomain b = codomain g) \/ % 3.27/3.47 compose (compose g (compose a b)) (compose (compose a b) a) = % 3.27/3.47 compose (compose (compose g (compose a b)) (compose a b)) a % 3.27/3.47 |- ~(codomain b = codomain g) \/ % 3.27/3.47 compose (codomain b) (compose (compose a b) a) = % 3.27/3.47 compose (compose (codomain b) (compose a b)) a % 3.27/3.47 |- ~(codomain $X = domain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.47 compose (compose a b) (compose (codomain $X) h) = % 3.27/3.47 compose (compose (compose a b) (codomain $X)) h % 3.27/3.47 |- ~(codomain b = domain g) \/ % 3.27/3.47 compose (compose a b) (compose (compose g (compose a b)) h) = % 3.27/3.47 compose (compose (compose a b) (compose g (compose a b))) h % 3.27/3.47 |- ~(codomain $_1 = codomain b) \/ ~(codomain b = domain g) \/ % 3.27/3.47 compose (codomain $_1) (compose (compose g (compose a b)) h) = % 3.27/3.47 compose (compose (codomain $_1) (compose g (compose a b))) h % 3.27/3.47 |- ~(codomain b = domain g) \/ % 3.27/3.47 compose (compose g (compose a b)) % 3.27/3.47 (compose (compose g (compose a b)) h) = % 3.27/3.47 compose (compose (compose g (compose a b)) (compose g (compose a b))) h % 3.27/3.47 |- ~(codomain b = domain g) \/ % 3.27/3.47 compose (codomain b) (compose (compose g (compose a b)) h) = % 3.27/3.47 compose (compose (codomain b) (compose g (compose a b))) h % 3.27/3.47 |- ~(codomain b = domain g) \/ ~(codomain g = codomain $X) \/ % 3.27/3.47 compose (compose a b) (compose h (codomain $X)) = % 3.27/3.47 compose (compose (compose a b) h) (codomain $X) % 3.27/3.47 |- ~(codomain b = domain g) \/ ~(codomain g = codomain b) \/ % 3.27/3.47 compose (compose a b) (compose h (compose g (compose a b))) = % 3.27/3.47 compose (compose (compose a b) h) (compose g (compose a b)) % 3.27/3.47 |- ~(codomain a = codomain $X) \/ ~(codomain b = codomain g) \/ % 3.27/3.47 compose (compose a b) (compose a (codomain $X)) = % 3.27/3.47 compose (compose (compose a b) a) (codomain $X) % 3.27/3.47 |- ~(codomain a = domain g) \/ ~(codomain b = codomain g) \/ % 3.27/3.47 compose (compose a b) (compose a (compose g (compose a b))) = % 3.27/3.47 compose (compose (compose a b) a) (compose g (compose a b)) % 3.27/3.47 |- ~(codomain $_1 = codomain g) \/ ~(codomain g = domain g) \/ % 3.27/3.47 compose (codomain $_1) (compose h (compose g (compose a b))) = % 3.27/3.47 compose (compose (codomain $_1) h) (compose g (compose a b)) % 3.27/3.47 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.47 compose (compose g (compose a b)) % 3.27/3.47 (compose h (compose g (compose a b))) = % 3.27/3.47 compose (compose (compose g (compose a b)) h) (compose g (compose a b)) % 3.27/3.47 |- ~(codomain g = domain g) \/ % 3.27/3.47 compose (codomain g) (compose h (compose g (compose a b))) = % 3.27/3.47 compose (compose (codomain g) h) (compose g (compose a b)) % 3.27/3.48 |- ~(codomain $_1 = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.48 compose (codomain $_1) (compose a (compose g (compose a b))) = % 3.27/3.48 compose (compose (codomain $_1) a) (compose g (compose a b)) % 3.27/3.48 |- ~(codomain a = domain g) \/ ~(codomain b = codomain g) \/ % 3.27/3.48 compose (compose g (compose a b)) % 3.27/3.48 (compose a (compose g (compose a b))) = % 3.27/3.48 compose (compose (compose g (compose a b)) a) (compose g (compose a b)) % 3.27/3.48 |- ~(codomain a = codomain $X) \/ ~(codomain b = codomain a) \/ % 3.27/3.48 compose (compose g (compose a b)) (compose b (codomain $X)) = % 3.27/3.48 compose (compose (compose g (compose a b)) b) (codomain $X) % 3.27/3.48 |- ~(codomain b = codomain a) \/ % 3.27/3.48 compose (compose g (compose a b)) (compose b (codomain a)) = % 3.27/3.48 compose (compose (compose g (compose a b)) b) (codomain a) % 3.27/3.48 |- ~(codomain b = codomain $X) \/ ~(codomain g = domain g) \/ % 3.27/3.48 compose h (compose (compose g (compose a b)) (codomain $X)) = % 3.27/3.48 compose (compose h (compose g (compose a b))) (codomain $X) % 3.27/3.48 |- ~(codomain b = domain g) \/ ~(codomain g = codomain b) \/ % 3.27/3.48 compose h % 3.27/3.48 (compose (compose g (compose a b)) (compose g (compose a b))) = % 3.27/3.48 compose (compose h (compose g (compose a b))) (compose g (compose a b)) % 3.27/3.48 |- ~(codomain $X = domain g) \/ ~(codomain g = codomain $X) \/ % 3.27/3.48 compose h (compose (codomain $X) (compose g (compose a b))) = % 3.27/3.48 compose (compose h (codomain $X)) (compose g (compose a b)) % 3.27/3.48 |- ~(codomain $X = codomain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.48 compose (compose a b) (compose (codomain $X) a) = % 3.27/3.48 compose (compose (compose a b) (codomain $X)) a % 3.27/3.48 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose (compose a b) (compose (compose g (compose a b)) a) = % 3.27/3.48 compose (compose (compose a b) (compose g (compose a b))) a % 3.27/3.48 |- ~(codomain $X = codomain a) \/ ~(codomain b = codomain $X) \/ % 3.27/3.48 compose (compose g (compose a b)) (compose (codomain $X) b) = % 3.27/3.48 compose (compose (compose g (compose a b)) (codomain $X)) b % 3.27/3.48 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose (compose g (compose a b)) % 3.27/3.48 (compose (compose g (compose a b)) a) = % 3.27/3.48 compose (compose (compose g (compose a b)) (compose g (compose a b))) a % 3.27/3.48 |- ~(codomain $X = domain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.48 compose (compose g (compose a b)) (compose (codomain $X) h) = % 3.27/3.48 compose (compose (compose g (compose a b)) (codomain $X)) h % 3.27/3.48 |- ~(codomain b = domain g) \/ ~(codomain g = codomain $X) \/ % 3.27/3.48 compose (compose g (compose a b)) (compose h (codomain $X)) = % 3.27/3.48 compose (compose (compose g (compose a b)) h) (codomain $X) % 3.27/3.48 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.48 compose (codomain a) (compose b (compose g (compose a b))) = % 3.27/3.48 compose b (compose g (compose a b)) % 3.27/3.48 |- ~(codomain a = codomain $X) \/ ~(codomain b = codomain g) \/ % 3.27/3.48 compose (compose g (compose a b)) (compose a (codomain $X)) = % 3.27/3.48 compose (compose (compose g (compose a b)) a) (codomain $X) % 3.27/3.48 |- ~(codomain $_447 = codomain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.48 compose $_447 (compose (compose a b) (codomain $X)) = % 3.27/3.48 compose (compose $_447 (compose a b)) (codomain $X) % 3.27/3.48 |- ~(codomain $_447 = codomain b) \/ ~(codomain b = codomain g) \/ % 3.27/3.48 compose $_447 (compose (compose a b) (compose a b)) = % 3.27/3.48 compose (compose $_447 (compose a b)) (compose a b) % 3.27/3.48 |- ~(codomain $_447 = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose $_447 (compose (compose a b) (compose g a)) = % 3.27/3.48 compose (compose $_447 (compose a b)) (compose g a) % 3.27/3.48 |- ~(codomain $_447 = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose $_447 (compose (compose a b) (compose g (compose a b))) = % 3.27/3.48 compose (compose $_447 (compose a b)) (compose g (compose a b)) % 3.27/3.48 |- ~(codomain $_447 = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose $_447 (compose (compose a b) (compose h a)) = % 3.27/3.48 compose (compose $_447 (compose a b)) (compose h a) % 3.27/3.48 |- ~(codomain $_1 = codomain g) \/ ~(codomain b = domain $_448) \/ % 3.27/3.48 compose (codomain $_1) (compose (compose a b) $_448) = % 3.27/3.48 compose (compose (codomain $_1) (compose a b)) $_448 % 3.27/3.48 |- ~(codomain a = codomain g) \/ ~(codomain b = domain $_448) \/ % 3.27/3.48 compose (compose g a) (compose (compose a b) $_448) = % 3.27/3.48 compose (compose (compose g a) (compose a b)) $_448 % 3.27/3.48 |- ~(codomain b = codomain g) \/ ~(codomain b = domain $_448) \/ % 3.27/3.48 compose (compose g (compose a b)) (compose (compose a b) $_448) = % 3.27/3.48 compose (compose (compose g (compose a b)) (compose a b)) $_448 % 3.27/3.48 |- ~(codomain a = codomain g) \/ ~(codomain b = domain $_448) \/ % 3.27/3.48 compose (compose h a) (compose (compose a b) $_448) = % 3.27/3.48 compose (compose (compose h a) (compose a b)) $_448 % 3.27/3.48 |- ~(codomain b = codomain g) \/ % 3.27/3.48 compose b (compose (compose a b) (compose a b)) = % 3.27/3.48 compose (compose b (compose a b)) (compose a b) % 3.27/3.48 |- ~(codomain $_1 = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose (codomain $_1) (compose (compose a b) (compose g a)) = % 3.27/3.48 compose (compose (codomain $_1) (compose a b)) (compose g a) % 3.27/3.48 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose (compose a b) (compose (compose a b) (compose g a)) = % 3.27/3.48 compose (compose (compose a b) (compose a b)) (compose g a) % 3.27/3.48 |- ~(codomain a = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose (compose g a) (compose (compose a b) (compose g a)) = % 3.27/3.48 compose (compose (compose g a) (compose a b)) (compose g a) % 3.27/3.48 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose (compose g (compose a b)) % 3.27/3.48 (compose (compose a b) (compose g a)) = % 3.27/3.48 compose (compose (compose g (compose a b)) (compose a b)) (compose g a) % 3.27/3.48 |- ~(codomain a = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose (compose h a) (compose (compose a b) (compose g a)) = % 3.27/3.48 compose (compose (compose h a) (compose a b)) (compose g a) % 3.27/3.48 |- ~(codomain $_1 = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose (codomain $_1) (compose (compose a b) (compose h a)) = % 3.27/3.48 compose (compose (codomain $_1) (compose a b)) (compose h a) % 3.27/3.48 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose (compose a b) (compose (compose a b) (compose h a)) = % 3.27/3.48 compose (compose (compose a b) (compose a b)) (compose h a) % 3.27/3.48 |- ~(codomain a = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose (compose g a) (compose (compose a b) (compose h a)) = % 3.27/3.48 compose (compose (compose g a) (compose a b)) (compose h a) % 3.27/3.48 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose (compose g (compose a b)) % 3.27/3.48 (compose (compose a b) (compose h a)) = % 3.27/3.48 compose (compose (compose g (compose a b)) (compose a b)) (compose h a) % 3.27/3.48 |- ~(codomain a = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose (compose h a) (compose (compose a b) (compose h a)) = % 3.27/3.48 compose (compose (compose h a) (compose a b)) (compose h a) % 3.27/3.48 |- ~(codomain $_1 = codomain b) \/ ~(codomain b = codomain g) \/ % 3.27/3.48 compose (codomain $_1) (compose (compose a b) (compose a b)) = % 3.27/3.48 compose (compose (codomain $_1) (compose a b)) (compose a b) % 3.27/3.48 |- ~(codomain a = codomain b) \/ ~(codomain a = codomain g) \/ % 3.27/3.48 compose (compose g a) (compose (compose a b) (compose a b)) = % 3.27/3.48 compose (compose (compose g a) (compose a b)) (compose a b) % 3.27/3.48 |- ~(codomain b = codomain g) \/ % 3.27/3.48 compose (compose g (compose a b)) % 3.27/3.48 (compose (compose a b) (compose a b)) = % 3.27/3.48 compose (compose (compose g (compose a b)) (compose a b)) (compose a b) % 3.27/3.48 |- ~(codomain a = codomain b) \/ ~(codomain a = codomain g) \/ % 3.27/3.48 compose (compose h a) (compose (compose a b) (compose a b)) = % 3.27/3.48 compose (compose (compose h a) (compose a b)) (compose a b) % 3.27/3.48 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.48 compose (compose g a) (compose (compose a b) (codomain $X)) = % 3.27/3.48 compose (compose (compose g a) (compose a b)) (codomain $X) % 3.27/3.48 |- ~(codomain a = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose (compose g a) % 3.27/3.48 (compose (compose a b) (compose g (compose a b))) = % 3.27/3.48 compose (compose (compose g a) (compose a b)) (compose g (compose a b)) % 3.27/3.48 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.48 compose (compose h a) (compose (compose a b) (codomain $X)) = % 3.27/3.48 compose (compose (compose h a) (compose a b)) (codomain $X) % 3.27/3.48 |- ~(codomain a = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose (compose h a) % 3.27/3.48 (compose (compose a b) (compose g (compose a b))) = % 3.27/3.48 compose (compose (compose h a) (compose a b)) (compose g (compose a b)) % 3.27/3.48 |- ~(codomain $_454 = domain g) \/ ~(codomain a = codomain $X) \/ % 3.27/3.48 compose $_454 (compose (compose g a) (codomain $X)) = % 3.27/3.48 compose (compose $_454 (compose g a)) (codomain $X) % 3.27/3.48 |- ~(codomain $_454 = domain g) \/ ~(codomain a = codomain g) \/ % 3.27/3.48 compose $_454 (compose (compose g a) (compose a b)) = % 3.27/3.48 compose (compose $_454 (compose g a)) (compose a b) % 3.27/3.48 |- ~(codomain $_454 = codomain a) \/ ~(codomain a = domain g) \/ % 3.27/3.48 compose $_454 (compose (compose g a) (compose g a)) = % 3.27/3.48 compose (compose $_454 (compose g a)) (compose g a) % 3.27/3.48 |- ~(codomain $_454 = codomain a) \/ ~(codomain a = domain g) \/ % 3.27/3.48 compose $_454 (compose (compose g a) (compose g (compose a b))) = % 3.27/3.48 compose (compose $_454 (compose g a)) (compose g (compose a b)) % 3.27/3.48 |- ~(codomain $_454 = codomain a) \/ ~(codomain a = domain g) \/ % 3.27/3.48 compose $_454 (compose (compose g a) (compose h a)) = % 3.27/3.48 compose (compose $_454 (compose g a)) (compose h a) % 3.27/3.48 |- ~(codomain $_1 = domain g) \/ ~(codomain a = domain $_455) \/ % 3.27/3.48 compose (codomain $_1) (compose (compose g a) $_455) = % 3.27/3.48 compose (compose (codomain $_1) (compose g a)) $_455 % 3.27/3.48 |- ~(codomain a = domain $_455) \/ ~(codomain a = domain g) \/ % 3.27/3.48 compose (compose g a) (compose (compose g a) $_455) = % 3.27/3.48 compose (compose (compose g a) (compose g a)) $_455 % 3.27/3.48 |- ~(codomain a = domain $_455) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose (compose g (compose a b)) (compose (compose g a) $_455) = % 3.27/3.48 compose (compose (compose g (compose a b)) (compose g a)) $_455 % 3.27/3.48 |- ~(codomain a = domain $_455) \/ ~(codomain a = domain g) \/ % 3.27/3.48 compose (compose h a) (compose (compose g a) $_455) = % 3.27/3.48 compose (compose (compose h a) (compose g a)) $_455 % 3.27/3.48 |- ~(codomain a = domain g) \/ % 3.27/3.48 compose a (compose (compose g a) (compose g a)) = % 3.27/3.48 compose (compose a (compose g a)) (compose g a) % 3.27/3.48 |- ~(codomain a = domain g) \/ % 3.27/3.48 compose a (compose (compose g a) (compose g (compose a b))) = % 3.27/3.48 compose (compose a (compose g a)) (compose g (compose a b)) % 3.27/3.48 |- ~(codomain a = domain g) \/ % 3.27/3.48 compose a (compose (compose g a) (compose h a)) = % 3.27/3.48 compose (compose a (compose g a)) (compose h a) % 3.27/3.48 |- ~(codomain a = domain g) \/ % 3.27/3.48 compose (codomain a) (compose (compose g a) g) = % 3.27/3.48 compose (compose (codomain a) (compose g a)) g % 3.27/3.48 |- ~(codomain a = domain g) \/ % 3.27/3.48 compose (compose g a) (compose (compose g a) g) = % 3.27/3.48 compose (compose (compose g a) (compose g a)) g % 3.27/3.48 |- ~(codomain a = domain g) \/ % 3.27/3.48 compose (compose h a) (compose (compose g a) g) = % 3.27/3.48 compose (compose (compose h a) (compose g a)) g % 3.27/3.48 |- ~(codomain $_1 = codomain a) \/ ~(codomain a = domain g) \/ % 3.27/3.48 compose (codomain $_1) (compose (compose g a) (compose g a)) = % 3.27/3.48 compose (compose (codomain $_1) (compose g a)) (compose g a) % 3.27/3.48 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.48 compose (compose a b) (compose (compose g a) (compose g a)) = % 3.27/3.48 compose (compose (compose a b) (compose g a)) (compose g a) % 3.27/3.48 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.48 compose (compose g (compose a b)) % 3.27/3.48 (compose (compose g a) (compose g a)) = % 3.27/3.48 compose (compose (compose g (compose a b)) (compose g a)) (compose g a) % 3.27/3.48 |- ~(codomain a = domain g) \/ % 3.27/3.48 compose (compose h a) (compose (compose g a) (compose g a)) = % 3.27/3.48 compose (compose (compose h a) (compose g a)) (compose g a) % 3.27/3.48 |- ~(codomain $_1 = codomain a) \/ ~(codomain a = domain g) \/ % 3.27/3.48 compose (codomain $_1) (compose (compose g a) (compose h a)) = % 3.27/3.48 compose (compose (codomain $_1) (compose g a)) (compose h a) % 3.27/3.48 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.48 compose (compose a b) (compose (compose g a) (compose h a)) = % 3.27/3.48 compose (compose (compose a b) (compose g a)) (compose h a) % 3.27/3.48 |- ~(codomain a = domain g) \/ % 3.27/3.48 compose (compose g a) (compose (compose g a) (compose h a)) = % 3.27/3.48 compose (compose (compose g a) (compose g a)) (compose h a) % 3.27/3.48 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.48 compose (compose g (compose a b)) % 3.27/3.48 (compose (compose g a) (compose h a)) = % 3.27/3.48 compose (compose (compose g (compose a b)) (compose g a)) (compose h a) % 3.27/3.48 |- ~(codomain a = domain g) \/ % 3.27/3.48 compose (compose h a) (compose (compose g a) (compose h a)) = % 3.27/3.48 compose (compose (compose h a) (compose g a)) (compose h a) % 3.27/3.48 |- ~(codomain a = domain g) \/ % 3.27/3.48 compose (codomain a) (compose (compose g a) (compose h a)) = % 3.27/3.48 compose (compose (codomain a) (compose g a)) (compose h a) % 3.27/3.48 |- ~(codomain $_1 = domain g) \/ ~(codomain a = codomain g) \/ % 3.27/3.48 compose (codomain $_1) (compose (compose g a) (compose a b)) = % 3.27/3.48 compose (compose (codomain $_1) (compose g a)) (compose a b) % 3.27/3.48 |- ~(codomain a = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose (compose a b) (compose (compose g a) (compose a b)) = % 3.27/3.48 compose (compose (compose a b) (compose g a)) (compose a b) % 3.27/3.48 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.48 compose (compose g a) (compose (compose g a) (compose a b)) = % 3.27/3.48 compose (compose (compose g a) (compose g a)) (compose a b) % 3.27/3.48 |- ~(codomain a = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.48 compose (compose g (compose a b)) % 3.27/3.48 (compose (compose g a) (compose a b)) = % 3.27/3.48 compose (compose (compose g (compose a b)) (compose g a)) (compose a b) % 3.27/3.48 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.48 compose (compose h a) (compose (compose g a) (compose a b)) = % 3.27/3.48 compose (compose (compose h a) (compose g a)) (compose a b) % 3.27/3.48 |- ~(codomain a = codomain g) \/ ~(domain $X = domain g) \/ % 3.27/3.48 compose (domain $X) (compose (compose g a) (compose a b)) = % 3.27/3.48 compose (compose (domain $X) (compose g a)) (compose a b) % 3.27/3.48 |- ~(codomain a = codomain $X) \/ ~(codomain a = domain g) \/ % 3.27/3.48 compose (compose g a) (compose (compose g a) (codomain $X)) = % 3.27/3.48 compose (compose (compose g a) (compose g a)) (codomain $X) % 3.27/3.48 |- ~(codomain a = domain g) \/ % 3.27/3.48 compose (compose g a) % 3.27/3.48 (compose (compose g a) (compose g (compose a b))) = % 3.27/3.48 compose (compose (compose g a) (compose g a)) (compose g (compose a b)) % 3.27/3.48 |- ~(codomain a = codomain $X) \/ ~(codomain a = domain g) \/ % 3.27/3.48 compose (compose h a) (compose (compose g a) (codomain $X)) = % 3.27/3.48 compose (compose (compose h a) (compose g a)) (codomain $X) % 3.27/3.48 |- ~(codomain a = domain g) \/ % 3.27/3.48 compose (compose h a) % 3.27/3.48 (compose (compose g a) (compose g (compose a b))) = % 3.27/3.48 compose (compose (compose h a) (compose g a)) (compose g (compose a b)) % 3.27/3.48 |- ~(codomain $_461 = domain g) \/ ~(codomain a = codomain $X) \/ % 3.27/3.48 compose $_461 (compose (compose h a) (codomain $X)) = % 3.27/3.48 compose (compose $_461 (compose h a)) (codomain $X) % 3.27/3.48 |- ~(codomain $_461 = domain g) \/ ~(codomain a = codomain g) \/ % 3.27/3.48 compose $_461 (compose (compose h a) (compose a b)) = % 3.27/3.48 compose (compose $_461 (compose h a)) (compose a b) % 3.27/3.48 |- ~(codomain $_461 = codomain a) \/ ~(codomain a = domain g) \/ % 3.27/3.48 compose $_461 (compose (compose h a) (compose g a)) = % 3.27/3.48 compose (compose $_461 (compose h a)) (compose g a) % 3.27/3.48 |- ~(codomain $_461 = codomain a) \/ ~(codomain a = domain g) \/ % 3.27/3.48 compose $_461 (compose (compose h a) (compose g (compose a b))) = % 3.27/3.48 compose (compose $_461 (compose h a)) (compose g (compose a b)) % 3.27/3.48 |- ~(codomain $_461 = codomain a) \/ ~(codomain a = domain g) \/ % 3.27/3.48 compose $_461 (compose (compose h a) (compose h a)) = % 3.27/3.48 compose (compose $_461 (compose h a)) (compose h a) % 3.27/3.49 |- ~(codomain $_1 = domain g) \/ ~(codomain a = domain $_462) \/ % 3.27/3.49 compose (codomain $_1) (compose (compose h a) $_462) = % 3.27/3.49 compose (compose (codomain $_1) (compose h a)) $_462 % 3.27/3.49 |- ~(codomain a = domain $_462) \/ ~(codomain a = domain g) \/ % 3.27/3.49 compose (compose g a) (compose (compose h a) $_462) = % 3.27/3.49 compose (compose (compose g a) (compose h a)) $_462 % 3.27/3.49 |- ~(codomain a = domain $_462) \/ ~(codomain b = domain g) \/ % 3.27/3.49 compose (compose g (compose a b)) (compose (compose h a) $_462) = % 3.27/3.49 compose (compose (compose g (compose a b)) (compose h a)) $_462 % 3.27/3.49 |- ~(codomain a = domain $_462) \/ ~(codomain a = domain g) \/ % 3.27/3.49 compose (compose h a) (compose (compose h a) $_462) = % 3.27/3.49 compose (compose (compose h a) (compose h a)) $_462 % 3.27/3.49 |- ~(codomain a = domain g) \/ % 3.27/3.49 compose a (compose (compose h a) (compose g a)) = % 3.27/3.49 compose (compose a (compose h a)) (compose g a) % 3.27/3.49 |- ~(codomain a = domain g) \/ % 3.27/3.49 compose a (compose (compose h a) (compose g (compose a b))) = % 3.27/3.49 compose (compose a (compose h a)) (compose g (compose a b)) % 3.27/3.49 |- ~(codomain a = domain g) \/ % 3.27/3.49 compose a (compose (compose h a) (compose h a)) = % 3.27/3.49 compose (compose a (compose h a)) (compose h a) % 3.27/3.49 |- ~(codomain a = domain g) \/ % 3.27/3.49 compose (codomain a) (compose (compose h a) g) = % 3.27/3.49 compose (compose (codomain a) (compose h a)) g % 3.27/3.49 |- ~(codomain a = domain g) \/ % 3.27/3.49 compose (compose g a) (compose (compose h a) g) = % 3.27/3.49 compose (compose (compose g a) (compose h a)) g % 3.27/3.49 |- ~(codomain a = domain g) \/ % 3.27/3.49 compose (compose h a) (compose (compose h a) g) = % 3.27/3.49 compose (compose (compose h a) (compose h a)) g % 3.27/3.49 |- ~(codomain $_1 = codomain a) \/ ~(codomain a = domain g) \/ % 3.27/3.49 compose (codomain $_1) (compose (compose h a) (compose g a)) = % 3.27/3.49 compose (compose (codomain $_1) (compose h a)) (compose g a) % 3.27/3.49 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.49 compose (compose a b) (compose (compose h a) (compose g a)) = % 3.27/3.49 compose (compose (compose a b) (compose h a)) (compose g a) % 3.27/3.49 |- ~(codomain a = domain g) \/ % 3.27/3.49 compose (compose g a) (compose (compose h a) (compose g a)) = % 3.27/3.49 compose (compose (compose g a) (compose h a)) (compose g a) % 3.27/3.49 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.49 compose (compose g (compose a b)) % 3.27/3.49 (compose (compose h a) (compose g a)) = % 3.27/3.49 compose (compose (compose g (compose a b)) (compose h a)) (compose g a) % 3.27/3.49 |- ~(codomain a = domain g) \/ % 3.27/3.49 compose (compose h a) (compose (compose h a) (compose g a)) = % 3.27/3.49 compose (compose (compose h a) (compose h a)) (compose g a) % 3.27/3.49 |- ~(codomain a = domain g) \/ % 3.27/3.49 compose (codomain a) (compose (compose h a) (compose g a)) = % 3.27/3.49 compose (compose (codomain a) (compose h a)) (compose g a) % 3.27/3.49 |- ~(codomain $_1 = codomain a) \/ ~(codomain a = domain g) \/ % 3.27/3.49 compose (codomain $_1) (compose (compose h a) (compose h a)) = % 3.27/3.49 compose (compose (codomain $_1) (compose h a)) (compose h a) % 3.27/3.49 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.49 compose (compose a b) (compose (compose h a) (compose h a)) = % 3.27/3.49 compose (compose (compose a b) (compose h a)) (compose h a) % 3.27/3.49 |- ~(codomain a = domain g) \/ % 3.27/3.49 compose (compose g a) (compose (compose h a) (compose h a)) = % 3.27/3.49 compose (compose (compose g a) (compose h a)) (compose h a) % 3.27/3.49 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.49 compose (compose g (compose a b)) % 3.27/3.49 (compose (compose h a) (compose h a)) = % 3.27/3.49 compose (compose (compose g (compose a b)) (compose h a)) (compose h a) % 3.27/3.49 |- ~(codomain $_1 = domain g) \/ ~(codomain a = codomain g) \/ % 3.27/3.49 compose (codomain $_1) (compose (compose h a) (compose a b)) = % 3.27/3.49 compose (compose (codomain $_1) (compose h a)) (compose a b) % 3.27/3.49 |- ~(codomain a = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.49 compose (compose a b) (compose (compose h a) (compose a b)) = % 3.27/3.49 compose (compose (compose a b) (compose h a)) (compose a b) % 3.27/3.49 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.49 compose (compose g a) (compose (compose h a) (compose a b)) = % 3.27/3.49 compose (compose (compose g a) (compose h a)) (compose a b) % 3.27/3.49 |- ~(codomain a = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.49 compose (compose g (compose a b)) % 3.27/3.49 (compose (compose h a) (compose a b)) = % 3.27/3.49 compose (compose (compose g (compose a b)) (compose h a)) (compose a b) % 3.27/3.49 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.49 compose (compose h a) (compose (compose h a) (compose a b)) = % 3.27/3.49 compose (compose (compose h a) (compose h a)) (compose a b) % 3.27/3.49 |- ~(codomain a = codomain g) \/ ~(domain $X = domain g) \/ % 3.27/3.49 compose (domain $X) (compose (compose h a) (compose a b)) = % 3.27/3.49 compose (compose (domain $X) (compose h a)) (compose a b) % 3.27/3.49 |- ~(codomain a = codomain $X) \/ ~(codomain a = domain g) \/ % 3.27/3.49 compose (compose g a) (compose (compose h a) (codomain $X)) = % 3.27/3.49 compose (compose (compose g a) (compose h a)) (codomain $X) % 3.27/3.49 |- ~(codomain a = domain g) \/ % 3.27/3.49 compose (compose g a) % 3.27/3.49 (compose (compose h a) (compose g (compose a b))) = % 3.27/3.49 compose (compose (compose g a) (compose h a)) (compose g (compose a b)) % 3.27/3.49 |- ~(codomain a = codomain $X) \/ ~(codomain a = domain g) \/ % 3.27/3.49 compose (compose h a) (compose (compose h a) (codomain $X)) = % 3.27/3.49 compose (compose (compose h a) (compose h a)) (codomain $X) % 3.27/3.49 |- ~(codomain a = domain g) \/ % 3.27/3.49 compose (compose h a) % 3.27/3.49 (compose (compose h a) (compose g (compose a b))) = % 3.27/3.49 compose (compose (compose h a) (compose h a)) (compose g (compose a b)) % 3.27/3.49 |- ~(codomain $_1 = domain $_469) \/ ~(codomain $_469 = codomain g) \/ % 3.27/3.49 compose (codomain $_1) (compose $_469 (compose a b)) = % 3.27/3.49 compose (compose (codomain $_1) $_469) (compose a b) % 3.27/3.49 |- ~(codomain $_469 = codomain g) \/ ~(codomain b = domain $_469) \/ % 3.27/3.49 compose (compose a b) (compose $_469 (compose a b)) = % 3.27/3.49 compose (compose (compose a b) $_469) (compose a b) % 3.27/3.49 |- ~(codomain $_469 = codomain g) \/ ~(codomain a = domain $_469) \/ % 3.27/3.49 compose (compose g a) (compose $_469 (compose a b)) = % 3.27/3.49 compose (compose (compose g a) $_469) (compose a b) % 3.27/3.49 |- ~(codomain $_469 = codomain g) \/ ~(codomain b = domain $_469) \/ % 3.27/3.49 compose (compose g (compose a b)) (compose $_469 (compose a b)) = % 3.27/3.49 compose (compose (compose g (compose a b)) $_469) (compose a b) % 3.27/3.49 |- ~(codomain $_469 = codomain g) \/ ~(codomain a = domain $_469) \/ % 3.27/3.49 compose (compose h a) (compose $_469 (compose a b)) = % 3.27/3.49 compose (compose (compose h a) $_469) (compose a b) % 3.27/3.49 |- ~(codomain $_469 = codomain g) \/ ~(domain $X = domain $_469) \/ % 3.27/3.49 compose (domain $X) (compose $_469 (compose a b)) = % 3.27/3.49 compose (compose (domain $X) $_469) (compose a b) % 3.27/3.49 |- ~(codomain $X = codomain g) \/ ~(codomain $_468 = codomain $X) \/ % 3.27/3.49 compose $_468 (compose (codomain $X) (compose a b)) = % 3.27/3.49 compose (compose $_468 (codomain $X)) (compose a b) % 3.27/3.49 |- ~(codomain $_468 = domain g) \/ ~(codomain b = codomain g) \/ % 3.27/3.49 compose $_468 (compose (compose g (compose a b)) (compose a b)) = % 3.27/3.49 compose (compose $_468 (compose g (compose a b))) (compose a b) % 3.27/3.49 |- ~(codomain $X = codomain g) \/ % 3.27/3.49 compose g (compose (codomain $X) (compose a b)) = % 3.27/3.49 compose (compose g (codomain $X)) (compose a b) % 3.27/3.49 |- ~(codomain $X = codomain g) \/ ~(codomain a = codomain $X) \/ % 3.27/3.49 compose (compose g a) (compose (codomain $X) (compose a b)) = % 3.27/3.49 compose (compose (compose g a) (codomain $X)) (compose a b) % 3.27/3.49 |- ~(codomain a = domain g) \/ ~(codomain b = codomain g) \/ % 3.27/3.49 compose (compose g a) % 3.27/3.49 (compose (compose g (compose a b)) (compose a b)) = % 3.27/3.49 compose (compose (compose g a) (compose g (compose a b))) (compose a b) % 3.27/3.49 |- ~(codomain $X = codomain g) \/ ~(codomain a = codomain $X) \/ % 3.27/3.49 compose (compose h a) (compose (codomain $X) (compose a b)) = % 3.27/3.49 compose (compose (compose h a) (codomain $X)) (compose a b) % 3.27/3.49 |- ~(codomain a = domain g) \/ ~(codomain b = codomain g) \/ % 3.27/3.49 compose (compose h a) % 3.27/3.49 (compose (compose g (compose a b)) (compose a b)) = % 3.27/3.49 compose (compose (compose h a) (compose g (compose a b))) (compose a b) % 3.27/3.49 |- ~(codomain $_1 = domain $_474) \/ ~(codomain $_474 = domain g) \/ % 3.27/3.49 compose (codomain $_1) (compose $_474 (compose g a)) = % 3.27/3.49 compose (compose (codomain $_1) $_474) (compose g a) % 3.27/3.49 |- ~(codomain $_474 = domain g) \/ ~(codomain b = domain $_474) \/ % 3.27/3.49 compose (compose a b) (compose $_474 (compose g a)) = % 3.27/3.49 compose (compose (compose a b) $_474) (compose g a) % 3.27/3.49 |- ~(codomain $_474 = domain g) \/ ~(codomain a = domain $_474) \/ % 3.27/3.49 compose (compose g a) (compose $_474 (compose g a)) = % 3.27/3.49 compose (compose (compose g a) $_474) (compose g a) % 3.27/3.49 |- ~(codomain $_474 = domain g) \/ ~(codomain b = domain $_474) \/ % 3.27/3.49 compose (compose g (compose a b)) (compose $_474 (compose g a)) = % 3.27/3.49 compose (compose (compose g (compose a b)) $_474) (compose g a) % 3.27/3.49 |- ~(codomain $_474 = domain g) \/ ~(codomain a = domain $_474) \/ % 3.27/3.49 compose (compose h a) (compose $_474 (compose g a)) = % 3.27/3.49 compose (compose (compose h a) $_474) (compose g a) % 3.27/3.49 |- ~(codomain $_474 = domain g) \/ ~(domain $X = domain $_474) \/ % 3.27/3.49 compose (domain $X) (compose $_474 (compose g a)) = % 3.27/3.49 compose (compose (domain $X) $_474) (compose g a) % 3.27/3.49 |- ~(codomain $X = domain g) \/ ~(codomain $_473 = codomain $X) \/ % 3.27/3.49 compose $_473 (compose (codomain $X) (compose g a)) = % 3.27/3.49 compose (compose $_473 (codomain $X)) (compose g a) % 3.27/3.49 |- ~(codomain $_473 = codomain b) \/ ~(codomain b = domain g) \/ % 3.27/3.49 compose $_473 (compose (compose g (compose a b)) (compose g a)) = % 3.27/3.49 compose (compose $_473 (compose g (compose a b))) (compose g a) % 3.27/3.49 |- ~(codomain g = domain g) \/ % 3.27/3.49 compose (codomain g) (compose g (compose g a)) = % 3.27/3.49 compose (compose (codomain g) g) (compose g a) % 3.27/3.49 |- ~(codomain b = domain g) \/ % 3.27/3.49 compose b (compose (compose g (compose a b)) (compose g a)) = % 3.27/3.49 compose (compose b (compose g (compose a b))) (compose g a) % 3.27/3.49 |- ~(codomain $X = domain g) \/ ~(codomain a = codomain $X) \/ % 3.27/3.49 compose (compose g a) (compose (codomain $X) (compose g a)) = % 3.27/3.49 compose (compose (compose g a) (codomain $X)) (compose g a) % 3.27/3.49 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.49 compose (compose g a) % 3.27/3.49 (compose (compose g (compose a b)) (compose g a)) = % 3.27/3.49 compose (compose (compose g a) (compose g (compose a b))) (compose g a) % 3.27/3.49 |- ~(codomain $X = domain g) \/ ~(codomain a = codomain $X) \/ % 3.27/3.49 compose (compose h a) (compose (codomain $X) (compose g a)) = % 3.27/3.49 compose (compose (compose h a) (codomain $X)) (compose g a) % 3.27/3.49 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.49 compose (compose h a) % 3.27/3.49 (compose (compose g (compose a b)) (compose g a)) = % 3.27/3.49 compose (compose (compose h a) (compose g (compose a b))) (compose g a) % 3.27/3.49 |- ~(codomain $_1 = codomain b) \/ ~(codomain b = domain g) \/ % 3.27/3.49 compose (codomain $_1) % 3.27/3.49 (compose (compose g (compose a b)) (compose g a)) = % 3.27/3.49 compose (compose (codomain $_1) (compose g (compose a b))) (compose g a) % 3.27/3.49 |- ~(codomain b = domain g) \/ % 3.27/3.49 compose (compose a b) % 3.27/3.49 (compose (compose g (compose a b)) (compose g a)) = % 3.27/3.49 compose (compose (compose a b) (compose g (compose a b))) (compose g a) % 3.27/3.49 |- ~(codomain b = domain g) \/ % 3.27/3.49 compose (compose g (compose a b)) % 3.27/3.49 (compose (compose g (compose a b)) (compose g a)) = % 3.27/3.49 compose (compose (compose g (compose a b)) (compose g (compose a b))) % 3.27/3.49 (compose g a) % 3.27/3.49 |- ~(codomain b = domain g) \/ % 3.27/3.49 compose (codomain b) (compose (compose g (compose a b)) (compose g a)) = % 3.27/3.49 compose (compose (codomain b) (compose g (compose a b))) (compose g a) % 3.27/3.49 |- ~(codomain $X = domain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.49 compose (compose a b) (compose (codomain $X) (compose g a)) = % 3.27/3.49 compose (compose (compose a b) (codomain $X)) (compose g a) % 3.27/3.49 |- ~(codomain $_1 = domain $_482) \/ ~(codomain $_482 = domain g) \/ % 3.27/3.49 compose (codomain $_1) (compose $_482 (compose h a)) = % 3.27/3.49 compose (compose (codomain $_1) $_482) (compose h a) % 3.27/3.49 |- ~(codomain $_482 = domain g) \/ ~(codomain b = domain $_482) \/ % 3.27/3.49 compose (compose a b) (compose $_482 (compose h a)) = % 3.27/3.49 compose (compose (compose a b) $_482) (compose h a) % 3.27/3.49 |- ~(codomain $_482 = domain g) \/ ~(codomain a = domain $_482) \/ % 3.27/3.49 compose (compose g a) (compose $_482 (compose h a)) = % 3.27/3.49 compose (compose (compose g a) $_482) (compose h a) % 3.27/3.49 |- ~(codomain $_482 = domain g) \/ ~(codomain b = domain $_482) \/ % 3.27/3.49 compose (compose g (compose a b)) (compose $_482 (compose h a)) = % 3.27/3.49 compose (compose (compose g (compose a b)) $_482) (compose h a) % 3.27/3.49 |- ~(codomain $_482 = domain g) \/ ~(codomain a = domain $_482) \/ % 3.27/3.49 compose (compose h a) (compose $_482 (compose h a)) = % 3.27/3.49 compose (compose (compose h a) $_482) (compose h a) % 3.27/3.49 |- ~(codomain $_482 = domain g) \/ ~(domain $X = domain $_482) \/ % 3.27/3.49 compose (domain $X) (compose $_482 (compose h a)) = % 3.27/3.49 compose (compose (domain $X) $_482) (compose h a) % 3.27/3.49 |- ~(codomain $X = domain g) \/ ~(codomain $_481 = codomain $X) \/ % 3.27/3.49 compose $_481 (compose (codomain $X) (compose h a)) = % 3.27/3.49 compose (compose $_481 (codomain $X)) (compose h a) % 3.27/3.49 |- ~(codomain $_481 = codomain b) \/ ~(codomain b = domain g) \/ % 3.27/3.49 compose $_481 (compose (compose g (compose a b)) (compose h a)) = % 3.27/3.49 compose (compose $_481 (compose g (compose a b))) (compose h a) % 3.27/3.49 |- ~(codomain g = domain g) \/ % 3.27/3.49 compose (codomain g) (compose g (compose h a)) = % 3.27/3.49 compose (compose (codomain g) g) (compose h a) % 3.27/3.49 |- ~(codomain b = domain g) \/ % 3.27/3.49 compose b (compose (compose g (compose a b)) (compose h a)) = % 3.27/3.49 compose (compose b (compose g (compose a b))) (compose h a) % 3.27/3.49 |- ~(codomain $X = domain g) \/ ~(codomain a = codomain $X) \/ % 3.27/3.49 compose (compose g a) (compose (codomain $X) (compose h a)) = % 3.27/3.49 compose (compose (compose g a) (codomain $X)) (compose h a) % 3.27/3.49 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.49 compose (compose g a) % 3.27/3.49 (compose (compose g (compose a b)) (compose h a)) = % 3.27/3.49 compose (compose (compose g a) (compose g (compose a b))) (compose h a) % 3.27/3.49 |- ~(codomain $X = domain g) \/ ~(codomain a = codomain $X) \/ % 3.27/3.49 compose (compose h a) (compose (codomain $X) (compose h a)) = % 3.27/3.49 compose (compose (compose h a) (codomain $X)) (compose h a) % 3.27/3.49 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.49 compose (compose h a) % 3.27/3.49 (compose (compose g (compose a b)) (compose h a)) = % 3.27/3.49 compose (compose (compose h a) (compose g (compose a b))) (compose h a) % 3.27/3.49 |- ~(codomain $_1 = codomain b) \/ ~(codomain b = domain g) \/ % 3.27/3.49 compose (codomain $_1) % 3.27/3.49 (compose (compose g (compose a b)) (compose h a)) = % 3.27/3.49 compose (compose (codomain $_1) (compose g (compose a b))) (compose h a) % 3.27/3.49 |- ~(codomain b = domain g) \/ % 3.27/3.49 compose (compose a b) % 3.27/3.49 (compose (compose g (compose a b)) (compose h a)) = % 3.27/3.49 compose (compose (compose a b) (compose g (compose a b))) (compose h a) % 3.27/3.49 |- ~(codomain b = domain g) \/ % 3.27/3.49 compose (compose g (compose a b)) % 3.27/3.49 (compose (compose g (compose a b)) (compose h a)) = % 3.27/3.49 compose (compose (compose g (compose a b)) (compose g (compose a b))) % 3.27/3.49 (compose h a) % 3.27/3.49 |- ~(codomain b = domain g) \/ % 3.27/3.49 compose (codomain b) (compose (compose g (compose a b)) (compose h a)) = % 3.27/3.49 compose (compose (codomain b) (compose g (compose a b))) (compose h a) % 3.27/3.49 |- ~(codomain $X = domain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.49 compose (compose a b) (compose (codomain $X) (compose h a)) = % 3.27/3.49 compose (compose (compose a b) (codomain $X)) (compose h a) % 3.27/3.49 |- ~(codomain $X = domain $_490) \/ ~(codomain b = codomain $X) \/ % 3.27/3.49 compose (compose a b) (compose (codomain $X) $_490) = % 3.27/3.49 compose (compose (compose a b) (codomain $X)) $_490 % 3.27/3.50 |- ~(codomain b = codomain g) \/ ~(codomain b = domain $_490) \/ % 3.27/3.50 compose (compose a b) (compose (compose a b) $_490) = % 3.27/3.50 compose (compose (compose a b) (compose a b)) $_490 % 3.27/3.50 |- ~(codomain a = domain $_490) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (compose a b) (compose (compose g a) $_490) = % 3.27/3.50 compose (compose (compose a b) (compose g a)) $_490 % 3.27/3.50 |- ~(codomain b = domain $_490) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (compose a b) (compose (compose g (compose a b)) $_490) = % 3.27/3.50 compose (compose (compose a b) (compose g (compose a b))) $_490 % 3.27/3.50 |- ~(codomain a = domain $_490) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (compose a b) (compose (compose h a) $_490) = % 3.27/3.50 compose (compose (compose a b) (compose h a)) $_490 % 3.27/3.50 |- ~(codomain $_489 = codomain $X) \/ ~(codomain b = domain $_489) \/ % 3.27/3.50 compose (compose a b) (compose $_489 (codomain $X)) = % 3.27/3.50 compose (compose (compose a b) $_489) (codomain $X) % 3.27/3.50 |- ~(codomain $_489 = domain g) \/ ~(codomain b = domain $_489) \/ % 3.27/3.50 compose (compose a b) (compose $_489 (compose g (compose a b))) = % 3.27/3.50 compose (compose (compose a b) $_489) (compose g (compose a b)) % 3.27/3.50 |- ~(codomain b = domain g) \/ % 3.27/3.50 compose (compose a b) (compose (compose g (compose a b)) g) = % 3.27/3.50 compose (compose (compose a b) (compose g (compose a b))) g % 3.27/3.50 |- ~(codomain a = codomain $X) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (compose a b) (compose (compose g a) (codomain $X)) = % 3.27/3.50 compose (compose (compose a b) (compose g a)) (codomain $X) % 3.27/3.50 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.50 compose (compose a b) % 3.27/3.50 (compose (compose g a) (compose g (compose a b))) = % 3.27/3.50 compose (compose (compose a b) (compose g a)) (compose g (compose a b)) % 3.27/3.50 |- ~(codomain a = codomain $X) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (compose a b) (compose (compose h a) (codomain $X)) = % 3.27/3.50 compose (compose (compose a b) (compose h a)) (codomain $X) % 3.27/3.50 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.50 compose (compose a b) % 3.27/3.50 (compose (compose h a) (compose g (compose a b))) = % 3.27/3.50 compose (compose (compose a b) (compose h a)) (compose g (compose a b)) % 3.27/3.50 |- ~(codomain $X = domain $_494) \/ ~(codomain a = codomain $X) \/ % 3.27/3.50 compose (compose g a) (compose (codomain $X) $_494) = % 3.27/3.50 compose (compose (compose g a) (codomain $X)) $_494 % 3.27/3.50 |- ~(codomain a = domain g) \/ ~(codomain b = domain $_494) \/ % 3.27/3.50 compose (compose g a) (compose (compose g (compose a b)) $_494) = % 3.27/3.50 compose (compose (compose g a) (compose g (compose a b))) $_494 % 3.27/3.50 |- ~(codomain $_493 = codomain $X) \/ ~(codomain a = domain $_493) \/ % 3.27/3.50 compose (compose g a) (compose $_493 (codomain $X)) = % 3.27/3.50 compose (compose (compose g a) $_493) (codomain $X) % 3.27/3.50 |- ~(codomain $_493 = domain g) \/ ~(codomain a = domain $_493) \/ % 3.27/3.50 compose (compose g a) (compose $_493 (compose g (compose a b))) = % 3.27/3.50 compose (compose (compose g a) $_493) (compose g (compose a b)) % 3.27/3.50 |- ~(codomain $_493 = domain $X) \/ ~(codomain a = domain $_493) \/ % 3.27/3.50 compose (compose g a) (compose $_493 (domain $X)) = % 3.27/3.50 compose (compose (compose g a) $_493) (domain $X) % 3.27/3.50 |- ~(codomain a = domain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.50 compose (compose g a) % 3.27/3.50 (compose (compose g (compose a b)) (codomain $X)) = % 3.27/3.50 compose (compose (compose g a) (compose g (compose a b))) (codomain $X) % 3.27/3.50 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.50 compose (compose g a) % 3.27/3.50 (compose (compose g (compose a b)) (compose g (compose a b))) = % 3.27/3.50 compose (compose (compose g a) (compose g (compose a b))) % 3.27/3.50 (compose g (compose a b)) % 3.27/3.50 |- ~(codomain $X = domain g) \/ ~(codomain a = codomain $X) \/ % 3.27/3.50 compose (compose g a) % 3.27/3.50 (compose (codomain $X) (compose g (compose a b))) = % 3.27/3.50 compose (compose (compose g a) (codomain $X)) (compose g (compose a b)) % 3.27/3.50 |- ~(codomain $X = domain $_499) \/ ~(codomain a = codomain $X) \/ % 3.27/3.50 compose (compose h a) (compose (codomain $X) $_499) = % 3.27/3.50 compose (compose (compose h a) (codomain $X)) $_499 % 3.27/3.50 |- ~(codomain a = domain g) \/ ~(codomain b = domain $_499) \/ % 3.27/3.50 compose (compose h a) (compose (compose g (compose a b)) $_499) = % 3.27/3.50 compose (compose (compose h a) (compose g (compose a b))) $_499 % 3.27/3.50 |- ~(codomain $_498 = codomain $X) \/ ~(codomain a = domain $_498) \/ % 3.27/3.50 compose (compose h a) (compose $_498 (codomain $X)) = % 3.27/3.50 compose (compose (compose h a) $_498) (codomain $X) % 3.27/3.50 |- ~(codomain $_498 = domain g) \/ ~(codomain a = domain $_498) \/ % 3.27/3.50 compose (compose h a) (compose $_498 (compose g (compose a b))) = % 3.27/3.50 compose (compose (compose h a) $_498) (compose g (compose a b)) % 3.27/3.50 |- ~(codomain $_498 = domain $X) \/ ~(codomain a = domain $_498) \/ % 3.27/3.50 compose (compose h a) (compose $_498 (domain $X)) = % 3.27/3.50 compose (compose (compose h a) $_498) (domain $X) % 3.27/3.50 |- ~(codomain a = domain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.50 compose (compose h a) % 3.27/3.50 (compose (compose g (compose a b)) (codomain $X)) = % 3.27/3.50 compose (compose (compose h a) (compose g (compose a b))) (codomain $X) % 3.27/3.50 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.50 compose (compose h a) % 3.27/3.50 (compose (compose g (compose a b)) (compose g (compose a b))) = % 3.27/3.50 compose (compose (compose h a) (compose g (compose a b))) % 3.27/3.50 (compose g (compose a b)) % 3.27/3.50 |- ~(codomain $X = domain g) \/ ~(codomain a = codomain $X) \/ % 3.27/3.50 compose (compose h a) % 3.27/3.50 (compose (codomain $X) (compose g (compose a b))) = % 3.27/3.50 compose (compose (compose h a) (codomain $X)) (compose g (compose a b)) % 3.27/3.50 |- ~(codomain $_1 = codomain a) \/ ~(codomain a = domain g) \/ % 3.27/3.50 compose (codomain $_1) % 3.27/3.50 (compose (compose g a) (compose g (compose a b))) = % 3.27/3.50 compose (compose (codomain $_1) (compose g a)) (compose g (compose a b)) % 3.27/3.50 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.50 compose (compose g (compose a b)) % 3.27/3.50 (compose (compose g a) (compose g (compose a b))) = % 3.27/3.50 compose (compose (compose g (compose a b)) (compose g a)) % 3.27/3.50 (compose g (compose a b)) % 3.27/3.50 |- ~(codomain a = domain g) \/ % 3.27/3.50 compose (codomain a) (compose (compose g a) (compose g (compose a b))) = % 3.27/3.50 compose (compose (codomain a) (compose g a)) (compose g (compose a b)) % 3.27/3.50 |- ~(codomain $_1 = codomain a) \/ ~(codomain a = domain g) \/ % 3.27/3.50 compose (codomain $_1) % 3.27/3.50 (compose (compose h a) (compose g (compose a b))) = % 3.27/3.50 compose (compose (codomain $_1) (compose h a)) (compose g (compose a b)) % 3.27/3.50 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.50 compose (compose g (compose a b)) % 3.27/3.50 (compose (compose h a) (compose g (compose a b))) = % 3.27/3.50 compose (compose (compose g (compose a b)) (compose h a)) % 3.27/3.50 (compose g (compose a b)) % 3.27/3.50 |- ~(codomain a = domain g) \/ % 3.27/3.50 compose (codomain a) (compose (compose h a) (compose g (compose a b))) = % 3.27/3.50 compose (compose (codomain a) (compose h a)) (compose g (compose a b)) % 3.27/3.50 |- ~(codomain $_1 = domain g) \/ ~(codomain b = codomain g) \/ % 3.27/3.50 compose (codomain $_1) % 3.27/3.50 (compose (compose g (compose a b)) (compose a b)) = % 3.27/3.50 compose (compose (codomain $_1) (compose g (compose a b))) (compose a b) % 3.27/3.50 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (compose a b) % 3.27/3.50 (compose (compose g (compose a b)) (compose a b)) = % 3.27/3.50 compose (compose (compose a b) (compose g (compose a b))) (compose a b) % 3.27/3.50 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (compose g (compose a b)) % 3.27/3.50 (compose (compose g (compose a b)) (compose a b)) = % 3.27/3.50 compose (compose (compose g (compose a b)) (compose g (compose a b))) % 3.27/3.50 (compose a b) % 3.27/3.50 |- ~(codomain b = codomain g) \/ ~(domain $X = domain g) \/ % 3.27/3.50 compose (domain $X) (compose (compose g (compose a b)) (compose a b)) = % 3.27/3.50 compose (compose (domain $X) (compose g (compose a b))) (compose a b) % 3.27/3.50 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (codomain b) (compose h (compose g a)) = % 3.27/3.50 compose (compose (codomain b) h) (compose g a) % 3.27/3.50 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.50 compose (codomain a) (compose h (compose g a)) = % 3.27/3.50 compose (compose (codomain a) h) (compose g a) % 3.27/3.50 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (codomain b) (compose h (compose h a)) = % 3.27/3.50 compose (compose (codomain b) h) (compose h a) % 3.27/3.50 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.50 compose (codomain a) (compose h (compose h a)) = % 3.27/3.50 compose (compose (codomain a) h) (compose h a) % 3.27/3.50 |- ~(codomain $X = codomain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.50 compose (compose a b) (compose (codomain $X) (compose a b)) = % 3.27/3.50 compose (compose (compose a b) (codomain $X)) (compose a b) % 3.27/3.50 |- ~(codomain b = codomain $X) \/ ~(codomain b = codomain g) \/ % 3.27/3.50 compose (compose a b) (compose (compose a b) (codomain $X)) = % 3.27/3.50 compose (compose (compose a b) (compose a b)) (codomain $X) % 3.27/3.50 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (compose a b) % 3.27/3.50 (compose (compose a b) (compose g (compose a b))) = % 3.27/3.50 compose (compose (compose a b) (compose a b)) (compose g (compose a b)) % 3.27/3.50 |- ~(codomain $X = codomain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.50 compose (compose g (compose a b)) (compose (codomain $X) a) = % 3.27/3.50 compose (compose (compose g (compose a b)) (codomain $X)) a % 3.27/3.50 |- ~(codomain $_1 = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (codomain $_1) % 3.27/3.50 (compose (compose a b) (compose g (compose a b))) = % 3.27/3.50 compose (compose (codomain $_1) (compose a b)) (compose g (compose a b)) % 3.27/3.50 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (compose g (compose a b)) % 3.27/3.50 (compose (compose a b) (compose g (compose a b))) = % 3.27/3.50 compose (compose (compose g (compose a b)) (compose a b)) % 3.27/3.50 (compose g (compose a b)) % 3.27/3.50 |- ~(codomain $X = domain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.50 compose (compose g (compose a b)) % 3.27/3.50 (compose (codomain $X) (compose g a)) = % 3.27/3.50 compose (compose (compose g (compose a b)) (codomain $X)) (compose g a) % 3.27/3.50 |- ~(codomain $X = domain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.50 compose (compose g (compose a b)) % 3.27/3.50 (compose (codomain $X) (compose h a)) = % 3.27/3.50 compose (compose (compose g (compose a b)) (codomain $X)) (compose h a) % 3.27/3.50 |- ~(codomain a = codomain b) \/ ~(codomain a = codomain g) \/ % 3.27/3.50 compose (compose a b) a = compose (compose (compose a b) a) (codomain a) % 3.27/3.50 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.50 compose (codomain a) (compose b a) = compose b a % 3.27/3.50 |- ~(codomain a = codomain b) \/ ~(codomain a = domain g) \/ % 3.27/3.50 compose (codomain a) (compose (compose g (compose a b)) h) = % 3.27/3.50 compose (compose (codomain a) (compose g (compose a b))) h % 3.27/3.50 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (codomain b) (compose h (compose g (compose a b))) = % 3.27/3.50 compose (compose (codomain b) h) (compose g (compose a b)) % 3.27/3.50 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.50 compose (codomain a) (compose h (compose g (compose a b))) = % 3.27/3.50 compose (compose (codomain a) h) (compose g (compose a b)) % 3.27/3.50 |- ~(codomain a = codomain $X) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (compose g (compose a b)) % 3.27/3.50 (compose (compose g a) (codomain $X)) = % 3.27/3.50 compose (compose (compose g (compose a b)) (compose g a)) (codomain $X) % 3.27/3.50 |- ~(codomain a = codomain b) \/ ~(codomain a = domain g) \/ % 3.27/3.50 compose (compose g (compose a b)) (compose g a) = % 3.27/3.50 compose (compose (compose g (compose a b)) (compose g a)) (codomain a) % 3.27/3.50 |- ~(codomain a = codomain $X) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (compose g (compose a b)) % 3.27/3.50 (compose (compose h a) (codomain $X)) = % 3.27/3.50 compose (compose (compose g (compose a b)) (compose h a)) (codomain $X) % 3.27/3.50 |- ~(codomain a = codomain b) \/ ~(codomain a = domain g) \/ % 3.27/3.50 compose (compose g (compose a b)) (compose h a) = % 3.27/3.50 compose (compose (compose g (compose a b)) (compose h a)) (codomain a) % 3.27/3.50 |- ~(codomain $X = codomain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.50 compose (compose g (compose a b)) % 3.27/3.50 (compose (codomain $X) (compose a b)) = % 3.27/3.50 compose (compose (compose g (compose a b)) (codomain $X)) (compose a b) % 3.27/3.50 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.50 compose (codomain a) (compose b (compose a b)) = compose b (compose a b) % 3.27/3.50 |- ~(codomain b = codomain $X) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (compose a b) % 3.27/3.50 (compose (compose g (compose a b)) (codomain $X)) = % 3.27/3.50 compose (compose (compose a b) (compose g (compose a b))) (codomain $X) % 3.27/3.50 |- ~(codomain b = domain g) \/ % 3.27/3.50 compose (compose a b) % 3.27/3.50 (compose (compose g (compose a b)) (compose g (compose a b))) = % 3.27/3.50 compose (compose (compose a b) (compose g (compose a b))) % 3.27/3.50 (compose g (compose a b)) % 3.27/3.50 |- ~(codomain $X = domain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.50 compose (compose a b) % 3.27/3.50 (compose (codomain $X) (compose g (compose a b))) = % 3.27/3.50 compose (compose (compose a b) (codomain $X)) (compose g (compose a b)) % 3.27/3.50 |- ~(codomain b = codomain $X) \/ ~(codomain b = codomain g) \/ % 3.27/3.50 compose (compose g (compose a b)) % 3.27/3.50 (compose (compose a b) (codomain $X)) = % 3.27/3.50 compose (compose (compose g (compose a b)) (compose a b)) (codomain $X) % 3.27/3.50 |- ~(codomain a = codomain b) \/ ~(codomain a = codomain g) \/ % 3.27/3.50 compose (compose g (compose a b)) a = % 3.27/3.50 compose (compose (compose g (compose a b)) a) (codomain a) % 3.27/3.50 |- ~(codomain $_561 = domain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.50 compose $_561 (compose (compose g (compose a b)) (codomain $X)) = % 3.27/3.50 compose (compose $_561 (compose g (compose a b))) (codomain $X) % 3.27/3.50 |- ~(codomain $_561 = codomain b) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose $_561 % 3.27/3.50 (compose (compose g (compose a b)) (compose g (compose a b))) = % 3.27/3.50 compose (compose $_561 (compose g (compose a b))) % 3.27/3.50 (compose g (compose a b)) % 3.27/3.50 |- ~(codomain $_1 = domain g) \/ ~(codomain b = domain $_562) \/ % 3.27/3.50 compose (codomain $_1) (compose (compose g (compose a b)) $_562) = % 3.27/3.50 compose (compose (codomain $_1) (compose g (compose a b))) $_562 % 3.27/3.50 |- ~(codomain b = domain $_562) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (compose g (compose a b)) % 3.27/3.50 (compose (compose g (compose a b)) $_562) = % 3.27/3.50 compose (compose (compose g (compose a b)) (compose g (compose a b))) % 3.27/3.50 $_562 % 3.27/3.50 |- ~(codomain b = domain $_562) \/ ~(domain $X = domain g) \/ % 3.27/3.50 compose (domain $X) (compose (compose g (compose a b)) $_562) = % 3.27/3.50 compose (compose (domain $X) (compose g (compose a b))) $_562 % 3.27/3.50 |- ~(codomain b = domain g) \/ % 3.27/3.50 compose b % 3.27/3.50 (compose (compose g (compose a b)) (compose g (compose a b))) = % 3.27/3.50 compose (compose b (compose g (compose a b))) (compose g (compose a b)) % 3.27/3.50 |- ~(codomain b = domain g) \/ % 3.27/3.50 compose (codomain b) (compose (compose g (compose a b)) g) = % 3.27/3.50 compose (compose (codomain b) (compose g (compose a b))) g % 3.27/3.50 |- ~(codomain b = domain g) \/ % 3.27/3.50 compose (compose g (compose a b)) % 3.27/3.50 (compose (compose g (compose a b)) g) = % 3.27/3.50 compose (compose (compose g (compose a b)) (compose g (compose a b))) g % 3.27/3.50 |- ~(codomain $_1 = codomain b) \/ ~(codomain b = domain g) \/ % 3.27/3.50 compose (codomain $_1) % 3.27/3.50 (compose (compose g (compose a b)) (compose g (compose a b))) = % 3.27/3.50 compose (compose (codomain $_1) (compose g (compose a b))) % 3.27/3.50 (compose g (compose a b)) % 3.27/3.51 |- ~(codomain a = codomain b) \/ ~(codomain a = domain g) \/ % 3.27/3.51 compose (codomain a) % 3.27/3.51 (compose (compose g (compose a b)) (compose g (compose a b))) = % 3.27/3.51 compose (compose (codomain a) (compose g (compose a b))) % 3.27/3.51 (compose g (compose a b)) % 3.27/3.51 |- ~(codomain b = codomain $X) \/ ~(codomain b = domain g) \/ % 3.27/3.51 compose (compose g (compose a b)) % 3.27/3.51 (compose (compose g (compose a b)) (codomain $X)) = % 3.27/3.51 compose (compose (compose g (compose a b)) (compose g (compose a b))) % 3.27/3.51 (codomain $X) % 3.27/3.51 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.51 compose (compose g (compose a b)) % 3.27/3.51 (compose (compose g (compose a b)) (codomain a)) = % 3.27/3.51 compose (compose (compose g (compose a b)) (compose g (compose a b))) % 3.27/3.51 (codomain a) % 3.27/3.51 |- ~(codomain $_1 = domain $_568) \/ ~(codomain $_568 = domain g) \/ % 3.27/3.51 compose (codomain $_1) (compose $_568 (compose g (compose a b))) = % 3.27/3.51 compose (compose (codomain $_1) $_568) (compose g (compose a b)) % 3.27/3.51 |- ~(codomain $_568 = domain g) \/ ~(codomain b = domain $_568) \/ % 3.27/3.51 compose (compose g (compose a b)) % 3.27/3.51 (compose $_568 (compose g (compose a b))) = % 3.27/3.51 compose (compose (compose g (compose a b)) $_568) % 3.27/3.51 (compose g (compose a b)) % 3.27/3.51 |- ~(codomain $_568 = domain g) \/ ~(domain $X = domain $_568) \/ % 3.27/3.51 compose (domain $X) (compose $_568 (compose g (compose a b))) = % 3.27/3.51 compose (compose (domain $X) $_568) (compose g (compose a b)) % 3.27/3.51 |- ~(codomain $X = domain g) \/ ~(codomain $_567 = codomain $X) \/ % 3.27/3.51 compose $_567 (compose (codomain $X) (compose g (compose a b))) = % 3.27/3.51 compose (compose $_567 (codomain $X)) (compose g (compose a b)) % 3.27/3.51 |- ~(codomain $_567 = domain $X) \/ ~(domain $X = domain g) \/ % 3.27/3.51 compose $_567 (compose (domain $X) (compose g (compose a b))) = % 3.27/3.51 compose (compose $_567 (domain $X)) (compose g (compose a b)) % 3.27/3.51 |- ~(codomain g = domain g) \/ % 3.27/3.51 compose (codomain g) (compose g (compose g (compose a b))) = % 3.27/3.51 compose (compose (codomain g) g) (compose g (compose a b)) % 3.27/3.51 |- ~(codomain $X = domain g) \/ ~(codomain b = codomain $X) \/ % 3.27/3.51 compose (compose g (compose a b)) % 3.27/3.51 (compose (codomain $X) (compose g (compose a b))) = % 3.27/3.51 compose (compose (compose g (compose a b)) (codomain $X)) % 3.27/3.51 (compose g (compose a b)) % 3.27/3.51 |- ~(codomain $X = domain $_572) \/ ~(codomain b = codomain $X) \/ % 3.27/3.51 compose (compose g (compose a b)) (compose (codomain $X) $_572) = % 3.27/3.51 compose (compose (compose g (compose a b)) (codomain $X)) $_572 % 3.27/3.51 |- ~(codomain $_571 = codomain $X) \/ ~(codomain b = domain $_571) \/ % 3.27/3.51 compose (compose g (compose a b)) (compose $_571 (codomain $X)) = % 3.27/3.51 compose (compose (compose g (compose a b)) $_571) (codomain $X) % 3.27/3.51 |- ~(codomain $_571 = domain $X) \/ ~(codomain b = domain $_571) \/ % 3.27/3.51 compose (compose g (compose a b)) (compose $_571 (domain $X)) = % 3.27/3.51 compose (compose (compose g (compose a b)) $_571) (domain $X) % 3.27/3.51 |- ~(codomain a = codomain b) \/ ~(codomain a = codomain g) \/ % 3.27/3.51 compose (codomain a) (compose (compose a b) a) = % 3.27/3.51 compose (compose (codomain a) (compose a b)) a % 3.27/3.51 |- ~(codomain a = codomain b) \/ ~(codomain a = domain g) \/ % 3.27/3.51 compose (codomain a) (compose (compose g (compose a b)) (compose g a)) = % 3.27/3.51 compose (compose (codomain a) (compose g (compose a b))) (compose g a) % 3.27/3.51 |- ~(codomain a = codomain b) \/ ~(codomain a = domain g) \/ % 3.27/3.51 compose (codomain a) (compose (compose g (compose a b)) (compose h a)) = % 3.27/3.51 compose (compose (codomain a) (compose g (compose a b))) (compose h a) % 3.27/3.51 |- ~(codomain a = codomain b) \/ ~(codomain a = domain g) \/ % 3.27/3.51 compose (compose a b) (compose g a) = % 3.27/3.51 compose (compose (compose a b) (compose g a)) (codomain a) % 3.27/3.51 |- ~(codomain a = codomain b) \/ ~(codomain a = domain g) \/ % 3.27/3.51 compose (compose a b) (compose h a) = % 3.27/3.51 compose (compose (compose a b) (compose h a)) (codomain a) % 3.27/3.51 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.27/3.51 compose (compose a b) (compose (compose a b) (codomain a)) = % 3.27/3.51 compose (compose (compose a b) (compose a b)) (codomain a) % 3.27/3.51 |- ~(codomain $_1 = codomain $_588) \/ ~(codomain $_588 = domain $_590) \/ % 3.27/3.51 compose (codomain $_1) (compose (codomain $_588) $_590) = % 3.27/3.51 compose (compose (codomain $_1) (codomain $_588)) $_590 % 3.27/3.51 |- ~(codomain $_588 = domain g) \/ ~(codomain $_589 = codomain $_588) \/ % 3.27/3.51 compose $_589 (compose (codomain $_588) h) = % 3.27/3.51 compose (compose $_589 (codomain $_588)) h % 3.27/3.51 |- ~(codomain $_588 = domain $X) \/ % 3.27/3.51 compose (domain $X) (compose (codomain $_588) $X) = % 3.27/3.51 compose (compose (domain $X) (codomain $_588)) $X % 3.27/3.51 |- ~(codomain $_588 = codomain $_589) \/ % 3.27/3.51 compose $_589 (compose (codomain $_588) (codomain $_589)) = % 3.27/3.51 compose (compose $_589 (codomain $_588)) (codomain $_589) % 3.27/3.51 |- ~(domain $X = domain $_591) \/ % 3.27/3.51 compose (domain $_591) (compose (domain $X) $_591) = % 3.27/3.51 compose (compose (domain $_591) (domain $X)) $_591 % 3.27/3.51 |- ~(codomain $_592 = codomain g) \/ % 3.27/3.51 compose (codomain g) (compose (codomain $_592) a) = % 3.27/3.51 compose (compose (codomain g) (codomain $_592)) a % 3.27/3.51 |- ~(codomain $_592 = codomain a) \/ % 3.27/3.51 compose (codomain a) (compose (codomain $_592) b) = % 3.27/3.51 compose (compose (codomain a) (codomain $_592)) b % 3.27/3.51 |- ~(codomain $_592 = codomain g) \/ % 3.27/3.51 compose (codomain g) (compose (codomain $_592) (compose a b)) = % 3.27/3.51 compose (compose (codomain g) (codomain $_592)) (compose a b) % 3.27/3.51 |- ~(codomain $_592 = domain g) \/ % 3.27/3.51 compose (domain g) (compose (codomain $_592) (compose g a)) = % 3.27/3.51 compose (compose (domain g) (codomain $_592)) (compose g a) % 3.27/3.51 |- ~(codomain $_592 = domain g) \/ % 3.27/3.51 compose (domain g) % 3.27/3.51 (compose (codomain $_592) (compose g (compose a b))) = % 3.27/3.51 compose (compose (domain g) (codomain $_592)) (compose g (compose a b)) % 3.27/3.51 |- ~(codomain $_592 = domain g) \/ % 3.27/3.51 compose (domain g) (compose (codomain $_592) (compose h a)) = % 3.27/3.51 compose (compose (domain g) (codomain $_592)) (compose h a) % 3.27/3.51 |- ~(codomain $_592 = domain g) \/ % 3.27/3.51 compose (domain g) (compose (codomain $_592) h) = % 3.27/3.51 compose (compose (domain g) (codomain $_592)) h % 3.27/3.51 |- ~(domain $X = domain g) \/ % 3.27/3.51 compose (domain g) (compose (domain $X) h) = % 3.27/3.51 compose (compose (domain g) (domain $X)) h % 3.27/3.51 |- ~(domain $X = domain g) \/ % 3.27/3.51 compose (domain g) (compose (domain $X) (compose g a)) = % 3.27/3.51 compose (compose (domain g) (domain $X)) (compose g a) % 3.27/3.51 |- ~(domain $X = domain g) \/ % 3.27/3.51 compose (domain g) (compose (domain $X) (compose h a)) = % 3.27/3.51 compose (compose (domain g) (domain $X)) (compose h a) % 3.27/3.51 |- ~(domain $X = codomain $_603) \/ % 3.27/3.51 compose $_603 (compose (domain $X) (codomain $_603)) = % 3.27/3.51 compose (compose $_603 (domain $X)) (codomain $_603) % 3.27/3.51 |- ~(codomain $_602 = codomain $_1) \/ % 3.27/3.51 compose (codomain $_1) (compose (codomain $_602) (codomain $_1)) = % 3.27/3.51 compose (compose (codomain $_1) (codomain $_602)) (codomain $_1) % 3.27/3.51 |- ~(codomain $_602 = codomain b) \/ % 3.27/3.51 compose (compose a b) (compose (codomain $_602) (codomain b)) = % 3.27/3.51 compose (compose (compose a b) (codomain $_602)) (codomain b) % 3.27/3.51 |- ~(codomain $_602 = codomain a) \/ % 3.27/3.51 compose (compose g a) (compose (codomain $_602) (codomain a)) = % 3.27/3.51 compose (compose (compose g a) (codomain $_602)) (codomain a) % 3.27/3.51 |- ~(codomain $_602 = codomain b) \/ % 3.27/3.51 compose (compose g (compose a b)) % 3.27/3.51 (compose (codomain $_602) (codomain b)) = % 3.27/3.51 compose (compose (compose g (compose a b)) (codomain $_602)) % 3.27/3.51 (codomain b) % 3.27/3.51 |- ~(codomain $_602 = codomain a) \/ % 3.27/3.51 compose (compose h a) (compose (codomain $_602) (codomain a)) = % 3.27/3.51 compose (compose (compose h a) (codomain $_602)) (codomain a) % 3.27/3.51 |- ~(codomain $_602 = domain $X) \/ % 3.27/3.51 compose (domain $X) (compose (codomain $_602) (domain $X)) = % 3.27/3.51 compose (compose (domain $X) (codomain $_602)) (domain $X) % 3.27/3.51 |- ~(codomain $_602 = codomain g) \/ % 3.27/3.51 compose h (compose (codomain $_602) (codomain g)) = % 3.27/3.51 compose (compose h (codomain $_602)) (codomain g) % 3.27/3.51 |- ~(domain $X = domain g) \/ % 3.27/3.51 compose (domain g) (compose (domain $X) (compose g (compose a b))) = % 3.27/3.51 compose (compose (domain g) (domain $X)) (compose g (compose a b)) % 3.27/3.51 |- ~(domain $X = domain $_617) \/ % 3.27/3.51 compose (domain $_617) (compose (domain $X) (domain $_617)) = % 3.27/3.51 compose (compose (domain $_617) (domain $X)) (domain $_617) % 3.27/3.51 |- ~(domain $_619 = codomain $X) \/ % 3.27/3.51 compose (codomain $X) (compose (domain $_619) (codomain $X)) = % 3.27/3.51 compose (compose (codomain $X) (domain $_619)) (codomain $X) % 3.27/3.51 |- ~(codomain $_624 = domain $_623) \/ ~(domain $_623 = codomain $X) \/ % 3.27/3.51 compose $_624 (compose (domain $_623) (codomain $X)) = % 3.27/3.51 compose (compose $_624 (domain $_623)) (codomain $X) % 3.27/3.51 |- ~(codomain $_624 = domain $_623) \/ ~(domain $_623 = domain g) \/ % 3.27/3.51 compose $_624 (compose (domain $_623) (compose g a)) = % 3.27/3.51 compose (compose $_624 (domain $_623)) (compose g a) % 3.27/3.51 |- ~(codomain $_624 = domain $_623) \/ ~(domain $_623 = domain g) \/ % 3.27/3.51 compose $_624 (compose (domain $_623) (compose h a)) = % 3.27/3.51 compose (compose $_624 (domain $_623)) (compose h a) % 3.27/3.51 |- ~(codomain $_624 = domain $_623) \/ ~(domain $_623 = domain $X) \/ % 3.27/3.51 compose $_624 (compose (domain $_623) (domain $X)) = % 3.27/3.51 compose (compose $_624 (domain $_623)) (domain $X) % 3.27/3.51 |- ~(codomain $_624 = domain $_623) \/ ~(domain $_623 = domain g) \/ % 3.27/3.51 compose $_624 (compose (domain $_623) h) = % 3.27/3.51 compose (compose $_624 (domain $_623)) h % 3.27/3.51 |- ~(codomain $_1 = domain $_623) \/ ~(domain $_623 = domain $_625) \/ % 3.27/3.51 compose (codomain $_1) (compose (domain $_623) $_625) = % 3.27/3.51 compose (compose (codomain $_1) (domain $_623)) $_625 % 3.27/3.51 |- ~(domain $X = domain $_623) \/ ~(domain $_623 = domain $_625) \/ % 3.27/3.51 compose (domain $X) (compose (domain $_623) $_625) = % 3.27/3.51 compose (compose (domain $X) (domain $_623)) $_625 % 3.27/3.51 |- ~(codomain $_1 = codomain $_632) \/ ~(codomain $_633 = codomain $_1) \/ % 3.27/3.51 compose $_633 (compose (codomain $_1) (codomain $_632)) = % 3.27/3.51 compose (compose $_633 (codomain $_1)) (codomain $_632) % 3.27/3.51 |- ~(codomain $_633 = domain g) \/ ~(codomain g = codomain $_632) \/ % 3.27/3.51 compose $_633 (compose h (codomain $_632)) = % 3.27/3.51 compose (compose $_633 h) (codomain $_632) % 3.27/3.51 |- ~(codomain $_1 = domain $_634) \/ ~(codomain $_634 = codomain $_632) \/ % 3.27/3.51 compose (codomain $_1) (compose $_634 (codomain $_632)) = % 3.27/3.51 compose (compose (codomain $_1) $_634) (codomain $_632) % 3.27/3.51 |- ~(codomain $_1 = domain $_635) \/ ~(codomain $_636 = codomain $_1) \/ % 3.27/3.51 compose $_636 (compose (codomain $_1) (domain $_635)) = % 3.27/3.51 compose (compose $_636 (codomain $_1)) (domain $_635) % 3.27/3.51 |- ~(codomain $_1 = domain $_637) \/ ~(codomain $_637 = domain $_635) \/ % 3.27/3.51 compose (codomain $_1) (compose $_637 (domain $_635)) = % 3.27/3.51 compose (compose (codomain $_1) $_637) (domain $_635) % 3.27/3.51 |- ~(codomain $_637 = domain $_635) \/ ~(codomain b = domain $_637) \/ % 3.27/3.51 compose (compose a b) (compose $_637 (domain $_635)) = % 3.27/3.51 compose (compose (compose a b) $_637) (domain $_635) % 3.27/3.51 |- ~(codomain $_637 = domain $_635) \/ ~(domain $X = domain $_637) \/ % 3.27/3.51 compose (domain $X) (compose $_637 (domain $_635)) = % 3.27/3.51 compose (compose (domain $X) $_637) (domain $_635) % 3.27/3.51 |- ~(codomain $_637 = domain $_635) \/ ~(codomain g = domain $_637) \/ % 3.27/3.51 compose h (compose $_637 (domain $_635)) = % 3.27/3.51 compose (compose h $_637) (domain $_635) % 3.27/3.51 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.51 compose h (compose g a) = compose (compose h (compose g a)) (codomain a) % 3.27/3.51 |- ~(codomain b = codomain g) \/ ~(codomain b = domain g) \/ % 3.27/3.51 compose h (compose g (compose a b)) = % 3.27/3.51 compose (compose h (compose g (compose a b))) (codomain b) % 3.27/3.51 |- ~(codomain a = codomain g) \/ ~(codomain a = domain g) \/ % 3.27/3.51 compose h (compose h a) = compose (compose h (compose h a)) (codomain a) % 3.27/3.51 |- ~(codomain $_643 = domain g) \/ ~(codomain g = domain $_645) \/ % 3.27/3.51 compose (codomain $_643) (compose h $_645) = % 3.27/3.51 compose (compose (codomain $_643) h) $_645 % 3.27/3.51 |- ~(codomain $_643 = domain $_644) \/ ~(codomain $_644 = domain g) \/ % 3.27/3.51 compose (codomain $_643) (compose $_644 h) = % 3.27/3.51 compose (compose (codomain $_643) $_644) h % 3.27/3.51 |- ~(codomain $X = domain $_648) \/ ~(domain $_646 = codomain $X) \/ % 3.27/3.51 compose (domain $_646) (compose (codomain $X) $_648) = % 3.27/3.51 compose (compose (domain $_646) (codomain $X)) $_648 % 3.27/3.51 |- ~(codomain a = domain $_648) \/ ~(domain $_646 = domain g) \/ % 3.27/3.51 compose (domain $_646) (compose (compose g a) $_648) = % 3.27/3.51 compose (compose (domain $_646) (compose g a)) $_648 % 3.27/3.51 |- ~(codomain a = domain $_648) \/ ~(domain $_646 = domain g) \/ % 3.27/3.51 compose (domain $_646) (compose (compose h a) $_648) = % 3.27/3.51 compose (compose (domain $_646) (compose h a)) $_648 % 3.27/3.51 |- ~(codomain g = domain $_648) \/ ~(domain $_646 = domain g) \/ % 3.27/3.51 compose (domain $_646) (compose h $_648) = % 3.27/3.51 compose (compose (domain $_646) h) $_648 % 3.27/3.51 |- ~(codomain $_647 = codomain g) \/ ~(domain $_646 = domain $_647) \/ % 3.27/3.51 compose (domain $_646) (compose $_647 a) = % 3.27/3.51 compose (compose (domain $_646) $_647) a % 3.27/3.51 |- ~(codomain $_647 = codomain a) \/ ~(domain $_646 = domain $_647) \/ % 3.27/3.51 compose (domain $_646) (compose $_647 b) = % 3.27/3.51 compose (compose (domain $_646) $_647) b % 3.27/3.51 |- ~(codomain $_647 = codomain $X) \/ ~(domain $_646 = domain $_647) \/ % 3.27/3.51 compose (domain $_646) (compose $_647 (codomain $X)) = % 3.27/3.51 compose (compose (domain $_646) $_647) (codomain $X) % 3.27/3.51 |- ~(codomain $_647 = domain g) \/ ~(domain $_646 = domain $_647) \/ % 3.27/3.51 compose (domain $_646) (compose $_647 h) = % 3.27/3.51 compose (compose (domain $_646) $_647) h % 3.27/3.51 |- ~(codomain $_656 = codomain a) \/ ~(codomain a = codomain g) \/ % 3.27/3.51 compose $_656 a = compose (compose $_656 a) (codomain a) % 3.27/3.51 |- ~(codomain $_1 = codomain a) \/ ~(codomain a = codomain g) \/ % 3.27/3.51 compose (codomain $_1) a = % 3.27/3.51 compose (compose (codomain $_1) a) (codomain a) % 3.36/3.51 |- ~(codomain $_659 = codomain g) \/ ~(codomain a = codomain $X) \/ % 3.36/3.51 compose (codomain $_659) (compose a (codomain $X)) = % 3.36/3.51 compose (compose (codomain $_659) a) (codomain $X) % 3.36/3.51 |- ~(codomain $_1 = codomain a) \/ ~(codomain b = codomain $_661) \/ % 3.36/3.51 compose (codomain $_1) (compose b (codomain $_661)) = % 3.36/3.51 compose (compose (codomain $_1) b) (codomain $_661) % 3.36/3.51 |- ~(codomain a = domain $_664) \/ ~(codomain b = codomain a) \/ % 3.36/3.51 compose (codomain a) (compose b $_664) = compose b $_664 % 3.36/3.51 |- ~(codomain a = codomain $X) \/ ~(codomain b = codomain a) \/ % 3.36/3.51 compose (codomain a) (compose b (codomain $X)) = compose b (codomain $X) % 3.36/3.51 |- ~(codomain a = codomain g) \/ ~(codomain b = codomain a) \/ % 3.36/3.51 compose (compose g (compose a b)) (compose (compose a b) (codomain a)) = % 3.36/3.51 compose (compose (compose g (compose a b)) (compose a b)) (codomain a) % 3.36/3.51 |- ~(codomain a = codomain b) \/ ~(codomain a = codomain g) \/ % 3.36/3.51 compose (codomain a) (compose (compose a b) (compose a b)) = % 3.36/3.51 compose (compose (codomain a) (compose a b)) (compose a b) % 3.36/3.51 |- ~(codomain $X = codomain $_694) \/ ~(codomain g = codomain $X) \/ % 3.36/3.51 compose h (compose (codomain $X) (codomain $_694)) = % 3.36/3.51 compose (compose h (codomain $X)) (codomain $_694) % 3.36/3.51 |- ~(codomain $X = codomain a) \/ ~(codomain $_698 = codomain $X) \/ % 3.36/3.51 compose (codomain $_698) (compose (codomain $X) b) = % 3.36/3.51 compose (compose (codomain $_698) (codomain $X)) b % 3.36/3.51 |- ~(codomain $X = codomain g) \/ ~(codomain $_704 = codomain $X) \/ % 3.36/3.51 compose (codomain $_704) (compose (codomain $X) a) = % 3.36/3.51 compose (compose (codomain $_704) (codomain $X)) a % 3.36/3.52 |- ~(codomain $_704 = domain g) \/ ~(codomain b = codomain g) \/ % 3.36/3.52 compose (codomain $_704) (compose (compose g (compose a b)) a) = % 3.36/3.52 compose (compose (codomain $_704) (compose g (compose a b))) a % 3.36/3.52 |- ~(codomain b = codomain g) \/ ~(domain $X = domain g) \/ % 3.36/3.52 compose (domain $X) (compose (compose g (compose a b)) a) = % 3.36/3.52 compose (compose (domain $X) (compose g (compose a b))) a % 3.36/3.52 |- ~(codomain $_708 = codomain g) \/ ~(domain $X = codomain $_708) \/ % 3.36/3.52 compose (domain $X) (compose (codomain $_708) a) = % 3.36/3.52 compose (compose (domain $X) (codomain $_708)) a % 3.36/3.52 |- ~(codomain $_1 = codomain $_710) \/ ~(codomain $_710 = domain g) \/ % 3.36/3.52 compose (codomain $_1) (compose (codomain $_710) h) = % 3.36/3.52 compose (compose (codomain $_1) (codomain $_710)) h % 3.36/3.52 |- ~(codomain $_710 = domain g) \/ ~(domain $X = codomain $_710) \/ % 3.36/3.52 compose (domain $X) (compose (codomain $_710) h) = % 3.36/3.52 compose (compose (domain $X) (codomain $_710)) h % 3.36/3.52 |- ~(codomain $_712 = domain g) \/ ~(codomain g = codomain $X) \/ % 3.36/3.52 compose (codomain $_712) (compose h (codomain $X)) = % 3.36/3.52 compose (compose (codomain $_712) h) (codomain $X) % 3.36/3.52 |- ~(codomain $_714 = domain $X) \/ ~(domain $X = domain g) \/ % 3.36/3.52 compose (codomain $_714) (compose (domain $X) h) = % 3.36/3.52 compose (compose (codomain $_714) (domain $X)) h % 3.36/3.52 |- ~(codomain $_716 = codomain $X) \/ ~(codomain a = codomain $_716) \/ % 3.36/3.52 compose (compose g a) (compose (codomain $_716) (codomain $X)) = % 3.36/3.52 compose (compose (compose g a) (codomain $_716)) (codomain $X) % 3.36/3.52 |- ~(codomain $X = domain $_720) \/ ~(codomain a = codomain $X) \/ % 3.36/3.52 compose (compose g a) (compose (codomain $X) (domain $_720)) = % 3.36/3.52 compose (compose (compose g a) (codomain $X)) (domain $_720) % 3.36/3.52 |- ~(codomain $_722 = codomain $X) \/ ~(codomain a = codomain $_722) \/ % 3.36/3.52 compose (compose h a) (compose (codomain $_722) (codomain $X)) = % 3.36/3.52 compose (compose (compose h a) (codomain $_722)) (codomain $X) % 3.36/3.52 |- ~(codomain $X = domain $_726) \/ ~(codomain a = codomain $X) \/ % 3.36/3.52 compose (compose h a) (compose (codomain $X) (domain $_726)) = % 3.36/3.52 compose (compose (compose h a) (codomain $X)) (domain $_726) % 3.36/3.52 |- ~(codomain a = domain g) \/ ~(codomain b = codomain a) \/ % 3.36/3.52 compose (compose a b) (compose (compose g (compose a b)) (codomain a)) = % 3.36/3.52 compose (compose (compose a b) (compose g (compose a b))) (codomain a) % 3.36/3.52 |- ~(codomain $_738 = domain $X) \/ ~(codomain g = codomain $_738) \/ % 3.36/3.52 compose h (compose (codomain $_738) (domain $X)) = % 3.36/3.52 compose (compose h (codomain $_738)) (domain $X) % 3.36/3.52 |- ~(codomain $_754 = codomain a) \/ ~(domain $X = codomain $_754) \/ % 3.36/3.52 compose (domain $X) (compose (codomain $_754) b) = % 3.36/3.52 compose (compose (domain $X) (codomain $_754)) b % 3.36/3.52 |- ~(codomain $X = codomain g) \/ ~(codomain $_760 = codomain $X) \/ % 3.36/3.52 compose (codomain $_760) (compose (codomain $X) (compose a b)) = % 3.36/3.52 compose (compose (codomain $_760) (codomain $X)) (compose a b) % 3.36/3.52 |- ~(codomain $X = codomain g) \/ ~(domain $_762 = codomain $X) \/ % 3.36/3.52 compose (domain $_762) (compose (codomain $X) (compose a b)) = % 3.36/3.52 compose (compose (domain $_762) (codomain $X)) (compose a b) % 3.36/3.52 |- ~(codomain g = codomain $_772) \/ ~(domain $X = domain g) \/ % 3.36/3.52 compose (domain $X) (compose h (codomain $_772)) = % 3.36/3.52 compose (compose (domain $X) h) (codomain $_772) % 3.36/3.52 |- ~(codomain $_782 = codomain $X) \/ ~(codomain b = codomain $_782) \/ % 3.36/3.52 compose (compose g (compose a b)) % 3.36/3.52 (compose (codomain $_782) (codomain $X)) = % 3.36/3.52 compose (compose (compose g (compose a b)) (codomain $_782)) % 3.36/3.52 (codomain $X) % 3.36/3.52 |- ~(codomain $X = domain $_786) \/ ~(codomain b = codomain $X) \/ % 3.36/3.52 compose (compose g (compose a b)) % 3.36/3.52 (compose (codomain $X) (domain $_786)) = % 3.36/3.52 compose (compose (compose g (compose a b)) (codomain $X)) (domain $_786) % 3.36/3.52 |- ~(codomain $X = codomain $_790) \/ ~(codomain b = codomain $X) \/ % 3.36/3.52 compose (compose a b) (compose (codomain $X) (codomain $_790)) = % 3.36/3.52 compose (compose (compose a b) (codomain $X)) (codomain $_790) % 3.36/3.52 |- ~(codomain $_793 = codomain b) \/ ~(codomain b = codomain g) \/ % 3.36/3.52 compose $_793 (compose a b) = % 3.36/3.52 compose (compose $_793 (compose a b)) (codomain b) % 3.36/3.52 |- ~(codomain $_1 = codomain b) \/ ~(codomain b = codomain g) \/ % 3.36/3.52 compose (codomain $_1) (compose a b) = % 3.36/3.52 compose (compose (codomain $_1) (compose a b)) (codomain b) % 3.36/3.52 |- ~(codomain a = codomain b) \/ ~(codomain a = codomain g) \/ % 3.36/3.52 compose (compose g a) (compose a b) = % 3.36/3.52 compose (compose (compose g a) (compose a b)) (codomain a) % 3.36/3.52 |- ~(codomain a = codomain b) \/ ~(codomain a = codomain g) \/ % 3.36/3.52 compose (compose h a) (compose a b) = % 3.36/3.52 compose (compose (compose h a) (compose a b)) (codomain a) % 3.36/3.52 |- ~(codomain a = codomain b) \/ ~(codomain a = codomain g) \/ % 3.36/3.52 compose (codomain a) (compose a b) = % 3.36/3.52 compose (compose (codomain a) (compose a b)) (codomain a) % 3.36/3.52 |- ~(codomain $_796 = codomain g) \/ ~(codomain b = codomain $X) \/ % 3.36/3.52 compose (codomain $_796) (compose (compose a b) (codomain $X)) = % 3.36/3.52 compose (compose (codomain $_796) (compose a b)) (codomain $X) % 3.36/3.52 |- ~(codomain $X = domain g) \/ ~(domain $_800 = codomain $X) \/ % 3.36/3.52 compose (domain $_800) (compose (codomain $X) (compose g a)) = % 3.36/3.52 compose (compose (domain $_800) (codomain $X)) (compose g a) % 3.36/3.52 |- ~(domain $X = domain g) \/ ~(domain $_800 = domain $X) \/ % 3.36/3.52 compose (domain $_800) (compose (domain $X) (compose g a)) = % 3.36/3.52 compose (compose (domain $_800) (domain $X)) (compose g a) % 3.36/3.52 |- ~(codomain $_1 = codomain $_802) \/ ~(codomain $_802 = domain g) \/ % 3.36/3.52 compose (codomain $_1) (compose (codomain $_802) (compose g a)) = % 3.36/3.52 compose (compose (codomain $_1) (codomain $_802)) (compose g a) % 3.36/3.52 |- ~(codomain $X = domain g) \/ ~(domain $_806 = codomain $X) \/ % 3.36/3.52 compose (domain $_806) (compose (codomain $X) (compose h a)) = % 3.36/3.52 compose (compose (domain $_806) (codomain $X)) (compose h a) % 3.36/3.52 |- ~(domain $X = domain g) \/ ~(domain $_806 = domain $X) \/ % 3.36/3.52 compose (domain $_806) (compose (domain $X) (compose h a)) = % 3.36/3.52 compose (compose (domain $_806) (domain $X)) (compose h a) % 3.36/3.52 |- ~(codomain $_1 = codomain $_808) \/ ~(codomain $_808 = domain g) \/ % 3.36/3.52 compose (codomain $_1) (compose (codomain $_808) (compose h a)) = % 3.36/3.52 compose (compose (codomain $_1) (codomain $_808)) (compose h a) % 3.36/3.52 |- ~(codomain $_824 = domain g) \/ ~(codomain a = codomain $X) \/ % 3.36/3.52 compose (codomain $_824) (compose (compose g a) (codomain $X)) = % 3.36/3.52 compose (compose (codomain $_824) (compose g a)) (codomain $X) % 3.36/3.52 |- ~(codomain $_828 = domain g) \/ ~(codomain a = codomain $X) \/ % 3.36/3.52 compose (codomain $_828) (compose (compose h a) (codomain $X)) = % 3.36/3.52 compose (compose (codomain $_828) (compose h a)) (codomain $X) % 3.36/3.52 |- ~(domain $X = domain g) \/ ~(domain $_843 = domain $X) \/ % 3.36/3.52 compose (domain $_843) (compose (domain $X) h) = % 3.36/3.52 compose (compose (domain $_843) (domain $X)) h % 3.36/3.52 |- ~(codomain $_853 = domain $X) \/ ~(codomain b = codomain $_853) \/ % 3.36/3.52 compose (compose a b) (compose (codomain $_853) (domain $X)) = % 3.36/3.52 compose (compose (compose a b) (codomain $_853)) (domain $X) % 3.36/3.52 |- ~(codomain $X = domain g) \/ ~(domain $_859 = codomain $X) \/ % 3.36/3.52 compose (domain $_859) % 3.36/3.52 (compose (codomain $X) (compose g (compose a b))) = % 3.36/3.52 compose (compose (domain $_859) (codomain $X)) (compose g (compose a b)) % 3.36/3.52 |- ~(domain $X = domain g) \/ ~(domain $_859 = domain $X) \/ % 3.36/3.52 compose (domain $_859) (compose (domain $X) (compose g (compose a b))) = % 3.36/3.52 compose (compose (domain $_859) (domain $X)) (compose g (compose a b)) % 3.36/3.52 |- ~(codomain $_1 = domain $_863) \/ ~(domain $_863 = domain g) \/ % 3.36/3.52 compose (codomain $_1) % 3.36/3.52 (compose (domain $_863) (compose g (compose a b))) = % 3.36/3.52 compose (compose (codomain $_1) (domain $_863)) % 3.36/3.52 (compose g (compose a b)) % 3.36/3.52 |- ~(codomain $_1 = domain g) \/ ~(codomain b = codomain $_867) \/ % 3.36/3.52 compose (codomain $_1) % 3.36/3.52 (compose (compose g (compose a b)) (codomain $_867)) = % 3.36/3.52 compose (compose (codomain $_1) (compose g (compose a b))) % 3.36/3.52 (codomain $_867) % 3.36/3.52 |- ~(codomain b = codomain $X) \/ ~(domain $_871 = domain g) \/ % 3.36/3.52 compose (domain $_871) % 3.36/3.52 (compose (compose g (compose a b)) (codomain $X)) = % 3.36/3.52 compose (compose (domain $_871) (compose g (compose a b))) (codomain $X) % 3.36/3.52 |- ~(codomain a = codomain $_873) \/ ~(domain $X = domain g) \/ % 3.36/3.52 compose (domain $X) (compose (compose g a) (codomain $_873)) = % 3.36/3.52 compose (compose (domain $X) (compose g a)) (codomain $_873) % 3.36/3.52 |- ~(codomain a = codomain $_875) \/ ~(domain $X = domain g) \/ % 3.36/3.52 compose (domain $X) (compose (compose h a) (codomain $_875)) = % 3.36/3.52 compose (compose (domain $X) (compose h a)) (codomain $_875) % 3.36/3.52 |- ~(codomain $X = domain $_890) \/ ~(domain $_890 = domain g) \/ % 3.36/3.52 compose (codomain $X) (compose (domain $_890) (compose g a)) = % 3.36/3.52 compose (compose (codomain $X) (domain $_890)) (compose g a) % 3.36/3.52 |- ~(codomain $X = domain $_898) \/ ~(domain $_898 = domain g) \/ % 3.36/3.52 compose (codomain $X) (compose (domain $_898) (compose h a)) = % 3.36/3.52 compose (compose (codomain $X) (domain $_898)) (compose h a) % 3.36/3.52 |- ~(codomain $_1 = domain $_922) \/ ~(domain $_922 = domain $_921) \/ % 3.36/3.52 compose (codomain $_1) (compose (domain $_922) (domain $_921)) = % 3.36/3.52 compose (compose (codomain $_1) (domain $_922)) (domain $_921) % 3.36/3.52 |- ~(domain $X = domain $_922) \/ ~(domain $_922 = domain $_921) \/ % 3.36/3.52 compose (domain $X) (compose (domain $_922) (domain $_921)) = % 3.36/3.52 compose (compose (domain $X) (domain $_922)) (domain $_921) % 3.36/3.52 |- ~(domain $_933 = domain $_934) \/ ~(domain $_934 = codomain $X) \/ % 3.36/3.52 compose (domain $_933) (compose (domain $_934) (codomain $X)) = % 3.36/3.52 compose (compose (domain $_933) (domain $_934)) (codomain $X) % 3.36/3.52 |- ~(codomain $X = domain $_956) \/ ~(domain $_955 = codomain $X) \/ % 3.36/3.52 compose (domain $_955) (compose (codomain $X) (domain $_956)) = % 3.36/3.52 compose (compose (domain $_955) (codomain $X)) (domain $_956) % 3.36/3.52 |- ~(codomain $X = domain g) \/ ~(codomain $_972 = codomain $X) \/ % 3.36/3.52 compose (codomain $_972) % 3.36/3.52 (compose (codomain $X) (compose g (compose a b))) = % 3.36/3.52 compose (compose (codomain $_972) (codomain $X)) % 3.36/3.52 (compose g (compose a b)) % 3.36/3.52 |- ~(codomain $_1 = codomain $_1000) \/ % 3.36/3.52 ~(codomain $_1000 = codomain $_1001) \/ % 3.36/3.52 compose (codomain $_1) (compose (codomain $_1000) (codomain $_1001)) = % 3.36/3.52 compose (compose (codomain $_1) (codomain $_1000)) (codomain $_1001) % 3.36/3.52 |- ~(codomain $_1000 = codomain $_1001) \/ % 3.36/3.52 ~(domain $X = codomain $_1000) \/ % 3.36/3.52 compose (domain $X) (compose (codomain $_1000) (codomain $_1001)) = % 3.36/3.52 compose (compose (domain $X) (codomain $_1000)) (codomain $_1001) % 3.36/3.52 |- ~(codomain $_1003 = domain $X) \/ ~(domain $X = codomain $_1004) \/ % 3.36/3.52 compose (codomain $_1003) (compose (domain $X) (codomain $_1004)) = % 3.36/3.52 compose (compose (codomain $_1003) (domain $X)) (codomain $_1004) % 3.36/3.52 |- ~(codomain $_1006 = codomain $_1007) \/ % 3.36/3.52 ~(codomain $_1007 = domain $X) \/ % 3.36/3.52 compose (codomain $_1006) (compose (codomain $_1007) (domain $X)) = % 3.36/3.52 compose (compose (codomain $_1006) (codomain $_1007)) (domain $X) % 3.36/3.52 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.36/3.52 %------------------------------------------------------------------------------