Search for blocks/addresses/...

Proofgold Asset

asset id
7d272e9036d1cd40f2cf00fad1ef76fefa071aee64d066116302dafb3a361d1a
asset hash
4a3c12857eba90724e46a3441610fb25d1842f8863e1106895c7eaa4f9fdba24
bday / block
31062
tx
493fb..
preasset
doc published by Pr4zB..
Param nat_pnat_p : ιο
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition bijbij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)) (∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)
Definition equipequip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3x2)x2
Param ordsuccordsucc : ιι
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Known 07015.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . nat_p x2equip x0 (ordsucc x2)∀ x3 . equip x3 x2∀ x4 : ι → ι . (∀ x5 . x5x3∀ x6 . x6x0x1 x6 x5x6 = x4 x5)(∀ x5 . x5x3∀ x6 . x6x3x4 x5 = x4 x6x5 = x6)∀ x5 : ο . (∀ x6 . and (x6x0) (∀ x7 . x7x3not (x1 x6 x7))x5)x5
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param atleastpatleastp : ιιο
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Param binintersectbinintersect : ιιι
Param SepSep : ι(ιο) → ι
Definition DirGraphOutNeighbors := λ x0 . λ x1 : ι → ι → ο . λ x2 . {x3 ∈ x0|and (x2 = x3∀ x4 : ο . x4) (x1 x2 x3)}
Param setminussetminus : ιιι
Param binunionbinunion : ιιι
Param SingSing : ιι
Known 05419.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)(∀ x2 . x2x0atleastp u3 x2not (∀ x3 . x3x2∀ x4 . x4x2(x3 = x4∀ x5 : ο . x5)x1 x3 x4))∀ x2 . nat_p x2(∀ x3 . x3x0∀ x4 . x4x0(x3 = x4∀ x5 : ο . x5)not (x1 x3 x4)or (equip (binintersect (DirGraphOutNeighbors x0 x1 x3) (DirGraphOutNeighbors x0 x1 x4)) x2) (equip (binintersect (DirGraphOutNeighbors x0 x1 x3) (DirGraphOutNeighbors x0 x1 x4)) (ordsucc x2)))∀ x3 x4 . x3x0x4DirGraphOutNeighbors x0 x1 x3(∀ x5 . x5{x6 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x6) (DirGraphOutNeighbors x0 x1 x3)) x2}not (x1 x4 x5))binunion (setminus (DirGraphOutNeighbors x0 x1 x4) (Sing x3)) (setminus {x6 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x6) (DirGraphOutNeighbors x0 x1 x3)) (ordsucc x2)} (setminus (DirGraphOutNeighbors x0 x1 x4) (Sing x3))) = {x6 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x6) (DirGraphOutNeighbors x0 x1 x3)) (ordsucc x2)}
Definition nInnIn := λ x0 x1 . not (x0x1)
Param add_natadd_nat : ιιι
Known 8bf56.. : ∀ x0 x1 x2 x3 x4 . binunion x0 x1 = x2(∀ x5 . x5x0nIn x5 x1)nat_p x3nat_p x4equip x0 x3equip x2 (add_nat x3 x4)equip x1 x4
Known f38da.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)∀ x2 . nat_p x2∀ x3 x4 . x3x0x4DirGraphOutNeighbors x0 x1 x3(∀ x5 . x5{x6 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x6) (DirGraphOutNeighbors x0 x1 x3)) x2}not (x1 x4 x5))∀ x5 : ι → ι . (∀ x6 . x6setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x4) (Sing x4))x5 x6binintersect (DirGraphOutNeighbors x0 x1 x6) (DirGraphOutNeighbors x0 x1 x4))∀ x6 . x6{x7 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x7) (DirGraphOutNeighbors x0 x1 x3)) x2}∀ x7 : ο . (∀ x8 . and (x8setminus (DirGraphOutNeighbors x0 x1 x4) (Sing x3)) (x1 x6 x8)x7)x7
Known c82b0.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)(∀ x2 . x2x0atleastp u3 x2not (∀ x3 . x3x2∀ x4 . x4x2(x3 = x4∀ x5 : ο . x5)x1 x3 x4))∀ x2 x3 . x2x0x3DirGraphOutNeighbors x0 x1 x2(x2 = x3∀ x4 : ο . x4)x1 x2 x3∀ x4 . x4setminus (DirGraphOutNeighbors x0 x1 x3) (Sing x2)not (x1 x2 x4)
Known 94e32.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)∀ x2 x3 . x2x0∀ x4 . nat_p x4(∀ x5 . x5x0(x5 = x2∀ x6 : ο . x6)not (x1 x5 x2)or (equip (binintersect (DirGraphOutNeighbors x0 x1 x5) (DirGraphOutNeighbors x0 x1 x2)) x4) (equip (binintersect (DirGraphOutNeighbors x0 x1 x5) (DirGraphOutNeighbors x0 x1 x2)) (ordsucc x4)))(∀ x5 . x5{x6 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x2) (Sing x2))|equip (binintersect (DirGraphOutNeighbors x0 x1 x6) (DirGraphOutNeighbors x0 x1 x2)) x4}not (x1 x3 x5))(∀ x5 . x5setminus (DirGraphOutNeighbors x0 x1 x3) (Sing x2)not (x1 x2 x5))∀ x5 . x5setminus (DirGraphOutNeighbors x0 x1 x3) (Sing x2)equip (binintersect (DirGraphOutNeighbors x0 x1 x5) (DirGraphOutNeighbors x0 x1 x2)) (ordsucc x4)
Definition 15fbd.. := λ x0 : ι → ι → ο . λ x1 . λ x2 : ι → ι . and (∀ x3 . x3x1x0 (x2 x3) (x2 (ordsucc x3))) (x0 (x2 x1) (x2 0))
Definition f1360.. := λ x0 : ι → ι → ο . λ x1 x2 . ∀ x3 : ο . (∀ x4 : ι → ι . and (bij (ordsucc x1) x2 x4) (15fbd.. x0 x1 x4)x3)x3
Definition u4 := ordsucc u3
Known 1f34f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)(∀ x2 . x2x0atleastp u3 x2not (∀ x3 . x3x2∀ x4 . x4x2(x3 = x4∀ x5 : ο . x5)x1 x3 x4))∀ x2 . x2x0equip x2 u4∀ x3 x4 : ι → ι . (∀ x5 . x5u4x3 x5x2)(∀ x5 . x5u4x4 x5x2)(∀ x5 . x5u4x3 x5 = x4 x5∀ x6 : ο . x6)(∀ x5 . x5u4x1 (x3 x5) (x4 x5))(∀ x5 . x5u4∀ x6 . x6u4x3 x5 = x3 x6x4 x5 = x4 x6x5 = x6)(∀ x5 . x5u4∀ x6 . x6u4x3 x5 = x4 x6x4 x5 = x3 x6x5 = x6)f1360.. x1 u3 x2
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition u17 := ordsucc u16
Definition u18 := ordsucc u17
Definition 4b3fa.. := λ x0 : ι → ι → ο . λ x1 x2 . prim0 (λ x3 . x3binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1))
Known 998ca.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 . x2setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))4b3fa.. x0 x1 x2binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)
Known 42af1.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 . x2{x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u1}4b3fa.. x0 x1 x2binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)
Known 80db2.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 . x2{x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u1}∀ x3 . x3DirGraphOutNeighbors u18 x0 x1x0 x3 x2x3 = 4b3fa.. x0 x1 x2
Known abdca.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 . x2{x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u1}∀ x3 . x3{x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1}4b3fa.. x0 x1 x2 = 4b3fa.. x0 x1 x3x2 = x3
Definition f14ce.. := λ x0 : ι → ι → ο . λ x1 x2 . prim0 (λ x3 . and (x3binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) (x3 = 4b3fa.. x0 x1 x2∀ x4 : ο . x4))
Known 0ddae.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 . x2{x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u2}and (f14ce.. x0 x1 x2binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) (f14ce.. x0 x1 x2 = 4b3fa.. x0 x1 x2∀ x3 : ο . x3)
Param invinv : ι(ιι) → ιι
Definition 31e20.. := λ x0 : ι → ι → ο . λ x1 . inv {x2 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) u1} (4b3fa.. x0 x1)
Known e1908.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 . x2DirGraphOutNeighbors u18 x0 x1∀ x3 . x3setminus (setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))) (DirGraphOutNeighbors u18 x0 x2)4b3fa.. x0 x1 x3setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x2)
Known 9fceb.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 . x2DirGraphOutNeighbors u18 x0 x1(∀ 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))∀ x3 . x3setminus {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2} (DirGraphOutNeighbors u18 x0 x2)31e20.. x0 x1 (4b3fa.. x0 x1 x3){x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1}
Known 23d19.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 . x2DirGraphOutNeighbors u18 x0 x1∀ x3 . x3setminus {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2} (DirGraphOutNeighbors u18 x0 x2)f14ce.. x0 x1 x3setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x2)
Known eb388.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 . x2DirGraphOutNeighbors u18 x0 x1(∀ 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))∀ x3 . x3setminus {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2} (DirGraphOutNeighbors u18 x0 x2)31e20.. x0 x1 (f14ce.. x0 x1 x3){x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1}
Known 82836.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 . x2DirGraphOutNeighbors u18 x0 x1(∀ 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))∀ x3 . x3setminus (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)
Known 68855.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 . x2DirGraphOutNeighbors u18 x0 x1(∀ 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))∀ x3 . x3setminus {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2} (DirGraphOutNeighbors u18 x0 x2)31e20.. x0 x1 (4b3fa.. x0 x1 x3) = 31e20.. x0 x1 (f14ce.. x0 x1 x3)∀ x4 : ο . x4
Known 8a908.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 . x2DirGraphOutNeighbors u18 x0 x1(∀ 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))∀ x3 . x3setminus {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2} (DirGraphOutNeighbors u18 x0 x2)x0 (31e20.. x0 x1 (4b3fa.. x0 x1 x3)) (31e20.. x0 x1 (f14ce.. x0 x1 x3))
Known 51de2.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18and (equip {x2 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) u1} u4) (equip {x2 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) u2} u8)
Known nat_4nat_4 : nat_p 4
Known b4538.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18equip (DirGraphOutNeighbors u18 x0 x1) u5
Known SepESepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1and (x2x0) (x1 x2)
Known equip_symequip_sym : ∀ x0 x1 . equip x0 x1equip x1 x0
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Known setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1x0
Known Sep_SubqSep_Subq : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1x0
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known setminusIsetminusI : ∀ x0 x1 x2 . x2x0nIn x2 x1x2setminus x0 x1
Known SingESingE : ∀ x0 x1 . x1Sing x0x1 = x0
Known 86f86.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 . x2u18(x1 = x2∀ x3 : ο . x3)not (x0 x1 x2)or (equip (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) u1) (equip (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) u2)
Known SepISepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0x1 x2x2Sep x0 x1
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known neq_i_symneq_i_sym : ∀ x0 x1 . (x0 = x1∀ x2 : ο . x2)x1 = x0∀ x2 : ο . x2
Known binunionEbinunionE : ∀ x0 x1 x2 . x2binunion x0 x1or (x2x0) (x2x1)
Known setminusE1setminusE1 : ∀ x0 x1 x2 . x2setminus x0 x1x2x0
Known 9c223..equip_ordsucc_remove1 : ∀ x0 x1 x2 . x2x0equip x0 (ordsucc x1)equip (setminus x0 (Sing x2)) x1
Known nat_1nat_1 : nat_p 1
Known b7308.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 . x2DirGraphOutNeighbors u18 x0 x1∀ x3 . x3DirGraphOutNeighbors u18 x0 x1(x2 = x3∀ x4 : ο . x4)∀ x4 . x4setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))∀ x5 . x5setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))x0 x4 x2x0 x5 x2x0 x4 x3x0 x5 x3x4 = x5
Known binintersectE2binintersectE2 : ∀ x0 x1 x2 . x2binintersect x0 x1x2x1
Known SepE2SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x1 x2
Known binintersectE1binintersectE1 : ∀ x0 x1 x2 . x2binintersect x0 x1x2x0
Known setminusEsetminusE : ∀ x0 x1 x2 . x2setminus x0 x1and (x2x0) (nIn x2 x1)
Known SepE1SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x2x0
Known setminusE2setminusE2 : ∀ x0 x1 x2 . x2setminus x0 x1nIn x2 x1
Known binunionI2binunionI2 : ∀ x0 x1 x2 . x2x1x2binunion x0 x1
Known 36602.. : add_nat 4 4 = 8
Known cfabd.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3DirGraphOutNeighbors x0 x1 x2x2DirGraphOutNeighbors x0 x1 x3
Theorem 52c6f.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 : ο . (∀ x3 . x3DirGraphOutNeighbors u18 x0 x1∀ x4 . x4u18∀ x5 . x5u18∀ x6 . x6u18∀ x7 . x7u18x4 = setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x3)x6 = setminus (DirGraphOutNeighbors u18 x0 x3) (Sing x1)x5 = {x9 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x9) (DirGraphOutNeighbors u18 x0 x1)) u1}x7 = setminus {x9 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x9) (DirGraphOutNeighbors u18 x0 x1)) u2} x6(∀ x8 . x8u18∀ x9 : ο . (x8 = x1x9)(x8 = x3x9)(x8x4x9)(x8x6x9)(x8x5x9)(x8x7x9)x9)(∀ x8 . x8x5not (x0 x3 x8))equip x4 u4equip x5 u4equip x6 u4equip x7 u4(∀ x8 . x8x6nIn x8 x7)(∀ x8 . x8x5∀ x9 : ο . (∀ x10 . and (x10x6) (x0 x8 x10)x9)x9)(∀ x8 . x8x6not (x0 x1 x8))(∀ x8 . x8x6equip (binintersect (DirGraphOutNeighbors u18 x0 x8) (DirGraphOutNeighbors u18 x0 x1)) u2)f1360.. x0 u3 x5x2)x2 (proof)
Param SetAdjoinSetAdjoin : ιιι
Param UPairUPair : ιιι
Known bijEbijE : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2∀ x3 : ο . ((∀ x4 . x4x0x2 x4x1)(∀ x4 . x4x0∀ x5 . x5x0x2 x4 = x2 x5x4 = x5)(∀ x4 . x4x1∀ x5 : ο . (∀ x6 . and (x6x0) (x2 x6 = x4)x5)x5)x3)x3
Known In_0_3In_0_3 : 03
Known In_2_3In_2_3 : 23
Param omegaomega : ι
Definition finitefinite := λ x0 . ∀ x1 : ο . (∀ x2 . and (x2omega) (equip x0 x2)x1)x1
Known 1b508.. : ∀ x0 x1 . finite x0atleastp x1 x0x0x1x0 = x1
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known 2c48a..atleastp_antisym_equip : ∀ x0 x1 . atleastp x0 x1atleastp x1 x0equip x0 x1
Known 38089.. : ∀ x0 x1 x2 x3 . atleastp (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) u4
Known atleastp_traatleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1atleastp x1 x2atleastp x0 x2
Known equip_atleastpequip_atleastp : ∀ x0 x1 . equip x0 x1atleastp x0 x1
Known 8698a.. : ∀ x0 x1 x2 x3 . ∀ x4 : ι → ο . x4 x0x4 x1x4 x2x4 x3∀ x5 . x5SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3x4 x5
Known 09d70.. : ∀ x0 x1 . x1x0∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0(x1 = x2∀ x5 : ο . x5)(x1 = x3∀ x5 : ο . x5)(x2 = x3∀ x5 : ο . x5)(x1 = x4∀ x5 : ο . x5)(x2 = x4∀ x5 : ο . x5)(x3 = x4∀ x5 : ο . x5)atleastp u4 x0
Known 69a9c.. : ∀ x0 x1 x2 x3 . x0SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3
Known e588e.. : ∀ x0 x1 x2 x3 . x1SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3
Known 14338.. : ∀ x0 x1 x2 x3 . x2SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3
Known b253c.. : ∀ x0 x1 x2 x3 . x3SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3
Known aa241.. : ∀ x0 x1 x2 . ∀ x3 : ι → ο . x3 x0x3 x1x3 x2∀ x4 . x4SetAdjoin (UPair x0 x1) x2x3 x4
Known 5d098.. : ∀ x0 x1 . x1x0∀ x2 . x2x0∀ x3 . x3x0(x1 = x2∀ x4 : ο . x4)(x1 = x3∀ x4 : ο . x4)(x2 = x3∀ x4 : ο . x4)atleastp u3 x0
Known 6be8c.. : ∀ x0 x1 x2 . x0SetAdjoin (UPair x0 x1) x2
Known 535ce.. : ∀ x0 x1 x2 . x1SetAdjoin (UPair x0 x1) x2
Known f4e2f.. : ∀ x0 x1 x2 . x2SetAdjoin (UPair x0 x1) x2
Known FalseEFalseE : False∀ x0 : ο . x0
Known neq_3_2neq_3_2 : u3 = u2∀ x0 : ο . x0
Known In_3_4In_3_4 : 34
Known In_2_4In_2_4 : 24
Known neq_3_1neq_3_1 : u3 = u1∀ x0 : ο . x0
Known In_1_4In_1_4 : 14
Known neq_3_0neq_3_0 : u3 = 0∀ x0 : ο . x0
Known In_0_4In_0_4 : 04
Known neq_2_1neq_2_1 : u2 = u1∀ x0 : ο . x0
Known neq_2_0neq_2_0 : u2 = 0∀ x0 : ο . x0
Known neq_1_0neq_1_0 : u1 = 0∀ x0 : ο . x0
Known In_1_3In_1_3 : 13
Theorem 8cad5.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 : ο . (∀ x3 . x3DirGraphOutNeighbors u18 x0 x1∀ x4 . x4u18∀ x5 . x5u18∀ x6 . x6u18∀ x7 . x7u18x4 = setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x3)x6 = setminus (DirGraphOutNeighbors u18 x0 x3) (Sing x1)x5 = {x9 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x9) (DirGraphOutNeighbors u18 x0 x1)) u1}x7 = setminus {x9 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x9) (DirGraphOutNeighbors u18 x0 x1)) u2} x6∀ x8 . x8x5∀ x9 . x9x5∀ x10 . x10x5∀ x11 . x11x5x0 x8 x9x0 x9 x10x0 x10 x11x0 x11 x8(x9 = x8∀ x12 : ο . x12)(x10 = x8∀ x12 : ο . x12)(x11 = x8∀ x12 : ο . x12)(x10 = x9∀ x12 : ο . x12)(x11 = x9∀ x12 : ο . x12)(x11 = x10∀ x12 : ο . x12)not (x0 x8 x10)not (x0 x9 x11)x5 = SetAdjoin (SetAdjoin (UPair x8 x9) x10) x11(∀ x12 . x12u18∀ x13 : ο . (x12 = x1x13)(x12 = x3x13)(x12x4x13)(x12x6x13)(x12x5x13)(x12x7x13)x13)(∀ x12 . x12x5not (x0 x3 x12))equip x4 u4equip x5 u4equip x6 u4equip x7 u4(∀ x12 . x12x6nIn x12 x7)(∀ x12 . x12x5∀ x13 : ο . (∀ x14 . and (x14x6) (x0 x12 x14)x13)x13)(∀ x12 . x12x6not (x0 x1 x12))(∀ x12 . x12x6equip (binintersect (DirGraphOutNeighbors u18 x0 x12) (DirGraphOutNeighbors u18 x0 x1)) u2)x2)x2 (proof)
Theorem 8cad5.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 : ο . (∀ x3 . x3DirGraphOutNeighbors u18 x0 x1∀ x4 . x4u18∀ x5 . x5u18∀ x6 . x6u18∀ x7 . x7u18x4 = setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x3)x6 = setminus (DirGraphOutNeighbors u18 x0 x3) (Sing x1)x5 = {x9 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x9) (DirGraphOutNeighbors u18 x0 x1)) u1}x7 = setminus {x9 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x9) (DirGraphOutNeighbors u18 x0 x1)) u2} x6∀ x8 . x8x5∀ x9 . x9x5∀ x10 . x10x5∀ x11 . x11x5x0 x8 x9x0 x9 x10x0 x10 x11x0 x11 x8(x9 = x8∀ x12 : ο . x12)(x10 = x8∀ x12 : ο . x12)(x11 = x8∀ x12 : ο . x12)(x10 = x9∀ x12 : ο . x12)(x11 = x9∀ x12 : ο . x12)(x11 = x10∀ x12 : ο . x12)not (x0 x8 x10)not (x0 x9 x11)x5 = SetAdjoin (SetAdjoin (UPair x8 x9) x10) x11(∀ x12 . x12u18∀ x13 : ο . (x12 = x1x13)(x12 = x3x13)(x12x4x13)(x12x6x13)(x12x5x13)(x12x7x13)x13)(∀ x12 . x12x5not (x0 x3 x12))equip x4 u4equip x5 u4equip x6 u4equip x7 u4(∀ x12 . x12x6nIn x12 x7)(∀ x12 . x12x5∀ x13 : ο . (∀ x14 . and (x14x6) (x0 x12 x14)x13)x13)(∀ x12 . x12x6not (x0 x1 x12))(∀ x12 . x12x6equip (binintersect (DirGraphOutNeighbors u18 x0 x12) (DirGraphOutNeighbors u18 x0 x1)) u2)x2)x2 (proof)
Known 782e4.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)(∀ x2 . x2x0atleastp u3 x2not (∀ x3 . x3x2∀ x4 . x4x2(x3 = x4∀ x5 : ο . x5)x1 x3 x4))∀ x2 . x2x0∀ x3 x4 x5 x6 . x2 = SetAdjoin (SetAdjoin (UPair x3 x4) x5) x6(x4 = x3∀ x7 : ο . x7)(x5 = x3∀ x7 : ο . x7)(x6 = x3∀ x7 : ο . x7)(x5 = x4∀ x7 : ο . x7)(x6 = x4∀ x7 : ο . x7)(x6 = x5∀ x7 : ο . x7)x1 x3 x4x1 x4 x5x1 x5 x6x1 x6 x3(∀ x7 . x7binintersect (DirGraphOutNeighbors x0 x1 x3) (DirGraphOutNeighbors x0 x1 x5)or (x7 = x4) (x7 = x6))(∀ x7 . x7binintersect (DirGraphOutNeighbors x0 x1 x4) (DirGraphOutNeighbors x0 x1 x6)or (x7 = x3) (x7 = x5))∀ x7 . x7x2∀ x8 . x8x2(x7 = x8∀ x9 : ο . x9)∀ x9 . x9binintersect (DirGraphOutNeighbors x0 x1 x7) (DirGraphOutNeighbors x0 x1 x8)x9x2
Known 02907.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)(∀ x2 . x2x0equip (DirGraphOutNeighbors x0 x1 x2) u5)∀ x2 x3 x4 x5 x6 x7 . x6x0x5x0x6 = {x9 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x2) (Sing x2))|equip (binintersect (DirGraphOutNeighbors x0 x1 x9) (DirGraphOutNeighbors x0 x1 x2)) u1}x4 = setminus (DirGraphOutNeighbors x0 x1 x2) (Sing x3)(∀ x8 . x8x6not (x1 x3 x8))(∀ x8 . x8x0∀ x9 : ο . (x8 = x2x9)(x8 = x3x9)(x8x4x9)(x8x5x9)(x8x6x9)(x8x7x9)x9)(∀ x8 . x8x6∀ x9 : ο . (∀ x10 . x10x6∀ x11 . x11x6(x10 = x11∀ x12 : ο . x12)x10DirGraphOutNeighbors x0 x1 x8x11DirGraphOutNeighbors x0 x1 x8not (x1 x10 x11)(∀ x12 . x12x6nIn x12 (SetAdjoin (UPair x8 x10) x11)not (x1 x8 x12))x9)x9)(∀ x8 . x8x6∀ x9 . x9x6(x8 = x9∀ x10 : ο . x10)∀ x10 . x10binintersect (DirGraphOutNeighbors x0 x1 x8) (DirGraphOutNeighbors x0 x1 x9)x10x6)(∀ x8 . x8x6nIn x8 x5)∀ x8 x9 : ι → ι . (∀ x10 . x10x6∀ x11 . x11DirGraphOutNeighbors x0 x1 x2x1 x11 x10x11 = x8 x10)(∀ x10 . x10x6x9 x10x5)(∀ x10 . x10x6x1 x10 (x9 x10))(∀ x10 . x10x5∀ x11 : ο . (∀ x12 . and (x12x6) (x9 x12 = x10)x11)x11)∀ x10 . x10x6∀ x11 : ο . (∀ x12 . and (x12x7) (x1 x10 x12)x11)x11
Known f0ba0.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)(∀ x2 . x2x0atleastp u3 x2not (∀ x3 . x3x2∀ x4 . x4x2(x3 = x4∀ x5 : ο . x5)x1 x3 x4))(∀ x2 . x2x0∀ x3 . x3x0(x2 = x3∀ x4 : ο . x4)not (x1 x2 x3)atleastp (binintersect (DirGraphOutNeighbors x0 x1 x2) (DirGraphOutNeighbors x0 x1 x3)) u2)∀ x2 x3 x4 x5 . x2x0x3x0x4x0x5x0(∀ x6 . x6x4nIn x6 x2)(∀ x6 . x6x4nIn x6 x3)(∀ x6 . x6x4nIn x6 x5)(∀ x6 . x6x2nIn x6 x3)(∀ x6 . x6x2nIn x6 x5)(∀ x6 . x6x3nIn x6 x5)∀ x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x6x4x7x4x3 = SetAdjoin (SetAdjoin (UPair x10 x11) x12) x13x14x2x15x5(x6 = x7∀ x16 : ο . x16)x1 x6 x7x1 x6 x10x1 x6 x15x1 x7 x14x1 x7 x11x1 x12 x15not (x1 x14 x6)x1 x14 x15x1 x13 x15∀ x16 . x16x3not (x1 x14 x16)
Known edcee.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)(∀ x2 . x2x0atleastp u3 x2not (∀ x3 . x3x2∀ x4 . x4x2(x3 = x4∀ x5 : ο . x5)x1 x3 x4))∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . x9x0x11x0x8 = setminus (DirGraphOutNeighbors x0 x1 x4) (Sing x5)x10 = setminus (DirGraphOutNeighbors x0 x1 x5) (Sing x4)x9 = {x13 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x4) (Sing x4))|equip (binintersect (DirGraphOutNeighbors x0 x1 x13) (DirGraphOutNeighbors x0 x1 x4)) x2}x11 = setminus {x13 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x4) (Sing x4))|equip (binintersect (DirGraphOutNeighbors x0 x1 x13) (DirGraphOutNeighbors x0 x1 x4)) x3} x10(∀ x12 . x12x9nIn x12 x8)(∀ x12 . x12x9nIn x12 x11)(∀ x12 . x12x8nIn x12 x11)x6x9x7x11x1 x6 x7∀ x12 x13 : ι → ι . x1 x6 (x12 x6)(∀ x14 . x14x8x13 x14{x15 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x4) (Sing x4))|equip (binintersect (DirGraphOutNeighbors x0 x1 x15) (DirGraphOutNeighbors x0 x1 x4)) x2})(∀ x14 . x14x8x12 (x13 x14) = x14)atleastp x3 {x14 ∈ setminus x9 (Sing x6)|x1 (x12 x14) x7}
Known 9a487.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)∀ x2 x3 . nat_p x2∀ x4 x5 . x5DirGraphOutNeighbors x0 x1 x4∀ x6 x7 x8 . x6x0x7x0x8x0x7 = setminus (DirGraphOutNeighbors x0 x1 x5) (Sing x4)x8 = setminus {x10 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x4) (Sing x4))|equip (binintersect (DirGraphOutNeighbors x0 x1 x10) (DirGraphOutNeighbors x0 x1 x4)) x3} x7equip x6 x2(∀ x9 . x9x6x9 = x5∀ x10 : ο . x10)(∀ x9 . x9x6nIn x9 x7)(∀ x9 . x9x6nIn x9 x8)(∀ x9 . x9x6nIn x9 (DirGraphOutNeighbors x0 x1 x4))(∀ x9 . x9x6nIn x9 (DirGraphOutNeighbors x0 x1 x5))(∀ x9 . x9x6∀ x10 . x10x6(x9 = x10∀ x11 : ο . x11)∀ x11 . x11binintersect (DirGraphOutNeighbors x0 x1 x9) (DirGraphOutNeighbors x0 x1 x10)x11x6)∀ x9 : ι → ι . (∀ x10 . x10x6x9 x10x7)(∀ x10 . x10x6x1 x10 (x9 x10))(∀ x10 . x10x7∀ x11 : ο . (∀ x12 . and (x12x6) (x9 x12 = x10)x11)x11)(∀ x10 . x10x8or (equip (binintersect (DirGraphOutNeighbors x0 x1 x10) (DirGraphOutNeighbors x0 x1 x5)) u1) (equip (binintersect (DirGraphOutNeighbors x0 x1 x10) (DirGraphOutNeighbors x0 x1 x5)) x3))equip {x10 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x5) (Sing x5))|equip (binintersect (DirGraphOutNeighbors x0 x1 x10) (DirGraphOutNeighbors x0 x1 x5)) u1} x2x8{x10 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x5) (Sing x5))|equip (binintersect (DirGraphOutNeighbors x0 x1 x10) (DirGraphOutNeighbors x0 x1 x5)) x3}
Known 0bee3.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)(∀ x2 . x2x0atleastp u3 x2not (∀ x3 . x3x2∀ x4 . x4x2(x3 = x4∀ x5 : ο . x5)x1 x3 x4))∀ x2 x3 x4 . nat_p x4∀ x5 x6 x7 . x5x0x6x0x7x0x5 = setminus (DirGraphOutNeighbors x0 x1 x3) (Sing x2)(∀ x8 . x8x6nIn x8 x5)(∀ x8 . x8x6nIn x8 x7)(∀ x8 . x8x5nIn x8 x7)(∀ x8 . x8x7x8{x9 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x9) (DirGraphOutNeighbors x0 x1 x3)) x4})∀ x8 x9 . x8x6x9x7x9setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x2) (Sing x2))x1 x8 x9∀ x10 : ι → ι . (∀ x11 . x11x6x10 x11x5)(∀ x11 . x11x6x1 x11 (x10 x11))(∀ x11 . x11x5∀ x12 : ο . (∀ x13 . and (x13x6) (x10 x13 = x11)x12)x12)atleastp x4 {x11 ∈ setminus x6 (Sing x8)|x1 (x10 x11) x9}
Known 3eb85.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)∀ x2 x3 x4 x5 . x2x0x3x0x4x0x5x0(∀ x6 . x6x2nIn x6 x5)(∀ x6 . x6x2nIn x6 x3)(∀ x6 . x6x4nIn x6 x2)(∀ x6 . x6x4nIn x6 x3)(∀ x6 . x6x4nIn x6 x5)(∀ x6 . x6x3nIn x6 x5)∀ x6 x7 x8 x9 x10 . x4 = SetAdjoin (SetAdjoin (UPair x6 x7) x8) x9x10x5(∀ x11 . x11x4(x11 = x10∀ x12 : ο . x12)not (x1 x11 x10)atleastp (binintersect (DirGraphOutNeighbors x0 x1 x11) (DirGraphOutNeighbors x0 x1 x10)) u2)x6binintersect (DirGraphOutNeighbors x0 x1 x7) (DirGraphOutNeighbors x0 x1 x10)x6binintersect (DirGraphOutNeighbors x0 x1 x9) (DirGraphOutNeighbors x0 x1 x10)not (x1 x7 x10)not (x1 x9 x10)∀ x11 x12 : ι → ι . (∀ x13 . x13x4x11 x13x2)(∀ x13 . x13x4x11 x13DirGraphOutNeighbors x0 x1 x13)(∀ x13 . x13x4x12 x13x3)(∀ x13 . x13x4x12 x13DirGraphOutNeighbors x0 x1 x13)∀ x13 . x13x4x13{x14 ∈ setminus x4 (Sing x6)|x1 (x11 x14) x10}x13{x14 ∈ setminus x4 (Sing x6)|x1 (x12 x14) x10}x13 = x8
Theorem 38ba8.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 . x8x4∀ x9 : ο . (x8x0x8DirGraphOutNeighbors x0 x1 x3(x3 = x8∀ x10 : ο . x10)x1 x3 x8(x8 = x2∀ x10 : ο . x10)x9)x9)(∀ x8 : ο . (∀ x9 . and (x9x4) (x1 x5 x9)x8)x8)(x1 x5 x6x1 x7 x6∀ x8 . x8x4not (x1 x5 x8))x1 x5 x6x1 x7 x6False (proof)
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Known 4fb58..Pigeonhole_not_atleastp_ordsucc : ∀ x0 . nat_p x0not (atleastp (ordsucc x0) x0)
Known nat_3nat_3 : nat_p 3
Known 256ca.. : add_nat 2 2 = 4
Param setsumsetsum : ιιι
Known c88e0.. : ∀ x0 x1 x2 x3 . nat_p x0nat_p x1equip x0 x2equip x1 x3equip (add_nat x0 x1) (setsum x2 x3)
Known nat_2nat_2 : nat_p 2
Known equip_refequip_ref : ∀ x0 . equip x0 x0
Known 1fe14.. : ∀ x0 x1 x2 x3 . atleastp x0 x2atleastp x1 x3(∀ x4 . x4x2nIn x4 x3)atleastp (setsum x0 x1) (binunion x2 x3)
Known Subq_atleastpSubq_atleastp : ∀ x0 x1 . x0x1atleastp x0 x1
Known binunion_Subq_minbinunion_Subq_min : ∀ x0 x1 x2 . x0x2x1x2binunion x0 x1x2
Theorem fe2f1.. : ∀ x0 . atleastp x0 u3∀ x1 . x1x0∀ x2 . x2x0atleastp u2 x1atleastp u2 x2∀ x3 : ο . (∀ x4 . and (x4x1) (x4x2)x3)x3 (proof)
Known 1aece.. : ∀ x0 x1 x2 x3 x4 . x4SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3∀ x5 : ι → ο . x5 x0x5 x1x5 x2x5 x3x5 x4
Known UPairI1UPairI1 : ∀ x0 x1 . x0UPair x0 x1
Known UPairI2UPairI2 : ∀ x0 x1 . x1UPair x0 x1
Theorem 71076.. : ∀ x0 x1 x2 x3 . setminus (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) (UPair x0 x2)UPair x1 x3 (proof)
Definition TwoRamseyProp_atleastp := λ x0 x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x3 x4 x5x3 x5 x4)or (∀ x4 : ο . (∀ x5 . and (x5x2) (and (atleastp x0 x5) (∀ x6 . x6x5∀ x7 . x7x5(x6 = x7∀ x8 : ο . x8)x3 x6 x7))x4)x4) (∀ x4 : ο . (∀ x5 . and (x5x2) (and (atleastp x1 x5) (∀ x6 . x6x5∀ x7 . x7x5(x6 = x7∀ x8 : ο . x8)not (x3 x6 x7)))x4)x4)
Known Eps_i_exEps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2x1)x1)x0 (prim0 x0)
Known 7f437.. : ∀ x0 x1 x2 . x2x0atleastp x0 (ordsucc x1)atleastp (setminus x0 (Sing x2)) x1
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Known binintersectEbinintersectE : ∀ x0 x1 x2 . x2binintersect x0 x1and (x2x0) (x2x1)
Known binintersectIbinintersectI : ∀ x0 x1 x2 . x2x0x2x1x2binintersect x0 x1
Known 4f2c3.. : ∀ x0 . atleastp (Sing x0) u1
Known e8716.. : ∀ x0 . atleastp u2 x0∀ x1 : ο . (∀ x2 . x2x0∀ x3 . x3x0(x2 = x3∀ x4 : ο . x4)x1)x1
Known UPairEUPairE : ∀ x0 x1 x2 . x0UPair x1 x2or (x0 = x1) (x0 = x2)
Known SingISingI : ∀ x0 . x0Sing x0
Known 2b310.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 . x2u18(x1 = x2∀ x3 : ο . x3)not (x0 x1 x2)atleastp (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) u2
Definition injinj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)
Known 77ee8.. : ∀ x0 x1 x2 . ∀ x3 : ι → ι . nat_p x0equip x1 x0equip x2 x0inj x1 x2 x3bij x1 x2 x3
Known binunionI1binunionI1 : ∀ x0 x1 x2 . x2x0x2binunion x0 x1
Known equip_traequip_tra : ∀ x0 x1 x2 . equip x0 x1equip x1 x2equip x0 x2
Known 7fc90.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)(∀ x2 . x2x0atleastp u3 x2not (∀ x3 . x3x2∀ x4 . x4x2(x3 = x4∀ x5 : ο . x5)x1 x3 x4))∀ x2 . x2x0∀ x3 . x3DirGraphOutNeighbors x0 x1 x2∀ x4 . x4DirGraphOutNeighbors x0 x1 x2(x3 = x4∀ x5 : ο . x5)not (x1 x3 x4)
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Known nat_0_in_ordsuccnat_0_in_ordsucc : ∀ x0 . nat_p x00ordsucc x0
Known nat_17nat_17 : nat_p 17
Theorem d777e.. : TwoRamseyProp_atleastp u3 u6 u18 (proof)
Param TwoRamseyPropTwoRamseyProp : ιιιο
Known b8b19.. : ∀ x0 x1 x2 . TwoRamseyProp_atleastp x0 x1 x2TwoRamseyProp x0 x1 x2
Theorem TwoRamseyProp_3_6_18TwoRamseyProp_3_6_18 : TwoRamseyProp u3 u6 u18 (proof)
Theorem TwoRamseyProp_3_6_18TwoRamseyProp_3_6_18 : TwoRamseyProp 3 6 18 (proof)