Search for blocks/addresses/...

Proofgold Asset

asset id
32d07ed52820d028686428dc253c24468b01ca1e9e79a6118c96d59ad367bb8e
asset hash
8d968ac11df79c036e2794c0f024502196e1aaf1f16287058c3fd23a97ffa9b8
bday / block
20801
tx
707bf..
preasset
doc published by Pr4zB..
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition In2_lexicographic := λ x0 x1 x2 x3 . or (x1x3) (and (x1 = x3) (x0x2))
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition nInnIn := λ x0 x1 . not (x0x1)
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Theorem 94e96.. : ∀ x0 x1 . not (In2_lexicographic x0 x1 x0 x1) (proof)
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Definition TransSetTransSet := λ x0 . ∀ x1 . x1x0x1x0
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem 65c2b.. : ∀ x0 x1 x2 x3 x4 x5 . TransSet x4TransSet x5In2_lexicographic x0 x1 x2 x3In2_lexicographic x2 x3 x4 x5In2_lexicographic x0 x1 x4 x5 (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
Param TwoRamseyGraph_4_6_35_a : ιιιιο
Param ordinalordinal : ιο
Known ordinal_trichotomy_or_impredordinal_trichotomy_or_impred : ∀ x0 x1 . ordinal x0ordinal x1∀ x2 : ο . (x0x1x2)(x0 = x1x2)(x1x0x2)x2
Known FalseEFalseE : False∀ x0 : ο . x0
Known dd650.. : ∀ x0 . x0u6∀ x1 . x1u6TwoRamseyGraph_4_6_35_a x0 x1 x0 x1
Param nat_pnat_p : ιο
Known nat_p_ordinalnat_p_ordinal : ∀ x0 . nat_p x0ordinal x0
Known nat_p_transnat_p_trans : ∀ x0 . nat_p x0∀ x1 . x1x0nat_p x1
Known nat_6nat_6 : nat_p 6
Theorem 67627.. : ∀ x0 . x0u6∀ x1 . x1u6∀ x2 . x2u6∀ x3 . x3u6not (TwoRamseyGraph_4_6_35_a x0 x1 x2 x3)or (In2_lexicographic x0 x1 x2 x3) (In2_lexicographic x2 x3 x0 x1) (proof)
Known In_0_1In_0_1 : 01
Theorem e709e.. : ∀ x0 . x0u6∀ x1 . x1u6In2_lexicographic x0 0 x1 u1 (proof)
Known In_0_2In_0_2 : 02
Theorem 0d8f3.. : ∀ x0 . x0u6∀ x1 . x1u6In2_lexicographic x0 0 x1 u2 (proof)
Known In_1_2In_1_2 : 12
Theorem b8306.. : ∀ x0 . x0u6∀ x1 . x1u6In2_lexicographic x0 u1 x1 u2 (proof)
Known In_0_3In_0_3 : 03
Theorem 27f34.. : ∀ x0 . x0u6∀ x1 . x1u6In2_lexicographic x0 0 x1 u3 (proof)
Known In_1_3In_1_3 : 13
Theorem 36690.. : ∀ x0 . x0u6∀ x1 . x1u6In2_lexicographic x0 u1 x1 u3 (proof)
Known In_2_3In_2_3 : 23
Theorem 27a87.. : ∀ x0 . x0u6∀ x1 . x1u6In2_lexicographic x0 u2 x1 u3 (proof)
Known In_0_4In_0_4 : 04
Theorem 3f697.. : ∀ x0 . x0u6∀ x1 . x1u6In2_lexicographic x0 0 x1 u4 (proof)
Known In_1_4In_1_4 : 14
Theorem be5f9.. : ∀ x0 . x0u6∀ x1 . x1u6In2_lexicographic x0 u1 x1 u4 (proof)
Known In_2_4In_2_4 : 24
Theorem 952f7.. : ∀ x0 . x0u6∀ x1 . x1u6In2_lexicographic x0 u2 x1 u4 (proof)
Known In_3_4In_3_4 : 34
Theorem e60e7.. : ∀ x0 . x0u6∀ x1 . x1u6In2_lexicographic x0 u3 x1 u4 (proof)
Known In_0_5In_0_5 : 05
Theorem 03171.. : ∀ x0 . x0u6∀ x1 . x1u6In2_lexicographic x0 0 x1 u5 (proof)
Known In_1_5In_1_5 : 15
Theorem 9750a.. : ∀ x0 . x0u6∀ x1 . x1u6In2_lexicographic x0 u1 x1 u5 (proof)
Known In_2_5In_2_5 : 25
Theorem f1e9b.. : ∀ x0 . x0u6∀ x1 . x1u6In2_lexicographic x0 u2 x1 u5 (proof)
Known In_3_5In_3_5 : 35
Theorem b30df.. : ∀ x0 . x0u6∀ x1 . x1u6In2_lexicographic x0 u3 x1 u5 (proof)
Known In_4_5In_4_5 : 45
Theorem 035bb.. : ∀ x0 . x0u6∀ x1 . x1u6In2_lexicographic x0 u4 x1 u5 (proof)
Known In_no2cycleIn_no2cycle : ∀ x0 x1 . x0x1x1x0False
Theorem 6f0f0.. : ∀ x0 . x0u6∀ x1 . x1u6not (In2_lexicographic x0 u1 x1 0) (proof)
Theorem 1b2aa.. : ∀ x0 . x0u6∀ x1 . x1u6not (In2_lexicographic x0 u2 x1 0) (proof)
Theorem 829cc.. : ∀ x0 . x0u6∀ x1 . x1u6not (In2_lexicographic x0 u3 x1 0) (proof)
Theorem 1c740.. : ∀ x0 . x0u6∀ x1 . x1u6not (In2_lexicographic x0 u4 x1 0) (proof)
Theorem 196b9.. : ∀ x0 . x0u6∀ x1 . x1u6not (In2_lexicographic x0 u5 x1 0) (proof)
Theorem 97a37.. : ∀ x0 . x0u6∀ x1 . x1u6not (In2_lexicographic x0 u2 x1 u1) (proof)
Theorem b27e1.. : ∀ x0 . x0u6∀ x1 . x1u6not (In2_lexicographic x0 u3 x1 u1) (proof)
Theorem 52c59.. : ∀ x0 . x0u6∀ x1 . x1u6not (In2_lexicographic x0 u4 x1 u1) (proof)
Theorem 2efb1.. : ∀ x0 . x0u6∀ x1 . x1u6not (In2_lexicographic x0 u5 x1 u1) (proof)
Theorem 696a1.. : ∀ x0 . x0u6∀ x1 . x1u6not (In2_lexicographic x0 u3 x1 u2) (proof)
Theorem dd794.. : ∀ x0 . x0u6∀ x1 . x1u6not (In2_lexicographic x0 u4 x1 u2) (proof)
Theorem dd382.. : ∀ x0 . x0u6∀ x1 . x1u6not (In2_lexicographic x0 u5 x1 u2) (proof)
Theorem ffa46.. : ∀ x0 . x0u6∀ x1 . x1u6not (In2_lexicographic x0 u4 x1 u3) (proof)
Theorem e28f6.. : ∀ x0 . x0u6∀ x1 . x1u6not (In2_lexicographic x0 u5 x1 u3) (proof)
Theorem 1f4d3.. : ∀ x0 . x0u6∀ x1 . x1u6not (In2_lexicographic x0 u5 x1 u4) (proof)
Theorem 0b098.. : ∀ x0 . x0u6In2_lexicographic 0 x0 u1 x0 (proof)
Theorem 5e815.. : ∀ x0 . x0u6In2_lexicographic 0 x0 u2 x0 (proof)
Theorem 6bdbd.. : ∀ x0 . x0u6In2_lexicographic u1 x0 u2 x0 (proof)
Theorem 0b5bd.. : ∀ x0 . x0u6In2_lexicographic 0 x0 u3 x0 (proof)
Theorem d2a78.. : ∀ x0 . x0u6In2_lexicographic u1 x0 u3 x0 (proof)
Theorem 07268.. : ∀ x0 . x0u6In2_lexicographic u2 x0 u3 x0 (proof)
Theorem e04f2.. : ∀ x0 . x0u6In2_lexicographic 0 x0 u4 x0 (proof)
Theorem e1002.. : ∀ x0 . x0u6In2_lexicographic u1 x0 u4 x0 (proof)
Theorem 58234.. : ∀ x0 . x0u6In2_lexicographic u2 x0 u4 x0 (proof)
Theorem b7796.. : ∀ x0 . x0u6In2_lexicographic u3 x0 u4 x0 (proof)
Theorem 6fa01.. : ∀ x0 . x0u6In2_lexicographic 0 x0 u5 x0 (proof)
Theorem 740f5.. : ∀ x0 . x0u6In2_lexicographic u1 x0 u5 x0 (proof)
Theorem 90d47.. : ∀ x0 . x0u6In2_lexicographic u2 x0 u5 x0 (proof)
Theorem 0a7a8.. : ∀ x0 . x0u6In2_lexicographic u3 x0 u5 x0 (proof)
Theorem bb6fa.. : ∀ x0 . x0u6In2_lexicographic u4 x0 u5 x0 (proof)
Theorem b5ca8.. : ∀ x0 . x0u6not (In2_lexicographic 0 x0 0 x0) (proof)
Theorem 15042.. : ∀ x0 . x0u6not (In2_lexicographic u1 x0 0 x0) (proof)
Theorem 4ed6e.. : ∀ x0 . x0u6not (In2_lexicographic u2 x0 0 x0) (proof)
Theorem aa680.. : ∀ x0 . x0u6not (In2_lexicographic u3 x0 0 x0) (proof)
Theorem be2c5.. : ∀ x0 . x0u6not (In2_lexicographic u4 x0 0 x0) (proof)
Theorem fb400.. : ∀ x0 . x0u6not (In2_lexicographic u5 x0 0 x0) (proof)
Theorem 69e13.. : ∀ x0 . x0u6not (In2_lexicographic u1 x0 u1 x0) (proof)
Theorem b695a.. : ∀ x0 . x0u6not (In2_lexicographic u2 x0 u1 x0) (proof)
Theorem e7d59.. : ∀ x0 . x0u6not (In2_lexicographic u3 x0 u1 x0) (proof)
Theorem a3e6e.. : ∀ x0 . x0u6not (In2_lexicographic u4 x0 u1 x0) (proof)
Theorem dadcc.. : ∀ x0 . x0u6not (In2_lexicographic u5 x0 u1 x0) (proof)
Theorem 05e9c.. : ∀ x0 . x0u6not (In2_lexicographic u2 x0 u2 x0) (proof)
Theorem a73b8.. : ∀ x0 . x0u6not (In2_lexicographic u3 x0 u2 x0) (proof)
Theorem b6f90.. : ∀ x0 . x0u6not (In2_lexicographic u4 x0 u2 x0) (proof)
Theorem 6bc25.. : ∀ x0 . x0u6not (In2_lexicographic u5 x0 u2 x0) (proof)
Theorem 52f87.. : ∀ x0 . x0u6not (In2_lexicographic u3 x0 u3 x0) (proof)
Theorem dc51f.. : ∀ x0 . x0u6not (In2_lexicographic u4 x0 u3 x0) (proof)
Theorem 447d5.. : ∀ x0 . x0u6not (In2_lexicographic u5 x0 u3 x0) (proof)
Theorem a58bd.. : ∀ x0 . x0u6not (In2_lexicographic u4 x0 u4 x0) (proof)
Theorem 2313b.. : ∀ x0 . x0u6not (In2_lexicographic u5 x0 u4 x0) (proof)
Theorem 56b5c.. : ∀ x0 . x0u6not (In2_lexicographic u5 x0 u5 x0) (proof)