Proofgold Address

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)