Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrJGW../985a5..
PUVPb../33af1..
vout
PrJGW../8efab.. 1.94 bars
TMMAt../213eb.. ownership of c67bf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTQv../98f81.. ownership of e619f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdJG../fe4a1.. ownership of 3968f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZu6../5f788.. ownership of 412f5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbd6../27a80.. ownership of 09839.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRNo../6b058.. ownership of 7be4c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSZN../dec6d.. ownership of e358b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMai../782c7.. ownership of 36581.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTQH../72fb1.. ownership of 23b00.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZUp../190f9.. ownership of d7a25.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMK62../90106.. ownership of 907b4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG45../91e9c.. ownership of 06821.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMErY../6aee4.. ownership of d5115.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXGY../8a658.. ownership of 111b7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTSC../07333.. ownership of e9104.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMK7E../77dc2.. ownership of d4b77.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXtE../2e262.. ownership of 6a35f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHqH../21823.. ownership of 6867e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQJ2../e648a.. ownership of 53e2d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHtz../c15fa.. ownership of 47d90.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPeX../ccedd.. ownership of bca09.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNLT../b9e0d.. ownership of e4825.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb2c../b7627.. ownership of 097e4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSaL../5925b.. ownership of 9133b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT8J../1d2db.. ownership of a3777.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdop../e5c3b.. ownership of dc174.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZzo../cd030.. ownership of 158f3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTmx../4458b.. ownership of da75f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUz7../a9969.. ownership of 3b6d2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVGa../2c0c9.. ownership of 27f39.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSaV../b82c3.. ownership of fa8f9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVyJ../aff43.. ownership of bda11.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYoP../001ac.. ownership of 57b3e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG5x../141c2.. ownership of 1a4ee.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSUS../a6f9b.. ownership of 02b64.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPrj../3979c.. ownership of ebbaf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJ6c../5085c.. ownership of 26d68.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdW5../9ade3.. ownership of 036ed.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGDF../10574.. ownership of e21c3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTsh../2924e.. ownership of 9884f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUAS../87fdc.. ownership of 9f585.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbzi../00e39.. ownership of fffb8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZFw../05c97.. ownership of 73bae.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYV4../3f4a9.. ownership of 06d1c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaLx../efb33.. ownership of 9593a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdrM../bf343.. ownership of a9dae.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJVo../76a83.. ownership of 10054.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGzp../a35df.. ownership of af50d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMP3D../f486e.. ownership of 3153c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcEr../500d7.. ownership of acb02.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZz5../7ee01.. ownership of 25763.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQdu../9b8ff.. ownership of 122fd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUhr2../d3066.. doc published by PrGxv..
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Param 0fc90.. : ι → (ι → ι) → ι
Definition ac767.. := λ x0 x1 . 0fc90.. x0 (λ x2 . x1)
Known 690be.. : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 x3 : ι → ι . (∀ x4 . prim1 x4 x0 ⟶ Subq (x2 x4) (x3 x4)) ⟶ Subq (0fc90.. x0 x2) (0fc90.. x1 x3)
Theorem 25763.. : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 x3 . Subq x2 x3 ⟶ Subq (ac767.. x0 x2) (ac767.. x1 x3) (proof)
Known d3673.. : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 : ι → ι . Subq (0fc90.. x0 x2) (0fc90.. x1 x2)
Theorem 3153c.. : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 . Subq (ac767.. x0 x2) (ac767.. x1 x2) (proof)
Known Subq_ref : ∀ x0 . Subq x0 x0
Theorem 10054.. : ∀ x0 x1 x2 . Subq x1 x2 ⟶ Subq (ac767.. x0 x1) (ac767.. x0 x2) (proof)
Param aae7a.. : ι → ι → ι
Param f482f.. : ι → ι → ι
Param 4a7ef.. : ι
Param 4ae4a.. : ι → ι
Param e76d4.. : ι → ι
Known 76a87.. : ∀ x0 . e76d4.. x0 = f482f.. x0 4a7ef..
Param 22ca9.. : ι → ι
Known 0ba89.. : ∀ x0 . 22ca9.. x0 = f482f.. x0 (4ae4a.. 4a7ef..)
Known 74782.. : ∀ x0 . Subq (aae7a.. (e76d4.. x0) (22ca9.. x0)) x0
Theorem 9593a.. : ∀ x0 . Subq (aae7a.. (f482f.. x0 4a7ef..) (f482f.. x0 (4ae4a.. 4a7ef..))) x0 (proof)
Known cdaf8.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ aae7a.. (e76d4.. x2) (22ca9.. x2) = x2
Theorem 73bae.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ aae7a.. (f482f.. x2 4a7ef..) (f482f.. x2 (4ae4a.. 4a7ef..)) = x2 (proof)
Param 94f9e.. : ι → (ι → ι) → ι
Known aff96.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 94f9e.. x0 x1 = 94f9e.. x0 x2
Known 33e74.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ prim1 (f482f.. x2 4a7ef..) x0
Known 35b50.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ prim1 (f482f.. x2 (4ae4a.. 4a7ef..)) (x1 (f482f.. x2 4a7ef..))
Theorem 9f585.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ 94f9e.. (ac767.. x0 x1) (λ x5 . x2 (f482f.. x5 4a7ef..) (f482f.. x5 (4ae4a.. 4a7ef..))) = 94f9e.. (ac767.. x0 x1) (λ x5 . x3 (f482f.. x5 4a7ef..) (f482f.. x5 (4ae4a.. 4a7ef..))) (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition 6b93f.. := λ x0 x1 . ∀ x2 . prim1 x2 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (∀ x5 : ο . (∀ x6 . x2 = aae7a.. x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Param If_i : ο → ι → ι → ι
Known exandE_i : ∀ x0 x1 : ι → ο . (∀ x2 : ο . (∀ x3 . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known 7d8a1.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (∀ x5 : ο . (∀ x6 . and (prim1 x6 (x1 x4)) (x2 = aae7a.. x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Theorem e21c3.. : ∀ x0 x1 x2 . 6b93f.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x3 . If_i (x3 = 4a7ef..) x0 (If_i (x3 = 4ae4a.. 4a7ef..) x1 x2))) (proof)
Theorem 26d68.. : ∀ x0 x1 x2 x3 . 6b93f.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (proof)
Param e5b72.. : ι → ι
Param 3097a.. : ι → (ι → ι) → ι
Known 3daee.. : ∀ x0 x1 . Subq x1 x0 ⟶ prim1 x1 (e5b72.. x0)
Known f1083.. : prim1 4a7ef.. (4ae4a.. 4a7ef..)
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known 3c674.. : ∀ x0 . (∀ x1 . nIn x1 x0) ⟶ x0 = 4a7ef..
Definition cad8f.. := λ x0 . aae7a.. (f482f.. x0 4a7ef..) (f482f.. x0 (4ae4a.. 4a7ef..)) = x0
Known 85578.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (3097a.. x0 x1) ⟶ and (∀ x3 . prim1 x3 x2 ⟶ and (cad8f.. x3) (prim1 (f482f.. x3 4a7ef..) x0)) (∀ x3 . prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3))
Param 91630.. : ι → ι
Known dcd83.. : ∀ x0 . nIn x0 4a7ef..
Known aa929.. : ∀ x0 x1 x2 . prim1 (aae7a.. x1 x2) x0 ⟶ prim1 x2 (f482f.. x0 x1)
Known fead7.. : ∀ x0 x1 . prim1 x1 (91630.. x0) ⟶ x1 = x0
Known 30652.. : Subq (4ae4a.. 4a7ef..) (91630.. 4a7ef..)
Known b21da.. : ∀ x0 x1 . prim1 x1 (e5b72.. x0) ⟶ Subq x1 x0
Theorem 02b64.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (e5b72.. (4ae4a.. 4a7ef..))) ⟶ prim1 (3097a.. x0 x1) (e5b72.. (4ae4a.. 4a7ef..)) (proof)
Known 8d403.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . (∀ x3 . prim1 x3 x2 ⟶ and (cad8f.. x3) (prim1 (f482f.. x3 4a7ef..) x0)) ⟶ (∀ x3 . prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3)) ⟶ prim1 x2 (3097a.. x0 x1)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm : ∀ x0 : ο . or x0 (not x0)
Known 34894.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (3097a.. x0 x1) ⟶ 0fc90.. x0 (f482f.. x2) = x2
Known 9e5b2.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . nIn x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = 4a7ef..
Theorem 57b3e.. : ∀ x0 x1 . ∀ x2 : ι → ι . Subq x0 x1 ⟶ (∀ x3 . prim1 x3 x1 ⟶ nIn x3 x0 ⟶ prim1 4a7ef.. (x2 x3)) ⟶ Subq (3097a.. x0 x2) (3097a.. x1 x2) (proof)
Theorem fa8f9.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ Subq (x1 x3) (x2 x3)) ⟶ Subq (3097a.. x0 x1) (3097a.. x0 x2) (proof)
Known Subq_tra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ Subq x1 x2 ⟶ Subq x0 x2
Theorem 3b6d2.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . (∀ x4 . prim1 x4 x0 ⟶ Subq (x2 x4) (x3 x4)) ⟶ Subq x0 x1 ⟶ (∀ x4 . prim1 x4 x1 ⟶ nIn x4 x0 ⟶ prim1 4a7ef.. (x3 x4)) ⟶ Subq (3097a.. x0 x2) (3097a.. x1 x3) (proof)
Definition b5c9f.. := λ x0 x1 . 3097a.. x1 (λ x2 . x0)
Known set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Known and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3
Known 016fc.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ and (and (aae7a.. (e76d4.. x2) (22ca9.. x2) = x2) (prim1 (e76d4.. x2) x0)) (prim1 (22ca9.. x2) (x1 (e76d4.. x2)))
Known f71c6.. : ∀ x0 x1 . aae7a.. x0 x1 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)
Known 27474.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) (x1 x3)) ⟶ prim1 (0fc90.. x0 x2) (3097a.. x0 x1)
Known If_i_or : ∀ x0 : ο . ∀ x1 x2 . or (If_i x0 x1 x2 = x1) (If_i x0 x1 x2 = x2)
Known f5701.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 (x1 x2) ⟶ prim1 (aae7a.. x2 x3) (0fc90.. x0 x1)
Known f336d.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..))
Known 0b783.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..))
Known dcd87.. : ∀ x0 . (∀ x1 . prim1 x1 x0 ⟶ and (cad8f.. x1) (prim1 (f482f.. x1 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ cad8f.. x0
Theorem 158f3.. : ∀ x0 . ac767.. x0 x0 = b5c9f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Theorem a3777.. : ∀ x0 . prim1 4a7ef.. x0 ⟶ ∀ x1 x2 . Subq x1 x2 ⟶ Subq (b5c9f.. x0 x1) (b5c9f.. x0 x2) (proof)
Theorem 097e4.. : ∀ x0 x1 x2 x3 . prim1 4a7ef.. x3 ⟶ Subq x2 x3 ⟶ Subq x0 x1 ⟶ Subq (b5c9f.. x2 x0) (b5c9f.. x3 x1) (proof)
Param ba9d8.. : ι → ο
Known 8f913.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ Subq x1 x0
Theorem bca09.. : ∀ x0 . prim1 4a7ef.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ ∀ x2 . prim1 x2 x1 ⟶ Subq (b5c9f.. x0 x2) (b5c9f.. x0 x1) (proof)
Known 204eb.. : aae7a.. = λ x1 x2 . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x1 x2)
Known 4b3cb.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 (aae7a.. 4a7ef.. x2) (aae7a.. x0 x1)
Theorem 53e2d.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) 4a7ef.. x2)) (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)) (proof)
Known 2391b.. : ∀ x0 x1 x2 . prim1 x2 x1 ⟶ prim1 (aae7a.. (4ae4a.. 4a7ef..) x2) (aae7a.. x0 x1)
Theorem 6a35f.. : ∀ x0 x1 x2 . prim1 x2 x1 ⟶ prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) (4ae4a.. 4a7ef..) x2)) (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)) (proof)
Known 2f64c.. : ∀ x0 x1 x2 . prim1 x2 (aae7a.. x0 x1) ⟶ or (∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (x2 = aae7a.. 4a7ef.. x4) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (prim1 x4 x1) (x2 = aae7a.. (4ae4a.. 4a7ef..) x4) ⟶ x3) ⟶ x3)
Theorem e9104.. : ∀ x0 x1 x2 . prim1 x2 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)) ⟶ or (∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (x2 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x6 . If_i (x6 = 4a7ef..) 4a7ef.. x4)) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (prim1 x4 x1) (x2 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x6 . If_i (x6 = 4a7ef..) (4ae4a.. 4a7ef..) x4)) ⟶ x3) ⟶ x3) (proof)
Theorem 1cc2a.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 (x1 x2) ⟶ prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x4 . If_i (x4 = 4a7ef..) x2 x3)) (0fc90.. x0 x1) (proof)
Theorem d5115.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x1 ⟶ prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x4 . If_i (x4 = 4a7ef..) x2 x3)) (ac767.. x0 x1) (proof)
Theorem 907b4.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x4 . If_i (x4 = 4a7ef..) (f482f.. x2 4a7ef..) (f482f.. x2 (4ae4a.. 4a7ef..))) = x2 (proof)
Theorem 23b00.. : ∀ x0 x1 x2 . prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x1 x2)) x0 ⟶ prim1 x2 (f482f.. x0 x1) (proof)
Known 2a2bc.. : ∀ x0 x1 x2 . prim1 x2 (f482f.. x0 x1) ⟶ prim1 (aae7a.. x1 x2) x0
Theorem e358b.. : ∀ x0 x1 x2 . prim1 x2 (f482f.. x0 x1) ⟶ prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x1 x2)) x0 (proof)
Known 3f849.. : ∀ x0 . Subq x0 4a7ef.. ⟶ x0 = 4a7ef..
Theorem 09839.. : ∀ x0 . f482f.. 4a7ef.. x0 = 4a7ef.. (proof)
Known bcb22.. : ∀ x0 x1 . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1))) = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)
Known 9f6cd.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 x0
Known 6f2e8.. : ∀ x0 x1 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)) 4a7ef.. = x0
Known 15d37.. : ∀ x0 x1 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)) (4ae4a.. 4a7ef..) = x1
Theorem 3968f.. : ∀ x0 x1 x2 . prim1 x0 x2 ⟶ prim1 x1 x2 ⟶ prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)) (b5c9f.. x2 (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Param bij : ι → ι → (ι → ι) → ο
Known aa4b6.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ bij x0 x0 x1
Known d7fe6.. : ba9d8.. (4ae4a.. (4ae4a.. 4a7ef..))
Theorem c67bf.. : ∀ x0 x1 . prim1 x0 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ prim1 x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ bij (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. 4a7ef..)) (f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x2 . If_i (x2 = 4a7ef..) x0 x1))) (proof)