current assets |
---|
217e4../69eba.. bday: 1478 doc published by PrGxv..Known andEandE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2Theorem e70ba..exandE_iii : ∀ x0 x1 : (ι → ι → ι) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ι . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ι . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)Theorem b35ea..exandE_iiii : ∀ x0 x1 : (ι → ι → ι → ι) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)Theorem 9132c..exandE_iio : ∀ x0 x1 : (ι → ι → ο) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ο . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ο . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)Theorem 0f4a2..exandE_iiio : ∀ x0 x1 : (ι → ι → ι → ο) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ο . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ι → ο . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)Definition Descr_iiDescr_ii := λ x0 : (ι → ι) → ο . λ x1 . Eps_i (λ x2 . ∀ x3 : ι → ι . x0 x3 ⟶ x3 x1 = x2)Known 4cb75..Eps_i_R : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (Eps_i x0)Theorem Descr_ii_propDescr_ii_prop : ∀ x0 : (ι → ι) → ο . (∀ x1 : ο . (∀ x2 : ι → ι . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ι → ι . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_ii x0) (proof)Definition Descr_iiiDescr_iii := λ x0 : (ι → ι → ι) → ο . λ x1 x2 . Eps_i (λ x3 . ∀ x4 : ι → ι → ι . x0 x4 ⟶ x4 x1 x2 = x3)Theorem Descr_iii_propDescr_iii_prop : ∀ x0 : (ι → ι → ι) → ο . (∀ x1 : ο . (∀ x2 : ι → ι → ι . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ι → ι → ι . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_iii x0) (proof)Definition Descr_iioDescr_iio := λ x0 : (ι → ι → ο) → ο . λ x1 x2 . ∀ x3 : ι → ι → ο . x0 x3 ⟶ x3 x1 x2Known prop_ext_2prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1Theorem Descr_iio_propDescr_iio_prop : ∀ x0 : (ι → ι → ο) → ο . (∀ x1 : ο . (∀ x2 : ι → ι → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ι → ι → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_iio x0) (proof)Definition Descr_Vo1Descr_Vo1 := λ x0 : (ι → ο) → ο . λ x1 . ∀ x2 : ι → ο . x0 x2 ⟶ x2 x1Theorem Descr_Vo1_propDescr_Vo1_prop : ∀ x0 : (ι → ο) → ο . (∀ x1 : ο . (∀ x2 : ι → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ι → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo1 x0) (proof)Definition Descr_Vo2Descr_Vo2 := λ x0 : ((ι → ο) → ο) → ο . λ x1 : ι → ο . ∀ x2 : (ι → ο) → ο . x0 x2 ⟶ x2 x1Theorem Descr_Vo2_propDescr_Vo2_prop : ∀ x0 : ((ι → ο) → ο) → ο . (∀ x1 : ο . (∀ x2 : (ι → ο) → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : (ι → ο) → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo2 x0) (proof)Definition Descr_Vo3Descr_Vo3 := λ x0 : (((ι → ο) → ο) → ο) → ο . λ x1 : (ι → ο) → ο . ∀ x2 : ((ι → ο) → ο) → ο . x0 x2 ⟶ x2 x1Theorem Descr_Vo3_propDescr_Vo3_prop : ∀ x0 : (((ι → ο) → ο) → ο) → ο . (∀ x1 : ο . (∀ x2 : ((ι → ο) → ο) → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ((ι → ο) → ο) → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo3 x0) (proof)Definition Descr_Vo4Descr_Vo4 := λ x0 : ((((ι → ο) → ο) → ο) → ο) → ο . λ x1 : ((ι → ο) → ο) → ο . ∀ x2 : (((ι → ο) → ο) → ο) → ο . x0 x2 ⟶ x2 x1Theorem Descr_Vo4_propDescr_Vo4_prop : ∀ x0 : ((((ι → ο) → ο) → ο) → ο) → ο . (∀ x1 : ο . (∀ x2 : (((ι → ο) → ο) → ο) → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : (((ι → ο) → ο) → ο) → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo4 x0) (proof)Definition 711f6..If_ii := λ x0 : ο . λ x1 x2 : ι → ι . λ x3 . If_i x0 (x1 x3) (x2 x3)Known 0d2f9..If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1Theorem 7c9c7..If_ii_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι . x0 ⟶ 711f6.. x0 x1 x2 = x1 (proof)Known 81513..If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2Theorem bc627..If_ii_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι . not x0 ⟶ 711f6.. x0 x1 x2 = x2 (proof)Definition 0c026..If_iii := λ x0 : ο . λ x1 x2 : ι → ι → ι . λ x3 x4 . If_i x0 (x1 x3 x4) (x2 x3 x4)Theorem ce5db..If_iii_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ι . x0 ⟶ 0c026.. x0 x1 x2 = x1 (proof)Theorem 1202f..If_iii_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ι . not x0 ⟶ 0c026.. x0 x1 x2 = x2 (proof)Definition 5011a..If_Vo1 := λ x0 : ο . λ x1 x2 : ι → ο . λ x3 . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)Known 39854..andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0Known 7c02f..andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1Known FalseEFalseE : False ⟶ ∀ x0 : ο . x0Known notEnotE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ FalseTheorem 36071..If_Vo1_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ο . x0 ⟶ 5011a.. x0 x1 x2 = x1 (proof)Known eb789..andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1Theorem 29836..If_Vo1_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ο . not x0 ⟶ 5011a.. x0 x1 x2 = x2 (proof)Definition a113b..If_iio := λ x0 : ο . λ x1 x2 : ι → ι → ο . λ x3 x4 . and (x0 ⟶ x1 x3 x4) (not x0 ⟶ x2 x3 x4)Theorem 96e82..If_iio_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ο . x0 ⟶ a113b.. x0 x1 x2 = x1 (proof)Theorem b6c73..If_iio_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ο . not x0 ⟶ a113b.. x0 x1 x2 = x2 (proof)Definition 06f01..If_Vo2 := λ x0 : ο . λ x1 x2 : (ι → ο) → ο . λ x3 : ι → ο . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)Theorem 083fe..If_Vo2_1 : ∀ x0 : ο . ∀ x1 x2 : (ι → ο) → ο . x0 ⟶ 06f01.. x0 x1 x2 = x1 (proof)Theorem d4610..If_Vo2_0 : ∀ x0 : ο . ∀ x1 x2 : (ι → ο) → ο . not x0 ⟶ 06f01.. x0 x1 x2 = x2 (proof)Definition 3dad2..If_Vo3 := λ x0 : ο . λ x1 x2 : ((ι → ο) → ο) → ο . λ x3 : (ι → ο) → ο . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)Theorem 2a734..If_Vo3_1 : ∀ x0 : ο . ∀ x1 x2 : ((ι → ο) → ο) → ο . x0 ⟶ 3dad2.. x0 x1 x2 = x1 (proof)Theorem f6f11..If_Vo3_0 : ∀ x0 : ο . ∀ x1 x2 : ((ι → ο) → ο) → ο . not x0 ⟶ 3dad2.. x0 x1 x2 = x2 (proof)Definition eb5c9..If_Vo4 := λ x0 : ο . λ x1 x2 : (((ι → ο) → ο) → ο) → ο . λ x3 : ((ι → ο) → ο) → ο . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)Theorem eadde..If_Vo4_1 : ∀ x0 : ο . ∀ x1 x2 : (((ι → ο) → ο) → ο) → ο . x0 ⟶ eb5c9.. x0 x1 x2 = x1 (proof)Theorem 4223b..If_Vo4_0 : ∀ x0 : ο . ∀ x1 x2 : (((ι → ο) → ο) → ο) → ο . not x0 ⟶ eb5c9.. x0 x1 x2 = x2 (proof)Definition 61278.. := λ x0 : ι → (ι → ι → ι) → ι → ι . λ x1 . λ x2 : ι → ι . ∀ x3 : ι → (ι → ι) → ο . (∀ x4 . ∀ x5 : ι → ι → ι . (∀ x6 . In x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2Definition 6445c..In_rec_ii := λ x0 : ι → (ι → ι → ι) → ι → ι . λ x1 . Descr_ii (61278.. x0 x1)Theorem a4d18.. : ∀ x0 : ι → (ι → ι → ι) → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 . In x3 x1 ⟶ 61278.. x0 x3 (x2 x3)) ⟶ 61278.. x0 x1 (x0 x1 x2) (proof)Theorem 7cec9.. : ∀ x0 : ι → (ι → ι → ι) → ι → ι . ∀ x1 . ∀ x2 : ι → ι . 61278.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι → ι . and (∀ x5 . In x5 x1 ⟶ 61278.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)Known 61ad0..In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . In x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1Theorem 2c9e0.. : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ι . 61278.. x0 x1 x2 ⟶ 61278.. x0 x1 x3 ⟶ x2 = x3 (proof)Theorem 3124e.. : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 61278.. x0 x1 (6445c.. x0 x1) (proof)Theorem 58891.. : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 61278.. x0 x1 (x0 x1 (6445c.. x0)) (proof)Theorem 3b5bd..In_rec_ii_eq : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 6445c.. x0 x1 = x0 x1 (6445c.. x0) (proof)Definition ca584.. := λ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . λ x1 . λ x2 : ι → ι → ι . ∀ x3 : ι → (ι → ι → ι) → ο . (∀ x4 . ∀ x5 : ι → ι → ι → ι . (∀ x6 . In x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2Definition 28408..In_rec_iii := λ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . λ x1 . Descr_iii (ca584.. x0 x1)Theorem 94633.. : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι → ι . (∀ x3 . In x3 x1 ⟶ ca584.. x0 x3 (x2 x3)) ⟶ ca584.. x0 x1 (x0 x1 x2) (proof)Theorem f2e34.. : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι . ca584.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι → ι → ι . and (∀ x5 . In x5 x1 ⟶ ca584.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)Theorem 53b27.. : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ι → ι . ca584.. x0 x1 x2 ⟶ ca584.. x0 x1 x3 ⟶ x2 = x3 (proof)Theorem c7b81.. : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ca584.. x0 x1 (28408.. x0 x1) (proof)Theorem 15004.. : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ca584.. x0 x1 (x0 x1 (28408.. x0)) (proof)Theorem fba8c..In_rec_iii_eq : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 28408.. x0 x1 = x0 x1 (28408.. x0) (proof)Definition 6f52e.. := λ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . λ x1 . λ x2 : ι → ι → ο . ∀ x3 : ι → (ι → ι → ο) → ο . (∀ x4 . ∀ x5 : ι → ι → ι → ο . (∀ x6 . In x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2Definition 03431..In_rec_iio := λ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . λ x1 . Descr_iio (6f52e.. x0 x1)Theorem 23f38.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ι → ο . (∀ x3 . In x3 x1 ⟶ 6f52e.. x0 x3 (x2 x3)) ⟶ 6f52e.. x0 x1 (x0 x1 x2) (proof)Theorem 75c04.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ο . 6f52e.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι → ι → ο . and (∀ x5 . In x5 x1 ⟶ 6f52e.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)Theorem 09ec8.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ι → ο . 6f52e.. x0 x1 x2 ⟶ 6f52e.. x0 x1 x3 ⟶ x2 = x3 (proof)Theorem e071f.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 6f52e.. x0 x1 (03431.. x0 x1) (proof)Theorem dc49b.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 6f52e.. x0 x1 (x0 x1 (03431.. x0)) (proof)Theorem ee928..In_rec_iio_eq : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 03431.. x0 x1 = x0 x1 (03431.. x0) (proof)Definition 6869c.. := λ x0 : ι → (ι → ι → ο) → ι → ο . λ x1 . λ x2 : ι → ο . ∀ x3 : ι → (ι → ο) → ο . (∀ x4 . ∀ x5 : ι → ι → ο . (∀ x6 . In x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2Definition f9c5e..In_rec_Vo1 := λ x0 : ι → (ι → ι → ο) → ι → ο . λ x1 . Descr_Vo1 (6869c.. x0 x1)Theorem 98d06.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ο . (∀ x3 . In x3 x1 ⟶ 6869c.. x0 x3 (x2 x3)) ⟶ 6869c.. x0 x1 (x0 x1 x2) (proof)Theorem fc0f8.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . ∀ x1 . ∀ x2 : ι → ο . 6869c.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι → ο . and (∀ x5 . In x5 x1 ⟶ 6869c.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)Theorem 8511d.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ο . 6869c.. x0 x1 x2 ⟶ 6869c.. x0 x1 x3 ⟶ x2 = x3 (proof)Theorem a9e6e.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 6869c.. x0 x1 (f9c5e.. x0 x1) (proof)Theorem d502e.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 6869c.. x0 x1 (x0 x1 (f9c5e.. x0)) (proof)Theorem c87be..In_rec_Vo1_eq : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . f9c5e.. x0 x1 = x0 x1 (f9c5e.. x0) (proof)Definition 59843.. := λ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . λ x1 . λ x2 : (ι → ο) → ο . ∀ x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . ∀ x5 : ι → (ι → ο) → ο . (∀ x6 . In x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2Definition c2908..In_rec_Vo2 := λ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . λ x1 . Descr_Vo2 (59843.. x0 x1)Theorem 9be4c.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 : ι → (ι → ο) → ο . (∀ x3 . In x3 x1 ⟶ 59843.. x0 x3 (x2 x3)) ⟶ 59843.. x0 x1 (x0 x1 x2) (proof)Theorem 1e053.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 : (ι → ο) → ο . 59843.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → (ι → ο) → ο . and (∀ x5 . In x5 x1 ⟶ 59843.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)Theorem edb50.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : (ι → ο) → ο . 59843.. x0 x1 x2 ⟶ 59843.. x0 x1 x3 ⟶ x2 = x3 (proof)Theorem 56b05.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 59843.. x0 x1 (c2908.. x0 x1) (proof)Theorem 71f3a.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 59843.. x0 x1 (x0 x1 (c2908.. x0)) (proof)Theorem 61a08..In_rec_Vo2_eq : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . c2908.. x0 x1 = x0 x1 (c2908.. x0) (proof)Definition 31b02.. := λ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . λ x1 . λ x2 : ((ι → ο) → ο) → ο . ∀ x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . ∀ x5 : ι → ((ι → ο) → ο) → ο . (∀ x6 . In x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2Definition 2bbaf..In_rec_Vo3 := λ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . λ x1 . Descr_Vo3 (31b02.. x0 x1)Theorem 9bae8.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . ∀ x1 . ∀ x2 : ι → ((ι → ο) → ο) → ο . (∀ x3 . In x3 x1 ⟶ 31b02.. x0 x3 (x2 x3)) ⟶ 31b02.. x0 x1 (x0 x1 x2) (proof)Theorem 8ac8a.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . ∀ x1 . ∀ x2 : ((ι → ο) → ο) → ο . 31b02.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ((ι → ο) → ο) → ο . and (∀ x5 . In x5 x1 ⟶ 31b02.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)Theorem e33bc.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ((ι → ο) → ο) → ο . 31b02.. x0 x1 x2 ⟶ 31b02.. x0 x1 x3 ⟶ x2 = x3 (proof)Theorem b5998.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 31b02.. x0 x1 (2bbaf.. x0 x1) (proof)Theorem 9f3e1.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 31b02.. x0 x1 (x0 x1 (2bbaf.. x0)) (proof)Theorem 32d2e..In_rec_Vo3_eq : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 2bbaf.. x0 x1 = x0 x1 (2bbaf.. x0) (proof)Definition 77406.. := λ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . λ x1 . λ x2 : (((ι → ο) → ο) → ο) → ο . ∀ x3 : ι → ((((ι → ο) → ο) → ο) → ο) → ο . (∀ x4 . ∀ x5 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x6 . In x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2Definition 59fb5..In_rec_Vo4 := λ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . λ x1 . Descr_Vo4 (77406.. x0 x1)Theorem 57125.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . ∀ x1 . ∀ x2 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x3 . In x3 x1 ⟶ 77406.. x0 x3 (x2 x3)) ⟶ 77406.. x0 x1 (x0 x1 x2) (proof)Theorem a7e02.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . ∀ x1 . ∀ x2 : (((ι → ο) → ο) → ο) → ο . 77406.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → (((ι → ο) → ο) → ο) → ο . and (∀ x5 . In x5 x1 ⟶ 77406.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)Theorem 6dbd6.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : (((ι → ο) → ο) → ο) → ο . 77406.. x0 x1 x2 ⟶ 77406.. x0 x1 x3 ⟶ x2 = x3 (proof)Theorem 8a2fc.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 77406.. x0 x1 (59fb5.. x0 x1) (proof)Theorem 6fbc8.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 77406.. x0 x1 (x0 x1 (59fb5.. x0)) (proof)Theorem c6e41..In_rec_Vo4_eq : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 59fb5.. x0 x1 = x0 x1 (59fb5.. x0) (proof)Definition 1ce4f..incl_0_1 := λ x0 x1 . In x1 x0Definition d97e3..In_1 := λ x0 x1 : ι → ο . ∀ x2 : ο . (∀ x3 . and (x0 = 1ce4f.. x3) (x1 x3) ⟶ x2) ⟶ x2Definition 407b5..incl_1_2 := λ x0 x1 : ι → ο . d97e3.. x1 x0Definition 3a6d0..In_2 := λ x0 x1 : (ι → ο) → ο . ∀ x2 : ο . (∀ x3 : ι → ο . and (x0 = 407b5.. x3) (x1 x3) ⟶ x2) ⟶ x2Definition a4b00..incl_2_3 := λ x0 x1 : (ι → ο) → ο . 3a6d0.. x1 x0Definition e6217..In_3 := λ x0 x1 : ((ι → ο) → ο) → ο . ∀ x2 : ο . (∀ x3 : (ι → ο) → ο . and (x0 = a4b00.. x3) (x1 x3) ⟶ x2) ⟶ x2Definition a327b..incl_3_4 := λ x0 x1 : ((ι → ο) → ο) → ο . e6217.. x1 x0Definition 8fddf..In_4 := λ x0 x1 : (((ι → ο) → ο) → ο) → ο . ∀ x2 : ο . (∀ x3 : ((ι → ο) → ο) → ο . and (x0 = a327b.. x3) (x1 x3) ⟶ x2) ⟶ x2Theorem 289f7..In_1_I : ∀ x0 . ∀ x1 : ι → ο . x1 x0 ⟶ d97e3.. (1ce4f.. x0) x1 (proof)Theorem 4487e..In_1_E : ∀ x0 x1 : ι → ο . d97e3.. x0 x1 ⟶ ∀ x2 : (ι → ο) → ο . (∀ x3 . x1 x3 ⟶ x2 (1ce4f.. x3)) ⟶ x2 x0 (proof)Known 535f2..set_ext_2 : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ (∀ x2 . In x2 x1 ⟶ In x2 x0) ⟶ x0 = x1Theorem c0781..incl_0_1_inj : ∀ x0 x1 . 1ce4f.. x0 = 1ce4f.. x1 ⟶ x0 = x1 (proof)Theorem 8bd78..In_1_up : ∀ x0 x1 . In x0 x1 ⟶ d97e3.. (1ce4f.. x0) (1ce4f.. x1) (proof)Theorem 3172a..In_1_down : ∀ x0 x1 . d97e3.. (1ce4f.. x0) (1ce4f.. x1) ⟶ In x0 x1 (proof)Theorem 5b9f0..In_2_I : ∀ x0 : ι → ο . ∀ x1 : (ι → ο) → ο . x1 x0 ⟶ 3a6d0.. (407b5.. x0) x1 (proof)Theorem 724a1..In_2_E : ∀ x0 x1 : (ι → ο) → ο . 3a6d0.. x0 x1 ⟶ ∀ x2 : ((ι → ο) → ο) → ο . (∀ x3 : ι → ο . x1 x3 ⟶ x2 (407b5.. x3)) ⟶ x2 x0 (proof)Theorem 94a3d..incl_1_2_inj : ∀ x0 x1 : ι → ο . 407b5.. x0 = 407b5.. x1 ⟶ x0 = x1 (proof)Theorem 9b744..In_2_up : ∀ x0 x1 : ι → ο . d97e3.. x0 x1 ⟶ 3a6d0.. (407b5.. x0) (407b5.. x1) (proof)Theorem d6cc7..In_2_down : ∀ x0 x1 : ι → ο . 3a6d0.. (407b5.. x0) (407b5.. x1) ⟶ d97e3.. x0 x1 (proof)Theorem 7abdf..In_3_I : ∀ x0 : (ι → ο) → ο . ∀ x1 : ((ι → ο) → ο) → ο . x1 x0 ⟶ e6217.. (a4b00.. x0) x1 (proof)Theorem af1a5..In_3_E : ∀ x0 x1 : ((ι → ο) → ο) → ο . e6217.. x0 x1 ⟶ ∀ x2 : (((ι → ο) → ο) → ο) → ο . (∀ x3 : (ι → ο) → ο . x1 x3 ⟶ x2 (a4b00.. x3)) ⟶ x2 x0 (proof)Theorem ea98f..incl_2_3_inj : ∀ x0 x1 : (ι → ο) → ο . a4b00.. x0 = a4b00.. x1 ⟶ x0 = x1 (proof)Theorem 37ad7..In_3_up : ∀ x0 x1 : (ι → ο) → ο . 3a6d0.. x0 x1 ⟶ e6217.. (a4b00.. x0) (a4b00.. x1) (proof)Theorem db604..In_3_down : ∀ x0 x1 : (ι → ο) → ο . e6217.. (a4b00.. x0) (a4b00.. x1) ⟶ 3a6d0.. x0 x1 (proof)Theorem 483c0..In_4_I : ∀ x0 : ((ι → ο) → ο) → ο . ∀ x1 : (((ι → ο) → ο) → ο) → ο . x1 x0 ⟶ 8fddf.. (a327b.. x0) x1 (proof)Theorem 272c7..In_4_E : ∀ x0 x1 : (((ι → ο) → ο) → ο) → ο . 8fddf.. x0 x1 ⟶ ∀ x2 : ((((ι → ο) → ο) → ο) → ο) → ο . (∀ x3 : ((ι → ο) → ο) → ο . x1 x3 ⟶ x2 (a327b.. x3)) ⟶ x2 x0 (proof)Theorem 79850..incl_3_4_inj : ∀ x0 x1 : ((ι → ο) → ο) → ο . a327b.. x0 = a327b.. x1 ⟶ x0 = x1 (proof)Theorem b7736..In_4_up : ∀ x0 x1 : ((ι → ο) → ο) → ο . e6217.. x0 x1 ⟶ 8fddf.. (a327b.. x0) (a327b.. x1) (proof)Theorem edf38..In_4_down : ∀ x0 x1 : ((ι → ο) → ο) → ο . 8fddf.. (a327b.. x0) (a327b.. x1) ⟶ e6217.. x0 x1 (proof)
|
|