Proofgold Address

Param a842e.. : ι → (ι → ι) → ι
Param 94f9e.. : ι → (ι → ι) → ι
Param aae7a.. : ι → ι → ι
Definition 0fc90.. := λ x0 . λ x1 : ι → ι . a842e.. x0 (λ x2 . 94f9e.. (x1 x2) (aae7a.. x2))
Known 2236b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . prim1 x2 x0 ⟶ prim1 x3 (x1 x2) ⟶ prim1 x3 (a842e.. x0 x1)
Known 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (94f9e.. x0 x1)
Theorem f5701.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 (x1 x2) ⟶ prim1 (aae7a.. x2 x3) (0fc90.. x0 x1) (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param e76d4.. : ι → ι
Param 22ca9.. : ι → ι
Known exandE_i : ∀ x0 x1 : ι → ο . (∀ x2 : ο . (∀ x3 . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2
Known 8c6f6.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known 5dd0a.. : ∀ x0 x1 . e76d4.. (aae7a.. x0 x1) = x0
Known 40190.. : ∀ x0 x1 . 22ca9.. (aae7a.. x0 x1) = x1
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known 042d7.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (a842e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (prim1 x2 (x1 x4)) ⟶ x3) ⟶ x3
Theorem 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))) (proof)
Known and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3
Theorem cdaf8.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ aae7a.. (e76d4.. x2) (22ca9.. x2) = x2 (proof)
Theorem a268e.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ prim1 (e76d4.. x2) x0 (proof)
Theorem cbf3e.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ prim1 (22ca9.. x2) (x1 (e76d4.. x2)) (proof)
Theorem 5d5fc.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . prim1 (aae7a.. x2 x3) (0fc90.. x0 x1) ⟶ prim1 x2 x0 (proof)
Theorem e2bb7.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . prim1 (aae7a.. x2 x3) (0fc90.. x0 x1) ⟶ prim1 x3 (x1 x2) (proof)
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 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 (proof)
Definition iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Known iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem 9b331.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (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) (proof)
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Theorem 690be.. : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 x3 : ι → ι . (∀ x4 . prim1 x4 x0 ⟶ Subq (x2 x4) (x3 x4)) ⟶ Subq (0fc90.. x0 x2) (0fc90.. x1 x3) (proof)
Known Subq_ref : ∀ x0 . Subq x0 x0
Theorem d3673.. : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 : ι → ι . Subq (0fc90.. x0 x2) (0fc90.. x1 x2) (proof)
Theorem f42b8.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ Subq (x1 x3) (x2 x3)) ⟶ Subq (0fc90.. x0 x1) (0fc90.. x0 x2) (proof)
Param e5b72.. : ι → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Known 3daee.. : ∀ x0 x1 . Subq x1 x0 ⟶ prim1 x1 (e5b72.. x0)
Known f1083.. : prim1 4a7ef.. (4ae4a.. 4a7ef..)
Known 7144c.. : aae7a.. 4a7ef.. 4a7ef.. = 4a7ef..
Param 91630.. : ι → ι
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 2ad56.. : ∀ x0 . prim1 x0 (e5b72.. (4ae4a.. 4a7ef..)) ⟶ ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (e5b72.. (4ae4a.. 4a7ef..))) ⟶ prim1 (0fc90.. x0 x1) (e5b72.. (4ae4a.. 4a7ef..)) (proof)
Definition ac767.. := λ x0 x1 . 0fc90.. x0 (λ x2 . x1)
Theorem c5caa.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x1 ⟶ prim1 (aae7a.. x2 x3) (ac767.. x0 x1) (proof)
Theorem 8f68d.. : ∀ x0 x1 x2 . prim1 x2 (ac767.. x0 x1) ⟶ prim1 (e76d4.. x2) x0 (proof)
Theorem fd5b7.. : ∀ x0 x1 x2 . prim1 x2 (ac767.. x0 x1) ⟶ prim1 (22ca9.. x2) x1 (proof)
Theorem 713d5.. : ∀ x0 x1 x2 x3 . prim1 (aae7a.. x2 x3) (ac767.. x0 x1) ⟶ prim1 x2 x0 (proof)
Theorem 4949d.. : ∀ x0 x1 x2 x3 . prim1 (aae7a.. x2 x3) (ac767.. x0 x1) ⟶ prim1 x3 x1 (proof)
Param a4c2a.. : ι → (ι → ο) → (ι → ι) → ι
Definition f482f.. := λ x0 x1 . a4c2a.. x0 (λ x2 . ∀ x3 : ο . (∀ x4 . x2 = aae7a.. x1 x4 ⟶ x3) ⟶ x3) 22ca9..
Theorem f5701.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 (x1 x2) ⟶ prim1 (aae7a.. x2 x3) (0fc90.. x0 x1) (proof)
Theorem 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 (proof)
Theorem 9b331.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (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) (proof)
Known e951d.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . prim1 x3 x0 ⟶ x1 x3 ⟶ prim1 (x2 x3) (a4c2a.. x0 x1 x2)
Theorem aa929.. : ∀ x0 x1 x2 . prim1 (aae7a.. x1 x2) x0 ⟶ prim1 x2 (f482f.. x0 x1) (proof)
Known 932b3.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . prim1 x3 (a4c2a.. x0 x1 x2) ⟶ ∀ x4 : ο . (∀ x5 . prim1 x5 x0 ⟶ x1 x5 ⟶ x3 = x2 x5 ⟶ x4) ⟶ x4
Theorem 2a2bc.. : ∀ x0 x1 x2 . prim1 x2 (f482f.. x0 x1) ⟶ prim1 (aae7a.. x1 x2) x0 (proof)
Theorem 69f30.. : ∀ x0 x1 x2 . iff (prim1 x2 (f482f.. x0 x1)) (prim1 (aae7a.. x1 x2) x0) (proof)
Known set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Theorem f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2 (proof)
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..
Theorem 9e5b2.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . nIn x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = 4a7ef.. (proof)
Known a6d0f.. : ∀ x0 x1 . prim1 x1 (e76d4.. x0) ⟶ prim1 (aae7a.. 4a7ef.. x1) x0
Known 2ef56.. : ∀ x0 x1 . prim1 (aae7a.. 4a7ef.. x1) x0 ⟶ prim1 x1 (e76d4.. x0)
Theorem 76a87.. : ∀ x0 . e76d4.. x0 = f482f.. x0 4a7ef.. (proof)
Known 98a9e.. : ∀ x0 x1 . prim1 x1 (22ca9.. x0) ⟶ prim1 (aae7a.. (4ae4a.. 4a7ef..) x1) x0
Known 36427.. : ∀ x0 x1 . prim1 (aae7a.. (4ae4a.. 4a7ef..) x1) x0 ⟶ prim1 x1 (22ca9.. x0)
Theorem 0ba89.. : ∀ x0 . 22ca9.. x0 = f482f.. x0 (4ae4a.. 4a7ef..) (proof)
Theorem 3f040.. : ∀ x0 x1 . f482f.. (aae7a.. x0 x1) 4a7ef.. = x0 (proof)
Theorem a283f.. : ∀ x0 x1 . f482f.. (aae7a.. x0 x1) (4ae4a.. 4a7ef..) = x1 (proof)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
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)
Known cf31f.. : ∀ x0 x1 x2 x3 . aae7a.. x0 x1 = aae7a.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known f336d.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..))
Known 0b783.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..))
Theorem a7149.. : ∀ x0 x1 x2 . nIn x2 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ f482f.. (aae7a.. x0 x1) x2 = 4a7ef.. (proof)
Theorem 33e74.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ prim1 (f482f.. x2 4a7ef..) x0 (proof)
Theorem 35b50.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ prim1 (f482f.. x2 (4ae4a.. 4a7ef..)) (x1 (f482f.. x2 4a7ef..)) (proof)
Definition cad8f.. := λ x0 . aae7a.. (f482f.. x0 4a7ef..) (f482f.. x0 (4ae4a.. 4a7ef..)) = x0
Theorem 73bc9.. : ∀ x0 x1 . cad8f.. (aae7a.. x0 x1) (proof)
Known 2532b.. : ∀ x0 x1 x2 . prim1 x0 (prim2 x1 x2) ⟶ or (x0 = x1) (x0 = x2)
Known 4b3cb.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 (aae7a.. 4a7ef.. x2) (aae7a.. x0 x1)
Known 2391b.. : ∀ x0 x1 x2 . prim1 x2 x1 ⟶ prim1 (aae7a.. (4ae4a.. 4a7ef..) x2) (aae7a.. x0 x1)
Known 2ea0c.. : Subq (4ae4a.. (4ae4a.. 4a7ef..)) (prim2 4a7ef.. (4ae4a.. 4a7ef..))
Theorem dcd87.. : ∀ x0 . (∀ x1 . prim1 x1 x0 ⟶ and (cad8f.. x1) (prim1 (f482f.. x1 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ cad8f.. x0 (proof)
Theorem dfdb3.. : ∀ x0 x1 . cad8f.. x0 ⟶ prim1 x0 x1 ⟶ prim1 (f482f.. x0 (4ae4a.. 4a7ef..)) (f482f.. x1 (f482f.. x0 4a7ef..)) (proof)
Definition 6b93f.. := λ x0 x1 . ∀ x2 . prim1 x2 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (∀ x5 : ο . (∀ x6 . x2 = aae7a.. x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Known pred_ext_2 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x1 x2 ⟶ x0 x2) ⟶ x0 = x1
Theorem 7d7d0.. : cad8f.. = 6b93f.. (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Param If_i : ο → ι → ι → ι
Theorem d9414.. : ∀ x0 x1 . 6b93f.. (4ae4a.. (4ae4a.. 4a7ef..)) (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x2 . If_i (x2 = 4a7ef..) x0 x1)) (proof)
Known If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Known If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known 5c667.. : 4ae4a.. 4a7ef.. = 4a7ef.. ⟶ ∀ x0 : ο . x0
Theorem f71c6.. : ∀ x0 x1 . aae7a.. x0 x1 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1) (proof)
Param 1216a.. : ι → (ι → ο) → ι
Definition 3097a.. := λ x0 . λ x1 : ι → ι . 1216a.. (e5b72.. (0fc90.. x0 (λ x2 . prim3 (x1 x2)))) (λ x2 . ∀ x3 . prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3))
Known b2421.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 ⟶ prim1 x2 (1216a.. x0 x1)
Known UnionI : ∀ x0 x1 x2 . prim1 x1 x2 ⟶ prim1 x2 x0 ⟶ prim1 x1 (prim3 x0)
Theorem 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) (proof)
Known 6982e.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ and (prim1 x2 x0) (x1 x2)
Theorem 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)) (proof)
Theorem 5795e.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (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))) (proof)
Theorem 27474.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) (x1 x3)) ⟶ prim1 (0fc90.. x0 x2) (3097a.. x0 x1) (proof)
Known ac5c1.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ x1 x2
Theorem d8d74.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . prim1 x2 (3097a.. x0 x1) ⟶ prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3) (proof)
Theorem cce19.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (3097a.. x0 x1) ⟶ ∀ x3 . prim1 x3 (3097a.. x0 x1) ⟶ (∀ x4 . prim1 x4 x0 ⟶ Subq (f482f.. x2 x4) (f482f.. x3 x4)) ⟶ Subq x2 x3 (proof)
Theorem 6e275.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (3097a.. x0 x1) ⟶ ∀ x3 . prim1 x3 (3097a.. x0 x1) ⟶ (∀ x4 . prim1 x4 x0 ⟶ f482f.. x2 x4 = f482f.. x3 x4) ⟶ x2 = x3 (proof)
Theorem 34894.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (3097a.. x0 x1) ⟶ 0fc90.. x0 (f482f.. x2) = x2 (proof)
Definition b5c9f.. := λ x0 x1 . 3097a.. x1 (λ x2 . x0)
Theorem 204eb.. : aae7a.. = λ x1 x2 . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x1 x2) (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 8c3eb.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (∀ x5 : ο . (∀ x6 . and (prim1 x6 (x1 x4)) (x2 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x8 . If_i (x8 = 4a7ef..) x4 x6)) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Theorem 2d4b0.. : ∀ x0 x1 x2 x3 . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x5 . If_i (x5 = 4a7ef..) x0 x1) = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x5 . If_i (x5 = 4a7ef..) x2 x3) ⟶ and (x0 = x2) (x1 = x3) (proof)
Theorem 6f2e8.. : ∀ x0 x1 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)) 4a7ef.. = x0 (proof)
Theorem 15d37.. : ∀ x0 x1 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)) (4ae4a.. 4a7ef..) = x1 (proof)
Definition 38062.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ο . 1216a.. (0fc90.. x0 x1) (λ x3 . x2 (f482f.. x3 4a7ef..) (f482f.. x3 (4ae4a.. 4a7ef..)))
Theorem 380ca.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 (x1 x3) ⟶ x2 x3 x4 ⟶ prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x5 . If_i (x5 = 4a7ef..) x3 x4)) (38062.. x0 x1 x2) (proof)
Theorem fbd31.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . prim1 x3 (38062.. x0 x1 x2) ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (∀ x6 : ο . (∀ x7 . and (prim1 x7 (x1 x5)) (and (x3 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x9 . If_i (x9 = 4a7ef..) x5 x7)) (x2 x5 x7)) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4 (proof)
Theorem 0d9ad.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x5 . If_i (x5 = 4a7ef..) x3 x4)) (38062.. x0 x1 x2) ⟶ and (and (prim1 x3 x0) (prim1 x4 (x1 x3))) (x2 x3 x4) (proof)
Theorem 41662.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x5 . If_i (x5 = 4a7ef..) x3 x4)) (38062.. x0 x1 x2) ⟶ prim1 x3 x0 (proof)
Theorem 36b09.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x5 . If_i (x5 = 4a7ef..) x3 x4)) (38062.. x0 x1 x2) ⟶ prim1 x4 (x1 x3) (proof)
Theorem 338b2.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x5 . If_i (x5 = 4a7ef..) x3 x4)) (38062.. x0 x1 x2) ⟶ x2 x3 x4 (proof)
Definition 76607.. := λ x0 . ∀ x1 . prim1 x1 x0 ⟶ ∀ x2 : ο . (∀ x3 . (∀ x4 : ο . (∀ x5 . x1 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x7 . If_i (x7 = 4a7ef..) x3 x5) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2
Theorem 78561.. : ∀ x0 x1 . 76607.. x0 ⟶ 76607.. x1 ⟶ (∀ x2 x3 . iff (prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x4 . If_i (x4 = 4a7ef..) x2 x3)) x0) (prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x4 . If_i (x4 = 4a7ef..) x2 x3)) x1)) ⟶ x0 = x1 (proof)
Theorem f6f3f.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . 76607.. (38062.. x0 x1 x2) (proof)
Theorem 5af6c.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 : ι → ι → ο . (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 (x1 x4) ⟶ iff (x2 x4 x5) (x3 x4 x5)) ⟶ 38062.. x0 x1 x2 = 38062.. x0 x1 x3 (proof)
Theorem a850e.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ Subq (0fc90.. x0 x1) (0fc90.. x0 x2) (proof)
Theorem 4402a.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 0fc90.. x0 x1 = 0fc90.. x0 x2 (proof)
Theorem 7e4c2.. : ∀ x0 . ∀ x1 : ι → ι . 0fc90.. x0 (f482f.. (0fc90.. x0 x1)) = 0fc90.. x0 x1 (proof)
Theorem 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) (proof)
Definition 25755.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ι . 0fc90.. x0 (λ x3 . 0fc90.. (x1 x3) (x2 x3))
Theorem 1b91d.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 (x1 x3) ⟶ f482f.. (f482f.. (25755.. x0 x1 x2) x3) x4 = x2 x3 x4 (proof)
Theorem ed27c.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 : ι → ι → ι . (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 (x1 x4) ⟶ x2 x4 x5 = x3 x4 x5) ⟶ 25755.. x0 x1 x2 = 25755.. x0 x1 x3 (proof)
Definition 0fc90.. := 0fc90..
Definition f482f.. := f482f..
Definition eb53d.. := λ x0 . 25755.. x0 (λ x1 . x0)
Definition e3162.. := λ x0 x1 . f482f.. (f482f.. x0 x1)
Definition 1216a.. := 1216a..
Definition decode_p := λ x0 x1 . prim1 x1 x0
Definition d2155.. := λ x0 . 38062.. x0 (λ x1 . x0)
Definition 2b2e3.. := λ x0 x1 x2 . prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x1 x2)) x0
Definition e0e40.. := λ x0 . λ x1 : (ι → ο) → ο . 1216a.. (e5b72.. x0) (λ x2 . x1 (λ x3 . prim1 x3 x2))
Definition decode_c := λ x0 . λ x1 : ι → ο . ∀ x2 : ο . (∀ x3 . and (∀ x4 . iff (x1 x4) (prim1 x4 x3)) (prim1 x3 x0) ⟶ x2) ⟶ x2
Theorem f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2 (proof)
Theorem 4402a.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 0fc90.. x0 x1 = 0fc90.. x0 x2 (proof)
Theorem 35054.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ e3162.. (eb53d.. x0 x1) x2 x3 = x1 x2 x3 (proof)
Theorem 8fdaf.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ eb53d.. x0 x1 = eb53d.. x0 x2 (proof)
Known prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Theorem 931fe.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ decode_p (1216a.. x0 x1) x2 = x1 x2 (proof)
Theorem ee7ef.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ 1216a.. x0 x1 = 1216a.. x0 x2 (proof)
Theorem 67416.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ 2b2e3.. (d2155.. x0 x1) x2 x3 = x1 x2 x3 (proof)
Theorem 62ef7.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ iff (x1 x3 x4) (x2 x3 x4)) ⟶ d2155.. x0 x1 = d2155.. x0 x2 (proof)
Known d129e.. : ∀ x0 . ∀ x1 : ι → ο . prim1 (1216a.. x0 x1) (e5b72.. x0)
Theorem 81500.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ο . (∀ x3 . x2 x3 ⟶ prim1 x3 x0) ⟶ decode_c (e0e40.. x0 x1) x2 = x1 x2 (proof)
Theorem fe043.. : ∀ x0 . ∀ x1 x2 : (ι → ο) → ο . (∀ x3 : ι → ο . (∀ x4 . x3 x4 ⟶ prim1 x4 x0) ⟶ iff (x1 x3) (x2 x3)) ⟶ e0e40.. x0 x1 = e0e40.. x0 x2 (proof)