Search for blocks/addresses/...

Proofgold Asset

asset id
70f68cd3e9f5cfbd91c9c20632ac14e160984effbcd4ae80df750c8f5e5fc681
asset hash
30fcedc5872a7d60ada50bb2fb4e87c980a18194978b6cf3d6173f83bca4a6b7
bday / block
1149
tx
36a0a..
preasset
doc published by PrGxv..
Known 8106d..notI : ∀ x0 : ο . (x0False)not x0
Known notEnotE : ∀ x0 : ο . not x0x0False
Theorem 91bfe..dnegI : ∀ x0 : ο . x0not (not x0) (proof)
Known 5f92b..dneg : ∀ x0 : ο . not (not x0)x0
Theorem b4782..contra : ∀ x0 : ο . (not x0False)x0 (proof)
Known 47706..xmcases : ∀ x0 x1 : ο . (x0x1)(not x0x1)x1
Theorem 0a8dd..keepcopy : ∀ x0 : ο . (not x0x0)x0 (proof)
Known dcbd9..orIL : ∀ x0 x1 : ο . x0or x0 x1
Known eca40..orIR : ∀ x0 x1 : ο . x1or x0 x1
Known FalseEFalseE : False∀ x0 : ο . x0
Theorem 3f786..orI_contra : ∀ x0 x1 : ο . (not x0not x1False)or x0 x1 (proof)
Theorem d47b4..orI_imp1 : ∀ x0 x1 : ο . (x0x1)or (not x0) x1 (proof)
Theorem d5b81..orI_imp2 : ∀ x0 x1 : ο . (x1x0)or x0 (not x1) (proof)
Known andEandE : ∀ x0 x1 : ο . and x0 x1∀ x2 : ο . (x0x1x2)x2
Theorem 57def..tab_pos_and : ∀ x0 x1 : ο . and x0 x1(x0x1False)False (proof)
Known 37124..orE : ∀ x0 x1 : ο . or x0 x1∀ x2 : ο . (x0x2)(x1x2)x2
Theorem 26b88..tab_pos_or : ∀ x0 x1 : ο . or x0 x1(x0False)(x1False)False (proof)
Theorem 7ffa0..tab_pos_imp : ∀ x0 x1 : ο . (x0x1)(not x0False)(x1False)False (proof)
Known d182e..iffE : ∀ x0 x1 : ο . iff x0 x1∀ x2 : ο . (x0x1x2)(not x0not x1x2)x2
Theorem a19af..tab_pos_iff : ∀ x0 x1 : ο . iff x0 x1(x0x1False)(not x0not x1False)False (proof)
Theorem c44ec..tab_neg_imp : ∀ x0 x1 : ο . not (x0x1)(x0not x1False)False (proof)
Known 7c02f..andI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem 77eb0..tab_neg_and : ∀ x0 x1 : ο . not (and x0 x1)(not x0False)(not x1False)False (proof)
Theorem 6a5f4..tab_neg_or : ∀ x0 x1 : ο . not (or x0 x1)(not x0not x1False)False (proof)
Known 32c82..iffI : ∀ x0 x1 : ο . (x0x1)(x1x0)iff x0 x1
Theorem b2d9e..tab_neg_iff : ∀ x0 x1 : ο . not (iff x0 x1)(x0not x1False)(not x0x1False)False (proof)
Known 2540e..prop_ext : ∀ x0 x1 : ο . iff x0 x1x0 = x1
Theorem prop_ext_2prop_ext_2 : ∀ x0 x1 : ο . (x0x1)(x1x0)x0 = x1 (proof)
Theorem 30c0c..eqo_iff : ∀ x0 x1 : ο . x0 = x1iff x0 x1 (proof)
Theorem d0d7f..tab_pos_eqo : ∀ x0 x1 : ο . x0 = x1(x0x1False)(not x0not x1False)False (proof)
Theorem 7a33c..tab_neg_eqo : ∀ x0 x1 : ο . not (x0 = x1)(x0not x1False)(not x0x1False)False (proof)
Theorem b4c6f..tab_pos_all_i : ∀ x0 : ι → ο . ∀ x1 . (∀ x2 . x0 x2)(x0 x1False)False (proof)
Theorem 29614..tab_neg_all_i : ∀ x0 : ι → ο . not (∀ x1 . x0 x1)(∀ x1 . not (x0 x1)False)False (proof)
Theorem 2f8d2..tab_pos_ex_i : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2x1)x1)(∀ x1 . x0 x1False)False (proof)
Theorem 2f8d2..tab_pos_ex_i : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2x1)x1)(∀ x1 . x0 x1False)False (proof)
Theorem 18cb3..tab_mat_i_o : ∀ x0 : ι → ο . ∀ x1 x2 . x0 x1not (x0 x2)(not (x1 = x2)False)False (proof)
Theorem 8c503..tab_mat_i_i_o : ∀ x0 : ι → ι → ο . ∀ x1 x2 x3 x4 . x0 x1 x2not (x0 x3 x4)(not (x1 = x3)False)(not (x2 = x4)False)False (proof)
Theorem 2b3a3..tab_confront : ∀ x0 x1 x2 x3 . x0 = x1not (x2 = x3)(not (x0 = x2)not (x1 = x2)False)(not (x0 = x3)not (x1 = x3)False)False (proof)
Theorem f_eq_if_equal_i_i : ∀ x0 : ι → ι . ∀ x1 x2 . x1 = x2x0 x1 = x0 x2 (proof)
Theorem 31719..tab_dec_i : ∀ x0 : ι → ι . ∀ x1 x2 . not (x0 x1 = x0 x2)(not (x1 = x2)False)False (proof)
Theorem f_eq_i_if_equal_i_i_i : ∀ x0 : ι → ι → ι . ∀ x1 x2 x3 x4 . x1 = x2x3 = x4x0 x1 x3 = x0 x2 x4 (proof)
Theorem 06083..tab_dec_i_i : ∀ x0 : ι → ι → ι . ∀ x1 x2 x3 x4 . not (x0 x1 x3 = x0 x2 x4)(not (x1 = x2)False)(not (x3 = x4)False)False (proof)
Theorem 3f27c..tab_pos_eqf_i_i : ∀ x0 x1 : ι → ι . ∀ x2 . x0 = x1(x0 x2 = x1 x2False)False (proof)
Theorem 48643..tab_pos_neqf_i_i : ∀ x0 x1 : ι → ι . not (x0 = x1)(∀ x2 . not (x0 x2 = x1 x2)False)False (proof)