Proofgold Signed Transaction

Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param 91630.. : ι → ι
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known 958ef.. : ∀ x0 x1 . prim1 x1 (4ae4a.. x0) ⟶ or (prim1 x1 x0) (x1 = x0)
Definition False := ∀ x0 : ο . x0
Known FalseE : False ⟶ ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known dcd83.. : ∀ x0 . nIn x0 4a7ef..
Known e7a4c.. : ∀ x0 . prim1 x0 (91630.. x0)
Theorem 30652.. : Subq (4ae4a.. 4a7ef..) (91630.. 4a7ef..) (proof)
Known fead7.. : ∀ x0 x1 . prim1 x1 (91630.. x0) ⟶ x1 = x0
Known 5faa3.. : ∀ x0 . prim1 x0 (4ae4a.. x0)
Theorem 7d3c5.. : Subq (91630.. 4a7ef..) (4ae4a.. 4a7ef..) (proof)
Known set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Theorem 84d8a.. : 4ae4a.. 4a7ef.. = 91630.. 4a7ef.. (proof)
Known 67787.. : ∀ x0 x1 . prim1 x0 (prim2 x0 x1)
Known 5a932.. : ∀ x0 x1 . prim1 x1 (prim2 x0 x1)
Theorem 2ea0c.. : Subq (4ae4a.. (4ae4a.. 4a7ef..)) (prim2 4a7ef.. (4ae4a.. 4a7ef..)) (proof)
Known 2532b.. : ∀ x0 x1 x2 . prim1 x0 (prim2 x1 x2) ⟶ or (x0 = x1) (x0 = x2)
Known f336d.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..))
Known 0b783.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..))
Theorem 67f2b.. : Subq (prim2 4a7ef.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Theorem 7e6ff.. : 4ae4a.. (4ae4a.. 4a7ef..) = prim2 4a7ef.. (4ae4a.. 4a7ef..) (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition TransSet := λ x0 . ∀ x1 . prim1 x1 x0 ⟶ Subq x1 x0
Definition ordinal := λ x0 . and (TransSet x0) (∀ x1 . prim1 x1 x0 ⟶ TransSet x1)
Known In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Known ordinal_Hered : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ ordinal x1
Theorem ordinal_ind : ∀ x0 : ι → ο . (∀ x1 . ordinal x1 ⟶ (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . ordinal x1 ⟶ x0 x1 (proof)
Known dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem least_ordinal_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . and (ordinal x2) (x0 x2) ⟶ x1) ⟶ x1) ⟶ ∀ x1 : ο . (∀ x2 . and (and (ordinal x2) (x0 x2)) (∀ x3 . prim1 x3 x2 ⟶ not (x0 x3)) ⟶ x1) ⟶ x1 (proof)
Param ba9d8.. : ι → ο
Known f3fb5.. : ∀ x0 . ba9d8.. x0 ⟶ ordinal x0
Known 3db81.. : ba9d8.. (4ae4a.. 4a7ef..)
Theorem 9c410.. : ordinal (4ae4a.. 4a7ef..) (proof)
Known d7fe6.. : ba9d8.. (4ae4a.. (4ae4a.. 4a7ef..))
Theorem 5d775.. : ordinal (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Param 48ef8.. : ι
Known a3321.. : ∀ x0 . ba9d8.. x0 ⟶ prim1 x0 48ef8..
Known 10a0b.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ ba9d8.. x1
Known c2711.. : ∀ x0 . prim1 x0 48ef8.. ⟶ ba9d8.. x0
Theorem ee316.. : TransSet 48ef8.. (proof)
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known ordinal_TransSet : ∀ x0 . ordinal x0 ⟶ TransSet x0
Theorem c8a5e.. : ordinal 48ef8.. (proof)
Known b72a3.. : ∀ x0 . ordinal x0 ⟶ ordinal (4ae4a.. x0)
Theorem 31e2d.. : ordinal (4ae4a.. 48ef8..) (proof)
Theorem f72f7.. : ∀ x0 . TransSet x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ Subq (4ae4a.. x1) x0 (proof)
Theorem 7b84d.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ Subq (4ae4a.. x1) x0 (proof)
Known xm : ∀ x0 : ο . or x0 (not x0)
Known or3I1 : ∀ x0 x1 x2 : ο . x0 ⟶ or (or x0 x1) x2
Known or3I3 : ∀ x0 x1 x2 : ο . x2 ⟶ or (or x0 x1) x2
Known or3I2 : ∀ x0 x1 x2 : ο . x1 ⟶ or (or x0 x1) x2
Known or3E : ∀ x0 x1 x2 : ο . or (or x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x3) ⟶ (x1 ⟶ x3) ⟶ (x2 ⟶ x3) ⟶ x3
Theorem ordinal_trichotomy_or : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (or (prim1 x0 x1) (x0 = x1)) (prim1 x1 x0) (proof)
Param exactly1of3 : ο → ο → ο → ο
Known exactly1of3_I1 : ∀ x0 x1 x2 : ο . x0 ⟶ not x1 ⟶ not x2 ⟶ exactly1of3 x0 x1 x2
Known In_irref : ∀ x0 . nIn x0 x0
Known bba3d.. : ∀ x0 x1 . prim1 x0 x1 ⟶ nIn x1 x0
Known exactly1of3_I2 : ∀ x0 x1 x2 : ο . not x0 ⟶ x1 ⟶ not x2 ⟶ exactly1of3 x0 x1 x2
Known exactly1of3_I3 : ∀ x0 x1 x2 : ο . not x0 ⟶ not x1 ⟶ x2 ⟶ exactly1of3 x0 x1 x2
Theorem ordinal_trichotomy : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ exactly1of3 (prim1 x0 x1) (x0 = x1) (prim1 x1 x0) (proof)
Known orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known Subq_ref : ∀ x0 . Subq x0 x0
Theorem ordinal_In_Or_Subq : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (prim1 x0 x1) (Subq x1 x0) (proof)
Theorem ordinal_linear : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (Subq x0 x1) (Subq x1 x0) (proof)
Theorem 4f62a.. : ∀ x0 x1 . ordinal x0 ⟶ prim1 x1 x0 ⟶ or (prim1 (4ae4a.. x1) x0) (x0 = 4ae4a.. x1) (proof)
Theorem 74eef.. : ∀ x0 . ordinal x0 ⟶ or (∀ x1 . prim1 x1 x0 ⟶ prim1 (4ae4a.. x1) x0) (∀ x1 : ο . (∀ x2 . and (prim1 x2 x0) (x0 = 4ae4a.. x2) ⟶ x1) ⟶ x1) (proof)
Known c79db.. : ∀ x0 . Subq x0 (4ae4a.. x0)
Theorem 09068.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ prim1 (4ae4a.. x1) (4ae4a.. x0) (proof)
Known UnionE_impred : ∀ x0 x1 . prim1 x1 (prim3 x0) ⟶ ∀ x2 : ο . (∀ x3 . prim1 x1 x3 ⟶ prim1 x3 x0 ⟶ x2) ⟶ x2
Known UnionI : ∀ x0 x1 x2 . prim1 x1 x2 ⟶ prim1 x2 x0 ⟶ prim1 x1 (prim3 x0)
Theorem ordinal_Union : ∀ x0 . (∀ x1 . prim1 x1 x0 ⟶ ordinal x1) ⟶ ordinal (prim3 x0) (proof)
Param a842e.. : ι → (ι → ι) → ι
Known 042d7.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (a842e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (prim1 x2 (x1 x4)) ⟶ x3) ⟶ x3
Known 2236b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . prim1 x2 x0 ⟶ prim1 x3 (x1 x2) ⟶ prim1 x3 (a842e.. x0 x1)
Theorem d5fb2.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ordinal (x1 x2)) ⟶ ordinal (a842e.. x0 x1) (proof)
Param d3786.. : ι → ι → ι
Known bd118.. : ∀ x0 x1 . Subq x0 x1 ⟶ d3786.. x0 x1 = x0
Known d7325.. : ∀ x0 x1 . d3786.. x0 x1 = d3786.. x1 x0
Theorem dec57.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal (d3786.. x0 x1) (proof)
Param 0ac37.. : ι → ι → ι
Known 02255.. : ∀ x0 x1 . Subq x0 x1 = (0ac37.. x0 x1 = x1)
Known 47e6b.. : ∀ x0 x1 . 0ac37.. x0 x1 = 0ac37.. x1 x0
Theorem 45024.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal (0ac37.. x0 x1) (proof)
Param 1216a.. : ι → (ι → ο) → ι
Known 6982e.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ and (prim1 x2 x0) (x1 x2)
Known b2421.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 ⟶ prim1 x2 (1216a.. x0 x1)
Known d0a1f.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ prim1 x2 x0
Theorem 94de3.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x2 ⟶ x1 x2 ⟶ x1 x3) ⟶ ordinal (1216a.. x0 x1) (proof)
Param In_rec_i : (ι → (ι → ι) → ι) → ι → ι
Param 94f9e.. : ι → (ι → ι) → ι
Definition 09364.. := In_rec_i (λ x0 . λ x1 : ι → ι . 0ac37.. (91630.. 4a7ef..) (94f9e.. x0 x1))
Known In_rec_i_eq : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_i x0 x1 = x0 x1 (In_rec_i x0)
Known aff96.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 94f9e.. x0 x1 = 94f9e.. x0 x2
Theorem 23d9d.. : ∀ x0 . 09364.. x0 = 0ac37.. (91630.. 4a7ef..) (94f9e.. x0 09364..) (proof)
Known da962.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 x2 (0ac37.. x0 x1)
Theorem 91202.. : ∀ x0 . prim1 4a7ef.. (09364.. x0) (proof)
Known 287ca.. : ∀ x0 x1 x2 . prim1 x2 x1 ⟶ prim1 x2 (0ac37.. x0 x1)
Known 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (94f9e.. x0 x1)
Theorem 2bfb0.. : ∀ x0 x1 . prim1 x1 x0 ⟶ prim1 (09364.. x1) (09364.. x0) (proof)
Known edd11.. : ∀ x0 x1 x2 . prim1 x2 (0ac37.. x0 x1) ⟶ or (prim1 x2 x0) (prim1 x2 x1)
Known 6acac.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (x2 = x1 x4) ⟶ x3) ⟶ x3
Theorem 41491.. : ∀ x0 x1 . prim1 x1 (09364.. x0) ⟶ or (x1 = 4a7ef..) (∀ x2 : ο . (∀ x3 . and (prim1 x3 x0) (x1 = 09364.. x3) ⟶ x2) ⟶ x2) (proof)
Theorem ec645.. : ∀ x0 . 09364.. x0 = 4a7ef.. ⟶ ∀ x1 : ο . x1 (proof)
Theorem 69933.. : ∀ x0 . nIn (09364.. x0) (91630.. 4a7ef..) (proof)
Definition f6917.. := λ x0 . 94f9e.. x0 09364..
Theorem f6cc9.. : ∀ x0 x1 . prim1 x1 x0 ⟶ prim1 (09364.. x1) (f6917.. x0) (proof)
Theorem ee5e5.. : ∀ x0 x1 . prim1 x1 (f6917.. x0) ⟶ ∀ x2 : ο . (∀ x3 . and (prim1 x3 x0) (x1 = 09364.. x3) ⟶ x2) ⟶ x2 (proof)
Param 1ad11.. : ι → ι → ι
Definition 158d3.. := In_rec_i (λ x0 . 94f9e.. (1ad11.. x0 (91630.. 4a7ef..)))
Known 26c23.. : ∀ x0 x1 x2 . prim1 x2 (1ad11.. x0 x1) ⟶ prim1 x2 x0
Theorem 626b2.. : ∀ x0 . 158d3.. x0 = 94f9e.. (1ad11.. x0 (91630.. 4a7ef..)) 158d3.. (proof)
Known 8c6f6.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known 017d4.. : ∀ x0 x1 x2 . prim1 x2 (1ad11.. x0 x1) ⟶ and (prim1 x2 x0) (nIn x2 x1)
Known exandE_i : ∀ x0 x1 : ι → ο . (∀ x2 : ο . (∀ x3 . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2
Known 753c4.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ nIn x2 x1 ⟶ prim1 x2 (1ad11.. x0 x1)
Theorem 36ac3.. : ∀ x0 . 158d3.. (09364.. x0) = x0 (proof)
Theorem b38e0.. : ∀ x0 x1 . 09364.. x0 = 09364.. x1 ⟶ x0 = x1 (proof)
Theorem cfee8.. : ∀ x0 . 158d3.. (f6917.. x0) = x0 (proof)
Theorem c78f5.. : ∀ x0 x1 . f6917.. x0 = f6917.. x1 ⟶ x0 = x1 (proof)
Known d4dbc.. : ∀ x0 : ι → ι . 94f9e.. 4a7ef.. x0 = 4a7ef..
Theorem 6bdaa.. : f6917.. 4a7ef.. = 4a7ef.. (proof)
Known andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Theorem 21fb1.. : ∀ x0 x1 . f6917.. x0 = 09364.. x1 ⟶ ∀ x2 : ο . x2 (proof)
Definition aae7a.. := λ x0 x1 . 0ac37.. (94f9e.. x0 f6917..) (94f9e.. x1 09364..)
Theorem 21d47.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 (f6917.. x2) (aae7a.. x0 x1) (proof)
Theorem 6264f.. : ∀ x0 x1 x2 . prim1 x2 x1 ⟶ prim1 (09364.. x2) (aae7a.. x0 x1) (proof)
Theorem 757ca.. : ∀ x0 x1 x2 . prim1 x2 (aae7a.. x0 x1) ⟶ or (∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (x2 = f6917.. x4) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (prim1 x4 x1) (x2 = 09364.. x4) ⟶ x3) ⟶ x3) (proof)
Theorem 87fed.. : ∀ x0 . aae7a.. 4a7ef.. x0 = f6917.. x0 (proof)
Known f1083.. : prim1 4a7ef.. (4ae4a.. 4a7ef..)
Theorem df04e.. : ∀ x0 . aae7a.. (4ae4a.. 4a7ef..) x0 = 09364.. x0 (proof)
Known 839f4.. : ∀ x0 : ι → ο . (∀ x1 . ba9d8.. x1 ⟶ (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . ba9d8.. x1 ⟶ x0 x1
Known 26358.. : ∀ x0 . ba9d8.. x0 ⟶ prim1 4a7ef.. (4ae4a.. x0)
Known 3238a.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ prim1 (4ae4a.. x1) (4ae4a.. x0)
Known be77e.. : ∀ x0 . ba9d8.. x0 ⟶ or (x0 = 4a7ef..) (∀ x1 : ο . (∀ x2 . and (ba9d8.. x2) (x0 = 4ae4a.. x2) ⟶ x1) ⟶ x1)
Known 8f913.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ Subq x1 x0
Theorem 052e8.. : ∀ x0 . ba9d8.. x0 ⟶ aae7a.. (4ae4a.. 4a7ef..) x0 = 4ae4a.. x0 (proof)
Theorem 7144c.. : aae7a.. 4a7ef.. 4a7ef.. = 4a7ef.. (proof)
Known 4c9b8.. : ba9d8.. 4a7ef..
Theorem 6601d.. : aae7a.. (4ae4a.. 4a7ef..) 4a7ef.. = 4ae4a.. 4a7ef.. (proof)
Theorem 9cfb0.. : aae7a.. (4ae4a.. 4a7ef..) (4ae4a.. 4a7ef..) = 4ae4a.. (4ae4a.. 4a7ef..) (proof)
Theorem 5e53a.. : ∀ x0 x1 x2 x3 . Subq x0 x2 ⟶ Subq x1 x3 ⟶ Subq (aae7a.. x0 x1) (aae7a.. x2 x3) (proof)
Param If_i : ο → ι → ι → ι
Definition 04bd5.. := λ x0 x1 . λ x2 x3 : ι → ι . λ x4 . If_i (x4 = f6917.. (158d3.. x4)) (x2 (158d3.. x4)) (x3 (158d3.. x4))
Known If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem c9165.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . 04bd5.. x0 x1 x2 x3 (f6917.. x4) = x2 x4 (proof)
Known If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Theorem 0185a.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . 04bd5.. x0 x1 x2 x3 (09364.. x4) = x3 x4 (proof)
Theorem 7144c.. : aae7a.. 4a7ef.. 4a7ef.. = 4a7ef.. (proof)
Theorem 6601d.. : aae7a.. (4ae4a.. 4a7ef..) 4a7ef.. = 4ae4a.. 4a7ef.. (proof)
Theorem 9cfb0.. : aae7a.. (4ae4a.. 4a7ef..) (4ae4a.. 4a7ef..) = 4ae4a.. (4ae4a.. 4a7ef..) (proof)
Theorem 052e8.. : ∀ x0 . ba9d8.. x0 ⟶ aae7a.. (4ae4a.. 4a7ef..) x0 = 4ae4a.. x0 (proof)
Param a4c2a.. : ι → (ι → ο) → (ι → ι) → ι
Definition e76d4.. := λ x0 . a4c2a.. x0 (λ x1 . ∀ x2 : ο . (∀ x3 . f6917.. x3 = x1 ⟶ x2) ⟶ x2) 158d3..
Definition 22ca9.. := λ x0 . a4c2a.. x0 (λ x1 . ∀ x2 : ο . (∀ x3 . 09364.. x3 = x1 ⟶ x2) ⟶ x2) 158d3..
Theorem cec21.. : f6917.. = aae7a.. 4a7ef.. (proof)
Theorem 78070.. : 09364.. = aae7a.. (4ae4a.. 4a7ef..) (proof)
Theorem 4b3cb.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 (aae7a.. 4a7ef.. x2) (aae7a.. x0 x1) (proof)
Theorem 2391b.. : ∀ x0 x1 x2 . prim1 x2 x1 ⟶ prim1 (aae7a.. (4ae4a.. 4a7ef..) x2) (aae7a.. x0 x1) (proof)
Theorem 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) (proof)
Theorem b6093.. : ∀ x0 x1 x2 . prim1 (aae7a.. 4a7ef.. x2) (aae7a.. x0 x1) ⟶ prim1 x2 x0 (proof)
Theorem 2f7aa.. : ∀ x0 x1 x2 . prim1 (aae7a.. (4ae4a.. 4a7ef..) x2) (aae7a.. x0 x1) ⟶ prim1 x2 x1 (proof)
Param iff : ο → ο → ο
Known iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem 261cc.. : ∀ x0 x1 x2 . iff (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)) (proof)
Theorem 5e53a.. : ∀ x0 x1 x2 x3 . Subq x0 x2 ⟶ Subq x1 x3 ⟶ Subq (aae7a.. x0 x1) (aae7a.. x2 x3) (proof)
Known e951d.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . prim1 x3 x0 ⟶ x1 x3 ⟶ prim1 (x2 x3) (a4c2a.. x0 x1 x2)
Theorem 2ef56.. : ∀ x0 x1 . prim1 (aae7a.. 4a7ef.. x1) x0 ⟶ prim1 x1 (e76d4.. x0) (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 a6d0f.. : ∀ x0 x1 . prim1 x1 (e76d4.. x0) ⟶ prim1 (aae7a.. 4a7ef.. x1) x0 (proof)
Theorem 36427.. : ∀ x0 x1 . prim1 (aae7a.. (4ae4a.. 4a7ef..) x1) x0 ⟶ prim1 x1 (22ca9.. x0) (proof)
Theorem 98a9e.. : ∀ x0 x1 . prim1 x1 (22ca9.. x0) ⟶ prim1 (aae7a.. (4ae4a.. 4a7ef..) x1) x0 (proof)
Theorem 5dd0a.. : ∀ x0 x1 . e76d4.. (aae7a.. x0 x1) = x0 (proof)
Theorem 40190.. : ∀ x0 x1 . 22ca9.. (aae7a.. x0 x1) = x1 (proof)
Theorem cf31f.. : ∀ x0 x1 x2 x3 . aae7a.. x0 x1 = aae7a.. x2 x3 ⟶ and (x0 = x2) (x1 = x3) (proof)
Theorem 74782.. : ∀ x0 . Subq (aae7a.. (e76d4.. x0) (22ca9.. x0)) x0 (proof)