Proofgold Address

Param add_nat^add_nat : ι → ι → ι
Param u4 : ι
Param ordsucc^ordsucc : ι → ι
Definition u1 := 1
Definition u5 := ordsucc u4
Param nat_p^nat_p : ι → ο
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_0^nat_0 : nat_p 0
Known add_nat_0R^add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Theorem 893fe.. : add_nat u4 u1 = u5 (proof)
Definition u6 := ordsucc u5
Theorem 561b1.. : add_nat u5 u1 = u6 (proof)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known nat_inv^nat_inv : ∀ x0 . nat_p x0 ⟶ or (x0 = 0) (∀ x1 : ο . (∀ x2 . and (nat_p x2) (x0 = ordsucc x2) ⟶ x1) ⟶ x1)
Known nat_p_trans^nat_p_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ nat_p x1
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known nat_trans^nat_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Theorem 80d07.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ ordsucc x0 ⟶ or (x1 = 0) (∀ x2 : ο . (∀ x3 . and (x3 ∈ x0) (x1 = ordsucc x3) ⟶ x2) ⟶ x2) (proof)
Definition bij^bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Definition equip^equip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3 ⟶ x2) ⟶ x2
Param ordinal^ordinal : ι → ο
Definition inj^inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Definition False^False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known EmptyE^EmptyE : ∀ x0 . nIn x0 0
Known least_ordinal_ex^{least_ordinal_ex} : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . and (ordinal x2) (x0 x2) ⟶ x1) ⟶ x1) ⟶ ∀ x1 : ο . (∀ x2 . and (and (ordinal x2) (x0 x2)) (∀ x3 . x3 ∈ x2 ⟶ not (x0 x3)) ⟶ x1) ⟶ x1
Param setminus^setminus : ι → ι → ι
Param Sing^Sing : ι → ι
Known equip_sym^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Known 9c223..^{equip_ordsucc_remove1} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ equip x0 (ordsucc x1) ⟶ equip (setminus x0 (Sing x2)) x1
Known setminusE1^setminusE1 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ x2 ∈ x0
Param nat_primrec^nat_primrec : ι → (ι → ι → ι) → ι → ι
Known nat_primrec_0^{nat_primrec_0} : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Known nat_primrec_S^{nat_primrec_S} : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2 ⟶ nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2)
Known setminusE2^setminusE2 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ nIn x2 x1
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Known setminusE^setminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Known ordinal_trichotomy_or_impred^{ordinal_trichotomy_or_impred} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 : ο . (x0 ∈ x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (x1 ∈ x0 ⟶ x2) ⟶ x2
Known nat_p_ordinal^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Known In_no2cycle^In_no2cycle : ∀ x0 x1 . x0 ∈ x1 ⟶ x1 ∈ x0 ⟶ False
Known nat_ordsucc_in_ordsucc^{nat_ordsucc_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ ordsucc x0
Theorem e802a.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . equip x0 x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ ordinal x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι . and (inj x0 x1 x3) (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x4 ⟶ x3 x5 ∈ x3 x4) ⟶ x2) ⟶ x2 (proof)
Definition atleastp^atleastp := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3 ⟶ x2) ⟶ x2
Known d2050.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ equip x0 (prim5 x0 x1)
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Theorem 9a4b0.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . atleastp x0 x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ ordinal x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι . and (inj x0 x1 x3) (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x4 ⟶ x3 x5 ∈ x3 x4) ⟶ x2) ⟶ x2 (proof)
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Known nat_3^nat_3 : nat_p 3
Known In_0_3^In_0_3 : 0 ∈ 3
Known In_1_3^In_1_3 : 1 ∈ 3
Known In_2_3^In_2_3 : 2 ∈ 3
Known In_0_1^In_0_1 : 0 ∈ 1
Known In_1_2^In_1_2 : 1 ∈ 2
Theorem 865bf.. : ∀ x0 . atleastp u3 x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ ordinal x1) ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 ∈ x3 ⟶ x3 ∈ x4 ⟶ x1) ⟶ x1 (proof)
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Theorem 2ec5a.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . atleastp (ordsucc x0) x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ ordinal x2) ⟶ ∀ x2 : ο . (∀ x3 x4 . equip x0 x3 ⟶ x4 ∈ x1 ⟶ x3 ⊆ x1 ⟶ x3 ⊆ x4 ⟶ x2) ⟶ x2 (proof)
Param u17 : ι
Definition u18 := ordsucc u17
Known c5b55.. : 0 ∈ u17
Theorem a7790.. : 0 ∈ u18 (proof)
Known f6e42.. : u1 ∈ u17
Theorem b8ca4.. : u1 ∈ u18 (proof)
Known 9502b.. : u2 ∈ u17
Theorem a878b.. : u2 ∈ u18 (proof)
Known 35c0a.. : u3 ∈ u17
Theorem d07d6.. : u3 ∈ u18 (proof)
Known 793dd.. : u4 ∈ u17
Theorem 6d81a.. : u4 ∈ u18 (proof)
Known 79c48.. : u5 ∈ u17
Theorem e36c4.. : u5 ∈ u18 (proof)
Known b3205.. : u6 ∈ u17
Theorem 79cb7.. : u6 ∈ u18 (proof)
Param u7 : ι
Known 51ef0.. : u7 ∈ u17
Theorem 56aca.. : u7 ∈ u18 (proof)
Param u8 : ι
Known 6a4e9.. : u8 ∈ u17
Theorem fbe02.. : u8 ∈ u18 (proof)
Param u9 : ι
Known fd1a6.. : u9 ∈ u17
Theorem 1a5f0.. : u9 ∈ u18 (proof)
Param u10 : ι
Known e886d.. : u10 ∈ u17
Theorem f5af9.. : u10 ∈ u18 (proof)
Param u11 : ι
Known e57ea.. : u11 ∈ u17
Theorem c2b10.. : u11 ∈ u18 (proof)
Param u12 : ι
Known a1a10.. : u12 ∈ u17
Theorem 6591b.. : u12 ∈ u18 (proof)
Param u13 : ι
Known 7315d.. : u13 ∈ u17
Theorem c4f20.. : u13 ∈ u18 (proof)
Param u14 : ι
Known 35e01.. : u14 ∈ u17
Theorem 755d2.. : u14 ∈ u18 (proof)
Param u15 : ι
Known 31b8d.. : u15 ∈ u17
Theorem 0f93a.. : u15 ∈ u18 (proof)
Param u16 : ι
Known dfaf3.. : u16 ∈ u17
Theorem 7e227.. : u16 ∈ u18 (proof)
Theorem e0489.. : u17 ∈ u18 (proof)
Definition u19 := ordsucc u18
Theorem ee3ac.. : 0 ∈ u19 (proof)
Theorem 7d131.. : u1 ∈ u19 (proof)
Theorem b67e6.. : u2 ∈ u19 (proof)
Theorem 8cb19.. : u3 ∈ u19 (proof)
Theorem 1cffe.. : u4 ∈ u19 (proof)
Theorem f4c5f.. : u5 ∈ u19 (proof)
Theorem 621e0.. : u6 ∈ u19 (proof)
Theorem f0487.. : u7 ∈ u19 (proof)
Theorem 4d195.. : u8 ∈ u19 (proof)
Theorem 684da.. : u9 ∈ u19 (proof)
Theorem 142ec.. : u10 ∈ u19 (proof)
Theorem 58234.. : u11 ∈ u19 (proof)
Theorem 4f2ac.. : u12 ∈ u19 (proof)
Theorem 74754.. : u13 ∈ u19 (proof)
Theorem 82290.. : u14 ∈ u19 (proof)
Theorem f77c1.. : u15 ∈ u19 (proof)
Theorem 8d5b9.. : u16 ∈ u19 (proof)
Theorem a6826.. : u17 ∈ u19 (proof)
Theorem 25029.. : u18 ∈ u19 (proof)
Definition u20 := ordsucc u19
Theorem 4d7d5.. : 0 ∈ u20 (proof)
Theorem 8154f.. : u1 ∈ u20 (proof)
Theorem 2a239.. : u2 ∈ u20 (proof)
Theorem 112c4.. : u3 ∈ u20 (proof)
Theorem ae167.. : u4 ∈ u20 (proof)
Theorem d15f4.. : u5 ∈ u20 (proof)
Theorem 6a68d.. : u6 ∈ u20 (proof)
Theorem c3da7.. : u7 ∈ u20 (proof)
Theorem 67123.. : u8 ∈ u20 (proof)
Theorem 63ab7.. : u9 ∈ u20 (proof)
Theorem 1c8f4.. : u10 ∈ u20 (proof)
Theorem 96d5f.. : u11 ∈ u20 (proof)
Theorem f3e75.. : u12 ∈ u20 (proof)
Theorem b5fe0.. : u13 ∈ u20 (proof)
Theorem 985c5.. : u14 ∈ u20 (proof)
Theorem 2a2c2.. : u15 ∈ u20 (proof)
Theorem def07.. : u16 ∈ u20 (proof)
Theorem de57f.. : u17 ∈ u20 (proof)
Theorem 94188.. : u18 ∈ u20 (proof)
Theorem 9ea5b.. : u19 ∈ u20 (proof)
Definition u21 := ordsucc u20
Theorem 179f3.. : 0 ∈ u21 (proof)
Theorem 07fdb.. : u1 ∈ u21 (proof)
Theorem c25ea.. : u2 ∈ u21 (proof)
Theorem 0750b.. : u3 ∈ u21 (proof)
Theorem 701a9.. : u4 ∈ u21 (proof)
Theorem 0dc69.. : u5 ∈ u21 (proof)
Theorem 1d1d3.. : u6 ∈ u21 (proof)
Theorem 0b77c.. : u7 ∈ u21 (proof)
Theorem 5fc29.. : u8 ∈ u21 (proof)
Theorem 4b046.. : u9 ∈ u21 (proof)
Theorem 46da3.. : u10 ∈ u21 (proof)
Theorem 3ad1f.. : u11 ∈ u21 (proof)
Theorem 07061.. : u12 ∈ u21 (proof)
Theorem d16a4.. : u13 ∈ u21 (proof)
Theorem a6788.. : u14 ∈ u21 (proof)
Theorem ce294.. : u15 ∈ u21 (proof)
Theorem 20f4b.. : u16 ∈ u21 (proof)
Theorem d5f90.. : u17 ∈ u21 (proof)
Theorem 08993.. : u18 ∈ u21 (proof)
Theorem b8dfd.. : u19 ∈ u21 (proof)
Theorem c955e.. : u20 ∈ u21 (proof)
Theorem edc13.. : u18 = u19 ⟶ ∀ x0 : ο . x0 (proof)
Theorem 42954.. : u17 = u20 ⟶ ∀ x0 : ο . x0 (proof)
Known nat_17^nat_17 : nat_p u17
Theorem 2d2af.. : u12 ⊆ u17 (proof)
Known 2669c.. : nat_p u20
Theorem 2d95b.. : u17 ⊆ u20 (proof)
Known e8a0a.. : nat_p u21
Theorem c1d56.. : u17 ⊆ u21 (proof)
Param ap^ap : ι → ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Param If_i^If_i : ο → ι → ι → ι
Definition e7a80.. := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . ap (lam 22 (λ x23 . If_i (x23 = 0) x1 (If_i (x23 = 1) x23 (If_i (x23 = 2) x3 (If_i (x23 = 3) x4 (If_i (x23 = 4) x5 (If_i (x23 = 5) x6 (If_i (x23 = 6) x7 (If_i (x23 = 7) x8 (If_i (x23 = 8) x9 (If_i (x23 = 9) x10 (If_i (x23 = 10) x11 (If_i (x23 = 11) x12 (If_i (x23 = 12) x13 (If_i (x23 = 13) x14 (If_i (x23 = 14) x15 (If_i (x23 = 15) x16 (If_i (x23 = 16) x17 (If_i (x23 = 17) x18 (If_i (x23 = 18) x19 (If_i (x23 = 19) x20 (If_i (x23 = 20) x21 x22)))))))))))))))))))))) x0
Definition 00974.. := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x5) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x6) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x7) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x8) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x9) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x10) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x11) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x12) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x13) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x14) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x15) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x16) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x17) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x18) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x19) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x20) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x21) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x22) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x23) ⟶ x1 x0
Definition 94591.. := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x2 x3 . x0 (x1 x2 x2 x2 x3 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x3 x2 x3 x2 x3 x3 x3 x3) (x1 x2 x2 x3 x2 x3 x3 x2 x3 x3 x3 x3 x2 x2 x3 x3 x3 x3 x3 x3 x3 x3 x2) (x1 x2 x3 x2 x2 x3 x2 x3 x3 x2 x3 x3 x3 x3 x3 x2 x3 x3 x3 x3 x3 x3 x2) (x1 x3 x2 x2 x2 x2 x3 x3 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3 x3) (x1 x3 x3 x3 x2 x2 x2 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3) (x1 x3 x3 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x3 x3 x3 x3 x2 x3) (x1 x3 x2 x3 x3 x2 x3 x2 x2 x2 x3 x3 x3 x3 x3 x2 x3 x3 x3 x3 x3 x2 x3) (x1 x2 x3 x3 x3 x3 x2 x2 x2 x3 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3 x3 x3) (x1 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3 x2 x2 x2 x3 x3 x3 x3 x2 x3 x3 x3) (x1 x3 x3 x3 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x3 x3 x2 x3 x3 x3 x3 x2 x3) (x1 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x2 x3 x3 x2 x2 x3 x3 x3 x3 x3 x3 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x2 x3 x3 x2 x2 x3 x2 x3 x3 x3 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x2 x3 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3) (x1 x3 x3 x3 x2 x3 x3 x3 x2 x2 x3 x2 x3 x3 x2 x3 x3 x2 x3 x3 x2 x3 x3) (x1 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3 x2 x2 x3 x3 x2 x3 x2 x3 x3 x2 x3 x3) (x1 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x2 x3 x3) (x1 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x2 x2 x2 x2 x2 x2 x3 x3 x3 x2) (x1 x2 x3 x3 x2 x3 x3 x3 x3 x3 x3 x3 x2 x3 x3 x3 x3 x2 x2 x2 x3 x2 x3) (x1 x3 x3 x3 x3 x2 x3 x3 x2 x2 x3 x3 x3 x3 x3 x3 x3 x3 x2 x2 x2 x3 x2) (x1 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x2 x2 x2 x2 x3 x3 x2 x2 x2 x3) (x1 x3 x3 x3 x3 x3 x2 x2 x3 x3 x2 x3 x3 x3 x3 x3 x3 x3 x2 x3 x2 x2 x2) (x1 x3 x2 x2 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x2 x3 x2 x3 x2 x2)
Param u22 : ι
Definition 9043a.. := λ x0 x1 . x0 ∈ u22 ⟶ x1 ∈ u22 ⟶ 94591.. (e7a80.. x0) (e7a80.. x1) = λ x3 x4 . x3