Search for blocks/addresses/...

Proofgold Signed Transaction

vin
Pr3fd../bb753..
PUYky../1e9cb..
vout
Pr3fd../024ab.. 4.98 bars
TMTHq../4d9c1.. negprop ownership controlledby Pr4zB.. upto 0
TMF9r../0d2b3.. negprop ownership controlledby Pr4zB.. upto 0
TMFYW../eef3e.. ownership of 5039e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMPc9../0b0f1.. ownership of ac13d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMboa../382cb.. ownership of 68cc7.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMc9N../cb697.. ownership of 78f6b.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMcBV../b0287.. ownership of dd7b9.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMUK5../4b4e6.. ownership of dadf5.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKoV../a5348.. ownership of 5e23e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMMC3../97639.. ownership of 0622a.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMHRP../6657e.. ownership of ea2d2.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMFSb../28f78.. ownership of 24b80.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNFw../07832.. ownership of eb902.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMcE1../dd9d8.. ownership of 805df.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMacj../f3077.. ownership of 788d0.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKXd../ac9a6.. ownership of 1947e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMbkk../2fbb9.. ownership of 946e7.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMT7t../31a5d.. ownership of 60030.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMdJ1../9ac62.. ownership of b8710.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMdu1../4cdf9.. ownership of 5fd69.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMTMs../67166.. ownership of 75e61.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKeY../56e29.. ownership of 18a65.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMa6C../a9430.. ownership of 3dec4.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMUft../c3736.. ownership of 1030b.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
PUagg../c9ece.. doc published by Pr4zB..
Definition Church17_p := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x2)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x3)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x4)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x5)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x6)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x7)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x8)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x9)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x10)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x11)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x12)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x13)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x14)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x15)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x16)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x17)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x18)x1 x0
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Theorem 3dec4.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0or ((λ x2 x3 . x0 x2 x2 x2 x2 x2 x2 x2 x2 x2 x3 x3 x3 x3 x3 x3 x3 x3) = λ x2 x3 . x2) ((λ x2 x3 . x0 x3 x3 x3 x3 x3 x3 x3 x3 x3 x2 x2 x2 x2 x2 x2 x2 x2) = λ x2 x3 . x2) (proof)
Param ordsuccordsucc : ιι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
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
Known d6f89.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0Church17_p x1((λ x3 x4 . x0 x3 x3 x3 x3 x3 x3 x3 x3 x3 x4 x4 x4 x4 x4 x4 x4 x4) = λ x3 x4 . x3)x0 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 = x1 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16x0 = x1
Known d74be.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0Church17_p x1((λ x3 x4 . x0 x4 x4 x4 x4 x4 x4 x4 x4 x4 x3 x3 x3 x3 x3 x3 x3 x3) = λ x3 x4 . x3)x0 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 = x1 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16x0 = x1
Theorem 75e61.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0Church17_p x1x0 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 = x1 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16x0 = x1 (proof)
Definition TwoRamseyGraph_4_4_Church17 := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x2 x3 . x0 (x1 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2) (x1 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2) (x1 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3) (x1 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2) (x1 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3) (x1 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3) (x1 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3) (x1 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2) (x1 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2) (x1 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3) (x1 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3) (x1 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3) (x1 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2) (x1 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3) (x1 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2) (x1 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2) (x1 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3)
Definition FalseFalse := ∀ x0 : ο . x0
Known cc816.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0Church17_p x1Church17_p x2((λ x4 x5 . x0 x4 x4 x4 x4 x4 x4 x4 x4 x4 x5 x5 x5 x5 x5 x5 x5 x5) = λ x4 x5 . x4)((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x0∀ x3 : ο . x3)((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x1∀ x3 : ο . x3)((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x2∀ x3 : ο . x3)(x0 = x1∀ x3 : ο . x3)(x0 = x2∀ x3 : ο . x3)(x1 = x2∀ x3 : ο . x3)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x0 = λ x4 x5 . x4)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x1 = λ x4 x5 . x4)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x2 = λ x4 x5 . x4)(TwoRamseyGraph_4_4_Church17 x0 x1 = λ x4 x5 . x4)(TwoRamseyGraph_4_4_Church17 x0 x2 = λ x4 x5 . x4)(TwoRamseyGraph_4_4_Church17 x1 x2 = λ x4 x5 . x4)False
Known fb66e.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0Church17_p x1Church17_p x2((λ x4 x5 . x0 x5 x5 x5 x5 x5 x5 x5 x5 x5 x4 x4 x4 x4 x4 x4 x4 x4) = λ x4 x5 . x4)((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x0∀ x3 : ο . x3)((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x1∀ x3 : ο . x3)((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x2∀ x3 : ο . x3)(x0 = x1∀ x3 : ο . x3)(x0 = x2∀ x3 : ο . x3)(x1 = x2∀ x3 : ο . x3)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x0 = λ x4 x5 . x4)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x1 = λ x4 x5 . x4)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x2 = λ x4 x5 . x4)(TwoRamseyGraph_4_4_Church17 x0 x1 = λ x4 x5 . x4)(TwoRamseyGraph_4_4_Church17 x0 x2 = λ x4 x5 . x4)(TwoRamseyGraph_4_4_Church17 x1 x2 = λ x4 x5 . x4)False
Known 768c1.. : ((λ x1 x2 . x2) = λ x1 x2 . x1)∀ x0 : ο . x0
Theorem b8710.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0Church17_p x1Church17_p x2((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x0∀ x3 : ο . x3)((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x1∀ x3 : ο . x3)((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x2∀ x3 : ο . x3)(x0 = x1∀ x3 : ο . x3)(x0 = x2∀ x3 : ο . x3)(x1 = x2∀ x3 : ο . x3)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x0 = λ x4 x5 . x4)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x1 = λ x4 x5 . x4)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x2 = λ x4 x5 . x4)(TwoRamseyGraph_4_4_Church17 x0 x1 = λ x4 x5 . x4)(TwoRamseyGraph_4_4_Church17 x0 x2 = λ x4 x5 . x4)(TwoRamseyGraph_4_4_Church17 x1 x2 = λ x4 x5 . x4)False (proof)
Known 745f5.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0∀ x1 : ο . (∀ x2 x3 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι)ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (∀ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x4Church17_p (x2 x4))(∀ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x4Church17_p (x3 x4))(∀ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x2 (x3 x4) = x4)(∀ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x3 (x2 x4) = x4)(∀ x4 x5 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x4Church17_p x5TwoRamseyGraph_4_4_Church17 x4 x5 = TwoRamseyGraph_4_4_Church17 (x2 x4) (x2 x5))(x2 x0 = λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . x5)x1)x1
Theorem 946e7.. : ∀ x0 x1 x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0Church17_p x1Church17_p x2Church17_p x3(x0 = x1∀ x4 : ο . x4)(x0 = x2∀ x4 : ο . x4)(x0 = x3∀ x4 : ο . x4)(x1 = x2∀ x4 : ο . x4)(x1 = x3∀ x4 : ο . x4)(x2 = x3∀ x4 : ο . x4)(TwoRamseyGraph_4_4_Church17 x0 x1 = λ x5 x6 . x5)(TwoRamseyGraph_4_4_Church17 x0 x2 = λ x5 x6 . x5)(TwoRamseyGraph_4_4_Church17 x0 x3 = λ x5 x6 . x5)(TwoRamseyGraph_4_4_Church17 x1 x2 = λ x5 x6 . x5)(TwoRamseyGraph_4_4_Church17 x1 x3 = λ x5 x6 . x5)(TwoRamseyGraph_4_4_Church17 x2 x3 = λ x5 x6 . x5)False (proof)
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Definition u17 := ordsucc u16
Param atleastpatleastp : ιιο
Definition notnot := λ x0 : ο . x0False
Definition TwoRamseyGraph_4_4_17 := λ x0 x1 . ∀ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2Church17_p x3x0 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16x1 = x3 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16TwoRamseyGraph_4_4_Church17 x2 x3 = λ x5 x6 . x5
Known d03c6.. : ∀ x0 . atleastp u4 x0∀ x1 : ο . (∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0(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
Known ec2ba.. : ∀ x0 . x0u17∀ x1 : ο . (∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2x0 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16x1)x1
Theorem 788d0.. : ∀ x0 . x0u17atleastp u4 x0not (∀ x1 . x1x0∀ x2 . x2x0(x1 = x2∀ x3 : ο . x3)TwoRamseyGraph_4_4_17 x1 x2) (proof)
Theorem eb902.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0Church17_p x1or (TwoRamseyGraph_4_4_Church17 x0 x1 = λ x3 x4 . x3) (TwoRamseyGraph_4_4_Church17 x0 x1 = λ x3 x4 . x4) (proof)
Known 7861e.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0Church17_p x1Church17_p x2((λ x4 x5 . x4) = λ x4 x5 . x0 x4 x4 x4 x4 x4 x4 x4 x4 x4 x5 x5 x5 x5 x5 x5 x5 x5)((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x0∀ x3 : ο . x3)((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x1∀ x3 : ο . x3)((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x2∀ x3 : ο . x3)(x0 = x1∀ x3 : ο . x3)(x0 = x2∀ x3 : ο . x3)(x1 = x2∀ x3 : ο . x3)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x0 = λ x4 x5 . x5)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x1 = λ x4 x5 . x5)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x2 = λ x4 x5 . x5)(TwoRamseyGraph_4_4_Church17 x0 x1 = λ x4 x5 . x5)(TwoRamseyGraph_4_4_Church17 x0 x2 = λ x4 x5 . x5)(TwoRamseyGraph_4_4_Church17 x1 x2 = λ x4 x5 . x5)False
Known 2f37a.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0Church17_p x1Church17_p x2((λ x4 x5 . x4) = λ x4 x5 . x0 x5 x5 x5 x5 x5 x5 x5 x5 x5 x4 x4 x4 x4 x4 x4 x4 x4)((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x0∀ x3 : ο . x3)((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x1∀ x3 : ο . x3)((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x2∀ x3 : ο . x3)(x0 = x1∀ x3 : ο . x3)(x0 = x2∀ x3 : ο . x3)(x1 = x2∀ x3 : ο . x3)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x0 = λ x4 x5 . x5)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x1 = λ x4 x5 . x5)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x2 = λ x4 x5 . x5)(TwoRamseyGraph_4_4_Church17 x0 x1 = λ x4 x5 . x5)(TwoRamseyGraph_4_4_Church17 x0 x2 = λ x4 x5 . x5)(TwoRamseyGraph_4_4_Church17 x1 x2 = λ x4 x5 . x5)False
Theorem ea2d2.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0Church17_p x1Church17_p x2((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x0∀ x3 : ο . x3)((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x1∀ x3 : ο . x3)((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x2∀ x3 : ο . x3)(x0 = x1∀ x3 : ο . x3)(x0 = x2∀ x3 : ο . x3)(x1 = x2∀ x3 : ο . x3)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x0 = λ x4 x5 . x5)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x1 = λ x4 x5 . x5)(TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x2 = λ x4 x5 . x5)(TwoRamseyGraph_4_4_Church17 x0 x1 = λ x4 x5 . x5)(TwoRamseyGraph_4_4_Church17 x0 x2 = λ x4 x5 . x5)(TwoRamseyGraph_4_4_Church17 x1 x2 = λ x4 x5 . x5)False (proof)
Theorem 5e23e.. : ∀ x0 x1 x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0Church17_p x1Church17_p x2Church17_p x3(x0 = x1∀ x4 : ο . x4)(x0 = x2∀ x4 : ο . x4)(x0 = x3∀ x4 : ο . x4)(x1 = x2∀ x4 : ο . x4)(x1 = x3∀ x4 : ο . x4)(x2 = x3∀ x4 : ο . x4)(TwoRamseyGraph_4_4_Church17 x0 x1 = λ x5 x6 . x6)(TwoRamseyGraph_4_4_Church17 x0 x2 = λ x5 x6 . x6)(TwoRamseyGraph_4_4_Church17 x0 x3 = λ x5 x6 . x6)(TwoRamseyGraph_4_4_Church17 x1 x2 = λ x5 x6 . x6)(TwoRamseyGraph_4_4_Church17 x1 x3 = λ x5 x6 . x6)(TwoRamseyGraph_4_4_Church17 x2 x3 = λ x5 x6 . x6)False (proof)
Known FalseEFalseE : False∀ x0 : ο . x0
Theorem dd7b9.. : ∀ x0 . x0u17atleastp u4 x0not (∀ x1 . x1x0∀ x2 . x2x0(x1 = x2∀ x3 : ο . x3)not (TwoRamseyGraph_4_4_17 x1 x2)) (proof)
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
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 bea4f.. : ∀ x0 x1 . TwoRamseyGraph_4_4_17 x0 x1TwoRamseyGraph_4_4_17 x1 x0
Theorem not_TwoRamseyProp_atleast_4_4_17 : not (TwoRamseyProp_atleastp 4 4 17) (proof)
Param TwoRamseyPropTwoRamseyProp : ιιιο
Known TwoRamseyProp_atleastp_atleastp : ∀ x0 x1 x2 x3 x4 . TwoRamseyProp x0 x2 x4atleastp x1 x0atleastp x3 x2TwoRamseyProp_atleastp x1 x3 x4
Known atleastp_ref : ∀ x0 . atleastp x0 x0
Theorem not_TwoRamseyProp_4_4_17not_TwoRamseyProp_4_4_17 : not (TwoRamseyProp 4 4 17) (proof)