Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: ∃ x0 . ∃ x1 : ι → ι . ∃ x2 x3 x4 . ∃ x5 : ι → ι → ι → ι . MetaCat_nno_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x1 x2 x3 x4 x5.
Apply H0 with False.
Let x0 of type ι be given.
Assume H1: (λ x1 . ∃ x2 : ι → ι . ∃ x3 x4 x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x1 x2 x3 x4 x5 x6) x0.
Apply H1 with False.
Let x1 of type ι → ι be given.
Assume H2: (λ x2 : ι → ι . ∃ x3 x4 x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x2 x3 x4 x5 x6) x1.
Apply H2 with False.
Let x2 of type ι be given.
Assume H3: (λ x3 . ∃ x4 x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x1 x3 x4 x5 x6) x2.
Apply H3 with False.
Let x3 of type ι be given.
Assume H4: (λ x4 . ∃ x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x1 x2 x4 x5 x6) x3.
Apply H4 with False.
Let x4 of type ι be given.
Assume H5: (λ x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x1 x2 x3 x5 x6) x4.
Apply H5 with False.
Let x5 of type ι → ι → ι → ι be given.
Assume H6: MetaCat_nno_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x1 x2 x3 x4 x5.
Apply H6 with False.
Assume H7: and (and (and (MetaCat_terminal_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x1) (IrreflexiveTransitiveReln x2)) (BinRelnHom x0 x2 x3)) (BinRelnHom x2 x2 x4).
Apply H7 with (∀ x6 x7 x8 . IrreflexiveTransitiveReln x6 ⟶ BinRelnHom x0 x6 x7 ⟶ BinRelnHom x6 x6 x8 ⟶ and (and (and (BinRelnHom x2 x6 (x5 x6 x7 x8)) (struct_comp x0 x2 x6 (x5 x6 x7 x8) x3 = x7)) (struct_comp x2 x2 x6 (x5 x6 x7 x8) x4 = struct_comp x2 x6 x6 x8 (x5 x6 x7 x8))) (∀ x9 . BinRelnHom x2 x6 x9 ⟶ struct_comp x0 x2 x6 x9 x3 = x7 ⟶ struct_comp x2 x2 x6 x9 x4 = struct_comp x2 x6 x6 x8 x9 ⟶ x9 = x5 x6 x7 x8)) ⟶ False.
Assume H8: and (and (MetaCat_terminal_p IrreflexiveTransitiveReln BinRelnHom struct_id struct_comp x0 x1) (IrreflexiveTransitiveReln x2)) (BinRelnHom x0 x2 x3).
Apply H8 with ... ⟶ (∀ x6 x7 x8 . ... ⟶ ... ⟶ ... ⟶ and (and (and (BinRelnHom x2 x6 (x5 x6 x7 x8)) (struct_comp x0 x2 x6 (x5 x6 ... ...) ... = ...)) ...) ...) ⟶ False.
...
■