Let x0 of type ι → ι → ο be given.

Assume H0: ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1.

Apply dneg with or (∃ x1 . and (x1 ⊆ u18) (and (atleastp u3 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3))) (∃ x1 . and (x1 ⊆ u18) (and (atleastp u6 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3)))).

Assume H1: not (or (∃ x1 . and (x1 ⊆ u18) (and (atleastp u3 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3))) (∃ x1 . and (x1 ⊆ u18) (and (atleastp u6 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))))).

Claim L2: ...

...

Claim L3: ...

...

Claim L4: ...

...

Apply unknownprop_75df131ad7dbf427f64e1622b3f5ffa653dd6b3f8ca1f519d1e92930050a1d43 with x0, 0, False leaving 5 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying L2.

The subproof is completed by applying L3.

The subproof is completed by applying L4.

Let x1 of type ι be given.

Assume H5: x1 ∈ DirGraphOutNeighbors u18 x0 0.

Let x2 of type ι be given.

Assume H6: x2 ⊆ u18.

Let x3 of type ι be given.

Assume H7: x3 ⊆ u18.

Let x4 of type ι be given.

Assume H8: x4 ⊆ u18.

Let x5 of type ι be given.

Assume H9: x5 ⊆ u18.

Assume H10: x2 = setminus (DirGraphOutNeighbors u18 x0 0) (Sing x1).

Assume H11: x4 = setminus (DirGraphOutNeighbors u18 x0 x1) (Sing 0).

Assume H12: x3 = {x6 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 0) (Sing 0))|equip (binintersect (DirGraphOutNeighbors u18 x0 x6) (DirGraphOutNeighbors u18 x0 0)) u1}.

Assume H13: x5 = setminus {x6 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 0) (Sing 0))|equip (binintersect (DirGraphOutNeighbors u18 x0 x6) (DirGraphOutNeighbors u18 x0 0)) u2} x4.

Let x6 of type ι be given.

Assume H14: x6 ∈ x3.

Let x7 of type ι be given.

Assume H15: x7 ∈ x3.

Let x8 of type ι be given.

Assume H16: x8 ∈ x3.

Let x9 of type ι be given.

Assume H17: x9 ∈ x3.

Assume H18: x0 x6 x7.

Assume H19: x0 x7 x8.

Assume H20: x0 x8 x9.

Assume H21: x0 x9 x6.

Assume H22: x7 = x6 ⟶ ∀ x10 : ο . x10.

Assume H23: x8 = x6 ⟶ ∀ x10 : ο . x10.

Assume H24: x9 = x6 ⟶ ∀ x10 : ο . x10.

Assume H25: x8 = x7 ⟶ ∀ x10 : ο . x10.

Assume H26: x9 = x7 ⟶ ∀ x10 : ο . x10.

Assume H27: ... ⟶ ∀ x10 : ο . x10.

...

■

Proofgold Proof