| 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.
Apply unknownprop_45d11dce2d0b092bd17c01d64c29c5885c90b43dc7cb762c6d6ada999ea508c5 with u3, DirGraphOutNeighbors u18 x0 x1, atleastp u4 (DirGraphOutNeighbors u18 x0 x1) leaving 3 subgoals.
The subproof is completed by applying nat_3.
Apply FalseE with atleastp u4 (DirGraphOutNeighbors u18 x0 x1).
Apply binunion_Subq_min with DirGraphOutNeighbors u18 x0 x1, Sing x1, u18 leaving 2 subgoals.
The subproof is completed by applying Sep_Subq with u18, λ x2 . and (x1 = x2 ⟶ ∀ x3 : ο . x3) (x0 x1 x2). Let x2 of type ι be given.
Apply SingE with x1, x2, λ x3 x4 . x4 ∈ u18 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H3.
Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with u17 leaving 2 subgoals.
The subproof is completed by applying nat_17.
Apply atleastp_tra with u18, setsum u13 u4, u17 leaving 2 subgoals.
Apply unknownprop_2ec38089a92dcd86a75a337a6e999322444786992f1b612acfe1d68011bad142 with u18, binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1), λ x2 x3 . atleastp x3 (setsum u13 u4) leaving 2 subgoals.
The subproof is completed by applying L5.
Apply unknownprop_8805a75f81012de0423e9173532fc074fb73b80e451597fde52287a4721fb204 with setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1)), binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1), u13, u4 leaving 2 subgoals.
Apply unknownprop_85506b6c69878f76c92de64599015cf7ee14b1d70236436d66a4fb9fd9f5e012 with x0, x1 leaving 4 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.
Apply atleastp_tra with binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1), setsum u3 u1, u4 leaving 2 subgoals.
Apply unknownprop_8805a75f81012de0423e9173532fc074fb73b80e451597fde52287a4721fb204 with DirGraphOutNeighbors u18 x0 x1, Sing x1, u3, u1 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply equip_atleastp with Sing x1, u1.
The subproof is completed by applying unknownprop_be1ab2772f2343e1b7afd526582f606d68258ba3f0b6521a351e0ecb8bf3c52e with x1.
Apply add_nat_0R with u3, λ x2 x3 . atleastp (setsum u3 u1) (ordsucc x2).
Apply add_nat_SR with u3, 0, λ x2 x3 . atleastp (setsum u3 u1) x2 leaving 2 subgoals.
The subproof is completed by applying nat_0.
Apply equip_atleastp with setsum u3 u1, add_nat u3 u1.
Apply equip_sym with add_nat u3 u1, setsum u3 u1.
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with u3, u1, u3, u1 leaving 4 subgoals.
The subproof is completed by applying nat_3.
The subproof is completed by applying nat_1.
The subproof is completed by applying equip_ref with u3. The subproof is completed by applying equip_ref with u1. Apply equip_atleastp with setsum u13 u4, u17.
Apply unknownprop_a826f2620b9c1761a765a32e5d5dcbc640507b9be837b9f7de8f5a679692e566 with λ x2 x3 . equip (setsum u13 u4) x2.
Apply equip_sym with add_nat u13 u4, setsum u13 u4.
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with u13, u4, u13, u4 leaving 4 subgoals.
The subproof is completed by applying nat_13.
The subproof is completed by applying nat_4.
The subproof is completed by applying equip_ref with u13. The subproof is completed by applying equip_ref with u4.
The subproof is completed by applying H4.
■ |
|