Proofgold Proof

pf

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

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

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

Assume H2: ∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3)).

Let x1 of type ι be given.

Assume H3: x1 ∈ u18.

Let x2 of type ι be given.

Assume H4: x2 ∈ DirGraphOutNeighbors u18 x0 x1.

Assume H5: ∀ x3 . x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ not (x0 x2 x3).

Apply unknownprop_19c5bea28ef119e30d80f4e7c578df826b34bc3d0b15978a12c7c1b896ec3046 with {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u1}, ∀ x3 . x3 ∈ setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x2) ⟶ and (and (31e20.. x0 x1 x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1}) (binintersect (DirGraphOutNeighbors u18 x0 (31e20.. x0 x1 x3)) (DirGraphOutNeighbors u18 x0 x1) = Sing x3)) (4b3fa.. x0 x1 (31e20.. x0 x1 x3) = x3) leaving 2 subgoals.

Apply equip_atleastp with u4, {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u1}.

Apply equip_sym with {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u1}, u4.

Apply unknownprop_4fbe2821a224e8efa7f1f4b4d0cd1ce84da1c8c58e8885ed9a4c21b8062b6ee1 with x0, x1, equip {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u1} u4 leaving 5 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

The subproof is completed by applying H3.

Assume H6: equip {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip ... ...} ....

...

...

■