Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrCit../a7958..
PUW9A../f52d8..
vout
PrCit../fc231.. 3.70 bars
TMHYG../09694.. ownership of 1af34.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMS3A../20032.. ownership of f0e24.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMQce../fe88c.. ownership of e3c64.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUyW../9665d.. ownership of c8499.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMc7Z../36d9f.. ownership of 2c467.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMVXV../d0235.. ownership of 7c587.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMMcN../146d6.. ownership of f0c7f.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMNV1../85c3e.. ownership of 50143.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMKom../7d8cb.. ownership of 41efe.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMHfi../d17e0.. ownership of 71785.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMSex../712ff.. ownership of f957b.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMaMo../3dca9.. ownership of cbd9d.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMKG8../40dbf.. ownership of 0c032.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMXWZ../a11ba.. ownership of 5f291.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMaCM../29461.. ownership of 86574.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRuo../25b5e.. ownership of c6ead.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUUa../5e5ef.. ownership of f6130.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMcm6../55e51.. ownership of 584fb.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMVQs../ef22c.. ownership of d804d.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMXwx../f928e.. ownership of 3a3a7.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMaUq../e8635.. ownership of 5d146.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMQ2V../2cfd6.. ownership of d4cc0.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMHTs../d97b3.. ownership of c8c81.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMX8S../0b06a.. ownership of 1ac22.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMY8Y../e3a40.. ownership of 7cfa7.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMGoo../551fb.. ownership of db5c9.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMQb7../91105.. ownership of 91090.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUwD../6c76d.. ownership of 57d44.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRQS../e1c93.. ownership of 01a24.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMHZp../0db94.. ownership of b8a8e.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMJVM../aaa2a.. ownership of e6ce7.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMK26../71f48.. ownership of 6b3b9.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMNKy../cfdd4.. ownership of 412d7.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMWZF../f6db6.. ownership of 5bd54.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMJ4n../73377.. ownership of 3236d.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMLXf../88235.. ownership of ffc15.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMc9M../83b8e.. ownership of bfe59.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMdvH../44aeb.. ownership of 87c96.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TML4k../1af62.. ownership of 66a94.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMKsF../1b26f.. ownership of 0324a.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMTdx../0b70b.. ownership of 7a154.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMQoW../e678f.. ownership of fd2d2.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMZj4../02f36.. ownership of c03d6.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMSzK../e6436.. ownership of 291cb.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRDs../538bd.. ownership of 59a5e.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMR6J../fc56d.. ownership of cd025.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMbe3../16e1a.. ownership of 04dd3.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUgL../39ac8.. ownership of 024c0.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUYg../013cc.. ownership of eaeac.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMK2a../f4c8a.. ownership of 9ff34.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMJdR../50ed2.. ownership of a1082.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMGSr../f6e4e.. ownership of 19b95.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRxN../008e6.. ownership of 33ada.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMVZU../b341c.. ownership of 36345.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMGMg../7d404.. ownership of fe03b.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMGmH../0610c.. ownership of 32d31.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMd6P../9912a.. ownership of 03b78.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMTyR../896ca.. ownership of 9efcf.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMGrj../9ff83.. ownership of 9c958.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMZHb../76d36.. ownership of 38936.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMFHW../59fc5.. ownership of 6ab71.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMW9T../5f79c.. ownership of efe93.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMNgh../2bbfd.. ownership of be264.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMQkg../47d4e.. ownership of b8c53.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUXJ../e7306.. ownership of da9f0.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMdWe../ca79b.. ownership of 859ff.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMdVr../1a1c3.. ownership of 764ed.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMMUE../97e62.. ownership of f1501.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMK66../2cc7e.. ownership of 51a01.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMJhG../53d2d.. ownership of 655fa.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMXJP../87e0d.. ownership of e7d99.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMdtV../239cf.. ownership of 89cfb.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMEz8../6b0ca.. ownership of d257b.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMWF2../3f1b2.. ownership of 2b565.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMZtf../6b93b.. ownership of d7596.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMGeR../a4bbd.. ownership of 59b1a.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMSEw../89769.. ownership of a10f1.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMFfV../0943a.. ownership of b6a97.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMXCn../11e05.. ownership of 53a3c.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMTak../bbfb7.. ownership of 8777e.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRz8../cf36c.. ownership of e7c7c.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMJbE../f2fa4.. ownership of 304cf.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMKwi../826a3.. ownership of 860e7.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMHCo../85dbf.. ownership of 60efe.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMP1V../1a17f.. ownership of 61345.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMbjH../e02a3.. ownership of d5004.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMatV../85c83.. ownership of a55d1.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMctU../a3c95.. ownership of d3460.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMH9P../e835e.. ownership of 2fbe3.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMWxA../28729.. ownership of e8529.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUCJ../89a99.. ownership of 3ebe5.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMVdF../cfaf5.. ownership of ada8e.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRDA../b1e40.. ownership of 4aec2.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMSwQ../50606.. ownership of 9781d.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUSh../3b270.. ownership of 7204a.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMLNE../75505.. ownership of 1284c.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMZKp../671c2.. ownership of e2ea8.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMbbQ../773cb.. ownership of 5af27.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRvS../e15d7.. ownership of 80df3.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMFqc../ec57c.. ownership of 62c2f.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMLQe../84713.. ownership of 2b028.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMFmp../80265.. ownership of 35aca.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMP4b../8620a.. ownership of c5756.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMLCK../2fd8b.. ownership of d3fe5.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMdpM../28c29.. ownership of 42d13.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMKMP../305c3.. ownership of 0fe30.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMYkJ../9f1e4.. ownership of 87c36.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMGLd../dd522.. ownership of ba9a8.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMJud../37e06.. ownership of 62523.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMdgp../f4acd.. ownership of ddc05.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMNEi../12dc5.. ownership of 58403.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMY9x../af593.. ownership of c20bc.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMb1o../e7068.. ownership of 22dda.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMHsG../ef2a1.. ownership of 7350b.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMZjU../436c8.. ownership of 45422.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMPh3../ac010.. ownership of 7290e.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMNBQ../d49ff.. ownership of 0ee5a.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRXm../c11e1.. ownership of 2b471.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMXJS../f887d.. ownership of 32385.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMHzo../c5e74.. ownership of 4e417.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMa7i../0cf1a.. ownership of 6ff44.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMREa../ab1a9.. ownership of d1f16.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMdhC../577dc.. ownership of 5a3b5.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMTqE../0a330.. ownership of 87507.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMdhz../14e27.. ownership of 9b945.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMX6r../280eb.. ownership of d19d8.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMFP1../a57e9.. ownership of 180f5.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMS25../98dd7.. ownership of 1e298.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMJwo../41e8f.. ownership of a1d37.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMXvj../d3d87.. ownership of b4590.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMKqb../938aa.. ownership of 2f869.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMNPA../45a1e.. ownership of ab229.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMNL5../462d8.. ownership of 65a4c.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMG6a../eff40.. ownership of 6cab1.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMJaG../904ed.. ownership of 91306.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUi9../c441d.. ownership of 0979e.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMMbp../c617a.. ownership of 8b6ad.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMS3K../79b9b.. ownership of fb86d.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMcnK../d1c57.. ownership of cf2df.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMR1B../d0dcb.. ownership of b5c03.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMNWZ../9503f.. ownership of 2bc70.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMGYT../02890.. ownership of 96af8.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMW5M../26422.. ownership of 4402e.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMPQs../deb34.. ownership of a26d1.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMR7E../0bd86.. ownership of cdfa5.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMbDq../81bb4.. ownership of 3013d.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
PUTgE../d8766.. doc published by Pr4zB..
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition injinj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Definition atleastpatleastp := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3 ⟶ x2) ⟶ x2
Param ordsuccordsucc : ι → ι
Param setminussetminus : ι → ι → ι
Param SingSing : ι → ι
Known andIandI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known ordsuccI2ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Definition nInnIn := λ x0 x1 . not (x0 ∈ x1)
Known setminusIsetminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known ordsuccI1ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Known SingESingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Theorem e2ea8.. : ∀ x0 x1 . atleastp (ordsucc x0) x1 ⟶ ∀ x2 : ο . (∀ x3 . and (x3 ∈ x1) (atleastp x0 (setminus x1 (Sing x3))) ⟶ x2) ⟶ x2 (proof)
Param equipequip : ι → ι → ο
Param u3 : ι
Definition u4 := ordsucc u3
Param binunionbinunion : ι → ι → ι
Definition SetAdjoinSetAdjoin := λ x0 x1 . binunion x0 (Sing x1)
Param UPairUPair : ι → ι → ι
Known e8bc0..equip_adjoin_ordsucc : ∀ x0 x1 x2 . nIn x2 x1 ⟶ equip x0 x1 ⟶ equip (ordsucc x0) (binunion x1 (Sing x2))
Known aa241.. : ∀ x0 x1 x2 . ∀ x3 : ι → ο . x3 x0 ⟶ x3 x1 ⟶ x3 x2 ⟶ ∀ x4 . x4 ∈ SetAdjoin (UPair x0 x1) x2 ⟶ x3 x4
Known b2ff4.. : ∀ x0 x1 x2 . (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ equip u3 (SetAdjoin (UPair x0 x1) x2)
Theorem 7204a.. : ∀ x0 x1 x2 x3 . (x0 = x1 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ equip u4 (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) (proof)
Definition u5 := ordsucc u4
Known 8698a.. : ∀ x0 x1 x2 x3 . ∀ x4 : ι → ο . x4 x0 ⟶ x4 x1 ⟶ x4 x2 ⟶ x4 x3 ⟶ ∀ x5 . x5 ∈ SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3 ⟶ x4 x5
Theorem 4aec2.. : ∀ x0 x1 x2 x3 x4 . (x0 = x1 ⟶ ∀ x5 : ο . x5) ⟶ (x0 = x2 ⟶ ∀ x5 : ο . x5) ⟶ (x1 = x2 ⟶ ∀ x5 : ο . x5) ⟶ (x0 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x1 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x2 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x0 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x1 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x2 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ equip u5 (SetAdjoin (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) x4) (proof)
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Theorem 3ebe5.. : ∀ x0 x1 . ∀ x2 : ι → ο . x0 ⊆ x1 ⟶ (∀ x3 . x3 ⊆ x1 ⟶ x2 x3) ⟶ ∀ x3 . x3 ⊆ x0 ⟶ x2 x3 (proof)
Definition cdfa5.. := λ x0 x1 . λ x2 : ι → ι → ο . ∀ x3 . x3 ⊆ x1 ⟶ atleastp x0 x3 ⟶ not (∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ x2 x4 x5)
Theorem 2fbe3.. : ∀ x0 x1 x2 . ∀ x3 : ι → ι → ο . x1 ⊆ x2 ⟶ cdfa5.. x0 x2 x3 ⟶ cdfa5.. x0 x1 x3 (proof)
Definition 4402e.. := cdfa5.. u3
Theorem a55d1.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . x0 ⊆ x1 ⟶ 4402e.. x1 x2 ⟶ 4402e.. x0 x2 (proof)
Known equip_atleastpequip_atleastp : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Known FalseEFalseE : False ⟶ ∀ x0 : ο . x0
Theorem 61345.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x2 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x2 x3 ⟶ x1 x2 x4 ⟶ x1 x3 x4 ⟶ False (proof)
Definition 2bc70.. := cdfa5.. u5
Known 9b26d.. : ∀ x0 x1 x2 x3 x4 . ∀ x5 : ι → ο . x5 x0 ⟶ x5 x1 ⟶ x5 x2 ⟶ x5 x3 ⟶ x5 x4 ⟶ ∀ x6 . x6 ∈ SetAdjoin (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) x4 ⟶ x5 x6
Theorem 860e7.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 2bc70.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x4 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x4 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x5 = x6 ⟶ ∀ x7 : ο . x7) ⟶ x1 x2 x3 ⟶ x1 x2 x4 ⟶ x1 x3 x4 ⟶ x1 x2 x5 ⟶ x1 x3 x5 ⟶ x1 x4 x5 ⟶ x1 x2 x6 ⟶ x1 x3 x6 ⟶ x1 x4 x6 ⟶ x1 x5 x6 ⟶ False (proof)
Definition cf2df.. := λ x0 . λ x1 : ι → ι → ο . 2bc70.. x0 (λ x2 x3 . not (x1 x2 x3))
Theorem e7c7c.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . x0 ⊆ x1 ⟶ cf2df.. x1 x2 ⟶ cf2df.. x0 x2 (proof)
Theorem 53a3c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ not (x1 x2 x3) ⟶ not (x1 x3 x2)) ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x4 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x4 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x5 = x6 ⟶ ∀ x7 : ο . x7) ⟶ not (x1 x2 x3) ⟶ not (x1 x2 x4) ⟶ not (x1 x3 x4) ⟶ not (x1 x2 x5) ⟶ not (x1 x3 x5) ⟶ not (x1 x4 x5) ⟶ not (x1 x2 x6) ⟶ not (x1 x3 x6) ⟶ not (x1 x4 x6) ⟶ not (x1 x5 x6) ⟶ False (proof)
Definition 8b6ad.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 . ∀ x5 : ο . ((x1 = x2 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ not (x0 x1 x2) ⟶ not (x0 x1 x3) ⟶ not (x0 x2 x3) ⟶ not (x0 x1 x4) ⟶ not (x0 x2 x4) ⟶ not (x0 x3 x4) ⟶ x5) ⟶ x5
Definition 91306.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 . ∀ x5 : ο . ((x1 = x2 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ not (x0 x1 x2) ⟶ not (x0 x1 x3) ⟶ x0 x2 x3 ⟶ x0 x1 x4 ⟶ not (x0 x2 x4) ⟶ not (x0 x3 x4) ⟶ x5) ⟶ x5
Definition 65a4c.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 . ∀ x5 : ο . ((x1 = x2 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ not (x0 x1 x2) ⟶ x0 x1 x3 ⟶ x0 x2 x3 ⟶ x0 x1 x4 ⟶ x0 x2 x4 ⟶ not (x0 x3 x4) ⟶ x5) ⟶ x5
Definition 2f869.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 . ∀ x5 : ο . ((x1 = x2 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ not (x0 x1 x2) ⟶ not (x0 x1 x3) ⟶ not (x0 x2 x3) ⟶ not (x0 x1 x4) ⟶ not (x0 x2 x4) ⟶ x0 x3 x4 ⟶ x5) ⟶ x5
Definition a1d37.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 . ∀ x5 : ο . ((x1 = x2 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ not (x0 x1 x2) ⟶ not (x0 x1 x3) ⟶ x0 x2 x3 ⟶ x0 x1 x4 ⟶ not (x0 x2 x4) ⟶ x0 x3 x4 ⟶ x5) ⟶ x5
Definition 180f5.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 . ∀ x5 : ο . ((x1 = x2 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ not (x0 x1 x2) ⟶ not (x0 x1 x3) ⟶ not (x0 x2 x3) ⟶ not (x0 x1 x4) ⟶ x0 x2 x4 ⟶ x0 x3 x4 ⟶ x5) ⟶ x5
Definition 9b945.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 . ∀ x5 : ο . ((x1 = x2 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ not (x0 x1 x2) ⟶ not (x0 x1 x3) ⟶ not (x0 x2 x3) ⟶ x0 x1 x4 ⟶ x0 x2 x4 ⟶ x0 x3 x4 ⟶ x5) ⟶ x5
Known d03c6.. : ∀ x0 . atleastp u4 x0 ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ x1) ⟶ x1
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known neq_i_symneq_i_sym : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2
Theorem a10f1.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ atleastp u4 x0 ⟶ 4402e.. x0 x1 ⟶ ∀ x2 : ο . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 8b6ad.. x1 x3 x4 x5 x6 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 91306.. x1 x3 x4 x5 x6 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 65a4c.. x1 x3 x4 x5 x6 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 2f869.. x1 x3 x4 x5 x6 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ a1d37.. x1 x3 x4 x5 x6 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 180f5.. x1 x3 x4 x5 x6 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 9b945.. x1 x3 x4 x5 x6 ⟶ x2) ⟶ x2 (proof)
Theorem d7596.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ 8b6ad.. x1 x2 x3 x4 x5 ⟶ 8b6ad.. x1 x3 x2 x4 x5 (proof)
Theorem d257b.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ 8b6ad.. x1 x2 x3 x4 x5 ⟶ 8b6ad.. x1 x3 x4 x2 x5 (proof)
Theorem e7d99.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ 8b6ad.. x1 x2 x3 x4 x5 ⟶ 8b6ad.. x1 x5 x2 x3 x4 (proof)
Theorem 51a01.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ 8b6ad.. x1 x2 x3 x4 x5 ⟶ 8b6ad.. x1 x4 x5 x2 x3 (proof)
Theorem 764ed.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ 8b6ad.. x1 x2 x3 x4 x5 ⟶ 8b6ad.. x1 x3 x4 x5 x2 (proof)
Theorem da9f0.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ 8b6ad.. x1 x2 x3 x4 x5 ⟶ 8b6ad.. x1 x3 x2 x5 x4 (proof)
Definition 5a3b5.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (2f869.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ not (x0 x1 x5) ⟶ x0 x2 x5 ⟶ not (x0 x3 x5) ⟶ not (x0 x4 x5) ⟶ x6) ⟶ x6
Definition 6ff44.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (2f869.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ x0 x1 x5 ⟶ x0 x2 x5 ⟶ not (x0 x3 x5) ⟶ not (x0 x4 x5) ⟶ x6) ⟶ x6
Definition 32385.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (a1d37.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ x0 x1 x5 ⟶ x0 x2 x5 ⟶ not (x0 x3 x5) ⟶ not (x0 x4 x5) ⟶ x6) ⟶ x6
Definition 0ee5a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (180f5.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ x0 x1 x5 ⟶ not (x0 x2 x5) ⟶ x0 x3 x5 ⟶ not (x0 x4 x5) ⟶ x6) ⟶ x6
Definition 45422.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (180f5.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ not (x0 x1 x5) ⟶ x0 x2 x5 ⟶ x0 x3 x5 ⟶ not (x0 x4 x5) ⟶ x6) ⟶ x6
Definition 22dda.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (180f5.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ x0 x1 x5 ⟶ x0 x2 x5 ⟶ x0 x3 x5 ⟶ not (x0 x4 x5) ⟶ x6) ⟶ x6
Definition 58403.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (9b945.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ x0 x1 x5 ⟶ x0 x2 x5 ⟶ x0 x3 x5 ⟶ not (x0 x4 x5) ⟶ x6) ⟶ x6
Definition 62523.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (8b6ad.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ not (x0 x1 x5) ⟶ not (x0 x2 x5) ⟶ not (x0 x3 x5) ⟶ x0 x4 x5 ⟶ x6) ⟶ x6
Definition 87c36.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (2f869.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ not (x0 x1 x5) ⟶ x0 x2 x5 ⟶ not (x0 x3 x5) ⟶ x0 x4 x5 ⟶ x6) ⟶ x6
Definition 42d13.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (2f869.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ x0 x1 x5 ⟶ x0 x2 x5 ⟶ not (x0 x3 x5) ⟶ x0 x4 x5 ⟶ x6) ⟶ x6
Definition c5756.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (8b6ad.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ not (x0 x1 x5) ⟶ not (x0 x2 x5) ⟶ x0 x3 x5 ⟶ x0 x4 x5 ⟶ x6) ⟶ x6
Definition 2b028.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (8b6ad.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ not (x0 x1 x5) ⟶ x0 x2 x5 ⟶ x0 x3 x5 ⟶ x0 x4 x5 ⟶ x6) ⟶ x6
Definition 80df3.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (8b6ad.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ x0 x1 x5 ⟶ x0 x2 x5 ⟶ x0 x3 x5 ⟶ x0 x4 x5 ⟶ x6) ⟶ x6
Known setminusEsetminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Known SingISingI : ∀ x0 . x0 ∈ Sing x0
Theorem be264.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3) ⟶ cf2df.. x1 x2 ⟶ ∀ x3 . x3 ∈ x1 ⟶ x0 ⊆ setminus x1 (Sing x3) ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 8b6ad.. x2 x4 x5 x6 x7 ⟶ ∀ x8 : ο . (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 62523.. x2 x9 x10 x11 x12 x3 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ c5756.. x2 x9 x10 x11 x12 x3 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 2b028.. x2 x9 x10 x11 x12 x3 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 80df3.. x2 x9 x10 x11 x12 x3 ⟶ x8) ⟶ x8 (proof)
Known setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1 ⊆ x0
Theorem 6ab71.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3) ⟶ 4402e.. x1 x2 ⟶ ∀ x3 . x3 ∈ x1 ⟶ x0 ⊆ setminus x1 (Sing x3) ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 91306.. x2 x4 x5 x6 x7 ⟶ ∀ x8 : ο . (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 5a3b5.. x2 x3 x9 x10 x11 x12 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 6ff44.. x2 x9 x3 x10 x11 x12 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 0ee5a.. x2 x9 x10 x3 x11 x12 ⟶ x8) ⟶ x8 (proof)
Theorem 9c958.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3) ⟶ 4402e.. x1 x2 ⟶ ∀ x3 . x3 ∈ x1 ⟶ x0 ⊆ setminus x1 (Sing x3) ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 65a4c.. x2 x4 x5 x6 x7 ⟶ ∀ x8 : ο . (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 45422.. x2 x3 x9 x10 x11 x12 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 22dda.. x2 x3 x9 x10 x11 x12 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 58403.. x2 x9 x10 x3 x11 x12 ⟶ x8) ⟶ x8 (proof)
Theorem 03b78.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ 2f869.. x1 x2 x3 x4 x5 ⟶ 2f869.. x1 x3 x2 x4 x5 (proof)
Theorem fe03b.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ 2f869.. x1 x2 x3 x4 x5 ⟶ 2f869.. x1 x2 x3 x5 x4 (proof)
Theorem 33ada.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ 2f869.. x1 x2 x3 x4 x5 ⟶ 2f869.. x1 x3 x2 x5 x4 (proof)
Theorem a1082.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3) ⟶ 4402e.. x1 x2 ⟶ ∀ x3 . x3 ∈ x1 ⟶ x0 ⊆ setminus x1 (Sing x3) ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 2f869.. x2 x4 x5 x6 x7 ⟶ ∀ x8 : ο . (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 5a3b5.. x2 x9 x10 x11 x12 x3 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 6ff44.. x2 x9 x10 x11 x12 x3 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 62523.. x2 x9 x10 x3 x11 x12 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 87c36.. x2 x9 x10 x11 x12 x3 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 42d13.. x2 x9 x10 x11 x12 x3 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ c5756.. x2 x9 x10 x11 x3 x12 ⟶ x8) ⟶ x8 (proof)
Theorem eaeac.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3) ⟶ 4402e.. x1 x2 ⟶ ∀ x3 . x3 ∈ x1 ⟶ x0 ⊆ setminus x1 (Sing x3) ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ a1d37.. x2 x4 x5 x6 x7 ⟶ ∀ x8 : ο . (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 32385.. x2 x9 x10 x11 x12 x3 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 0ee5a.. x2 x9 x3 x10 x11 x12 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 22dda.. x2 x9 x10 x3 x11 x12 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 87c36.. x2 x3 x9 x10 x11 x12 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 42d13.. x2 x9 x3 x10 x11 x12 ⟶ x8) ⟶ x8 (proof)
Theorem 04dd3.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ 180f5.. x1 x2 x3 x4 x5 ⟶ 180f5.. x1 x2 x4 x3 x5 (proof)
Theorem 59a5e.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3) ⟶ 4402e.. x1 x2 ⟶ ∀ x3 . x3 ∈ x1 ⟶ x0 ⊆ setminus x1 (Sing x3) ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 180f5.. x2 x4 x5 x6 x7 ⟶ ∀ x8 : ο . (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 6ff44.. x2 x9 x10 x11 x3 x12 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 0ee5a.. x2 x9 x10 x11 x12 x3 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 45422.. x2 x9 x10 x11 x12 x3 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 22dda.. x2 x9 x10 x11 x12 x3 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 87c36.. x2 x9 x10 x3 x11 x12 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 42d13.. x2 x9 x10 x11 x3 x12 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ c5756.. x2 x9 x3 x10 x11 x12 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 2b028.. x2 x9 x10 x11 x3 x12 ⟶ x8) ⟶ x8 (proof)
Theorem c03d6.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3) ⟶ 4402e.. x1 x2 ⟶ ∀ x3 . x3 ∈ x1 ⟶ x0 ⊆ setminus x1 (Sing x3) ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 9b945.. x2 x4 x5 x6 x7 ⟶ ∀ x8 : ο . (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 22dda.. x2 x9 x10 x11 x3 x12 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 58403.. x2 x9 x10 x11 x12 x3 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 42d13.. x2 x9 x10 x3 x11 x12 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 2b028.. x2 x3 x9 x10 x11 x12 ⟶ x8) ⟶ (∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 80df3.. x2 x9 x10 x11 x3 x12 ⟶ x8) ⟶ x8 (proof)
Known Subq_refSubq_ref : ∀ x0 . x0 ⊆ x0
Known setminusE1setminusE1 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ x2 ∈ x0
Theorem 7a154.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ atleastp u5 x0 ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 : ο . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 5a3b5.. x1 x3 x4 x5 x6 x7 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 6ff44.. x1 x3 x4 x5 x6 x7 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 32385.. x1 x3 x4 x5 x6 x7 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 0ee5a.. x1 x3 x4 x5 x6 x7 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 45422.. x1 x3 x4 x5 x6 x7 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 22dda.. x1 x3 x4 x5 x6 x7 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 58403.. x1 x3 x4 x5 x6 x7 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 62523.. x1 x3 x4 x5 x6 x7 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 87c36.. x1 x3 x4 x5 x6 x7 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 42d13.. x1 x3 x4 x5 x6 x7 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ c5756.. x1 x3 x4 x5 x6 x7 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 2b028.. x1 x3 x4 x5 x6 x7 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 80df3.. x1 x3 x4 x5 x6 x7 ⟶ x2) ⟶ x2 (proof)
Theorem 66a94.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 5a3b5.. x1 x2 x3 x4 x5 x6 ⟶ 5a3b5.. x1 x2 x3 x5 x4 x6 (proof)
Theorem bfe59.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 5a3b5.. x1 x2 x3 x4 x5 x6 ⟶ 5a3b5.. x1 x2 x6 x4 x5 x3 (proof)
Theorem 3236d.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 45422.. x1 x2 x3 x4 x5 x6 ⟶ 45422.. x1 x2 x3 x4 x6 x5 (proof)
Theorem 412d7.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 62523.. x1 x2 x3 x4 x5 x6 ⟶ 62523.. x1 x3 x2 x4 x5 x6 (proof)
Theorem e6ce7.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 62523.. x1 x2 x3 x4 x5 x6 ⟶ 62523.. x1 x2 x4 x3 x5 x6 (proof)
Theorem 01a24.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 62523.. x1 x2 x3 x4 x5 x6 ⟶ 62523.. x1 x2 x3 x4 x6 x5 (proof)
Theorem 91090.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 62523.. x1 x2 x3 x4 x5 x6 ⟶ 62523.. x1 x3 x4 x2 x5 x6 (proof)
Theorem 7cfa7.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ c5756.. x1 x2 x3 x4 x5 x6 ⟶ c5756.. x1 x3 x2 x4 x5 x6 (proof)
Theorem c8c81.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ c5756.. x1 x2 x3 x4 x5 x6 ⟶ c5756.. x1 x2 x3 x5 x4 x6 (proof)
Theorem 5d146.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ c5756.. x1 x2 x3 x4 x5 x6 ⟶ c5756.. x1 x3 x2 x5 x4 x6 (proof)
Theorem d804d.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 2b028.. x1 x2 x3 x4 x5 x6 ⟶ 2b028.. x1 x2 x4 x3 x5 x6 (proof)
Theorem f6130.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 2b028.. x1 x2 x3 x4 x5 x6 ⟶ 2b028.. x1 x2 x4 x5 x3 x6 (proof)
Theorem 86574.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 62523.. x1 x2 x3 x4 x5 x6 ⟶ 62523.. x1 x3 x2 x4 x6 x5 (proof)
Theorem 0c032.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 5a3b5.. x1 x2 x3 x4 x5 x6 ⟶ 5a3b5.. x1 x2 x4 x3 x6 x5 (proof)
Theorem f957b.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 62523.. x1 x2 x3 x4 x5 x6 ⟶ 62523.. x1 x2 x4 x3 x6 x5 (proof)
Theorem 41efe.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 87c36.. x1 x2 x3 x4 x5 x6 ⟶ 87c36.. x1 x2 x4 x3 x6 x5 (proof)
Theorem f0c7f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 5a3b5.. x1 x2 x3 x4 x5 x6 ⟶ 5a3b5.. x1 x2 x5 x6 x3 x4 (proof)
Theorem 2c467.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 45422.. x1 x2 x3 x4 x5 x6 ⟶ 45422.. x1 x2 x5 x6 x3 x4 (proof)
Theorem e3c64.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 45422.. x1 x2 x3 x4 x5 x6 ⟶ 45422.. x1 x2 x6 x5 x4 x3 (proof)
Theorem 1af34.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 62523.. x1 x2 x3 x4 x5 x6 ⟶ 62523.. x1 x3 x4 x2 x6 x5 (proof)