Proofgold Signed Transaction

Known 21d45..^Loop_def : Loop = λ x1 . λ x2 x3 x4 : ι → ι → ι . λ x5 . and (and (and (and (binop_on x1 x2) (binop_on x1 x3)) (binop_on x1 x4)) (∀ x6 . In x6 x1 ⟶ and (x2 x5 x6 = x6) (x2 x6 x5 = x6))) (∀ x6 . In x6 x1 ⟶ ∀ x7 . In x7 x1 ⟶ and (and (and (x3 x6 (x2 x6 x7) = x7) (x2 x6 (x3 x6 x7) = x7)) (x4 (x2 x6 x7) x7 = x6)) (x2 (x4 x6 x7) x7 = x6))
Known 1bd08..^and5I : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ and (and (and (and x0 x1) x2) x3) x4
Theorem 46237..^LoopI : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . binop_on x0 x1 ⟶ binop_on x0 x2 ⟶ binop_on x0 x3 ⟶ (∀ x5 . In x5 x0 ⟶ and (x1 x4 x5 = x5) (x1 x5 x4 = x5)) ⟶ (∀ x5 . In x5 x0 ⟶ ∀ x6 . In x6 x0 ⟶ and (and (and (x2 x5 (x1 x5 x6) = x6) (x1 x5 (x2 x5 x6) = x6)) (x3 (x1 x5 x6) x6 = x5)) (x1 (x3 x5 x6) x6 = x5)) ⟶ Loop x0 x1 x2 x3 x4 (proof)
Known d5e32..^and5E : ∀ x0 x1 x2 x3 x4 : ο . and (and (and (and x0 x1) x2) x3) x4 ⟶ ∀ x5 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5) ⟶ x5
Theorem bca1a..^LoopE : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . Loop x0 x1 x2 x3 x4 ⟶ ∀ x5 : ο . (binop_on x0 x1 ⟶ binop_on x0 x2 ⟶ binop_on x0 x3 ⟶ (∀ x6 . In x6 x0 ⟶ and (x1 x4 x6 = x6) (x1 x6 x4 = x6)) ⟶ (∀ x6 . In x6 x0 ⟶ ∀ x7 . In x7 x0 ⟶ and (and (and (x2 x6 (x1 x6 x7) = x7) (x1 x6 (x2 x6 x7) = x7)) (x3 (x1 x6 x7) x7 = x6)) (x1 (x3 x6 x7) x7 = x6)) ⟶ x5) ⟶ x5 (proof)
Known 28be2..^{Loop_with_defs_def} : Loop_with_defs = λ x1 . λ x2 x3 x4 : ι → ι → ι . λ x5 . λ x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι . λ x8 : ι → ι → ι . λ x9 x10 : ι → ι → ι → ι . λ x11 x12 x13 x14 : ι → ι → ι . and (and (and (and (Loop x1 x2 x3 x4 x5) (∀ x15 . In x15 x1 ⟶ ∀ x16 . In x16 x1 ⟶ x6 x15 x16 = x3 (x2 x16 x15) (x2 x15 x16))) (∀ x15 . In x15 x1 ⟶ ∀ x16 . In x16 x1 ⟶ ∀ x17 . In x17 x1 ⟶ x7 x15 x16 x17 = x3 (x2 x15 (x2 x16 x17)) (x2 (x2 x15 x16) x17))) (∀ x15 . In x15 x1 ⟶ ∀ x16 . In x16 x1 ⟶ and (and (and (and (x8 x15 x16 = x3 x15 (x2 x16 x15)) (x11 x15 x16 = x2 x15 (x2 x16 (x3 x15 x5)))) (x12 x15 x16 = x2 (x2 (x4 x5 x15) x16) x15)) (x13 x15 x16 = x2 (x3 x15 x16) (x3 (x3 x15 x5) x5))) (x14 x15 x16 = x2 (x4 x5 (x4 x5 x15)) (x4 x16 x15)))) (∀ x15 . In x15 x1 ⟶ ∀ x16 . In x16 x1 ⟶ ∀ x17 . In x17 x1 ⟶ and (x9 x15 x16 x17 = x3 (x2 x16 x15) (x2 x16 (x2 x15 x17))) (x10 x15 x16 x17 = x4 (x2 (x2 x17 x15) x16) (x2 x15 x16)))
Theorem 20499..^{Loop_with_defs_I} : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop x0 x1 x2 x3 x4 ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ x5 x14 x15 = x2 (x1 x15 x14) (x1 x14 x15)) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ x6 x14 x15 x16 = x2 (x1 x14 (x1 x15 x16)) (x1 (x1 x14 x15) x16)) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ and (and (and (and (x7 x14 x15 = x2 x14 (x1 x15 x14)) (x10 x14 x15 = x1 x14 (x1 x15 (x2 x14 x4)))) (x11 x14 x15 = x1 (x1 (x3 x4 x14) x15) x14)) (x12 x14 x15 = x1 (x2 x14 x15) (x2 (x2 x14 x4) x4))) (x13 x14 x15 = x1 (x3 x4 (x3 x4 x14)) (x3 x15 x14))) ⟶ (∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ and (x8 x14 x15 x16 = x2 (x1 x15 x14) (x1 x15 (x1 x14 x16))) (x9 x14 x15 x16 = x3 (x1 (x1 x16 x14) x15) (x1 x14 x15))) ⟶ Loop_with_defs x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 (proof)
Theorem bfa6d..^{Loop_with_defs_E} : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ ∀ x14 : ο . (Loop x0 x1 x2 x3 x4 ⟶ (∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ x5 x15 x16 = x2 (x1 x16 x15) (x1 x15 x16)) ⟶ (∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ x6 x15 x16 x17 = x2 (x1 x15 (x1 x16 x17)) (x1 (x1 x15 x16) x17)) ⟶ (∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ and (and (and (and (x7 x15 x16 = x2 x15 (x1 x16 x15)) (x10 x15 x16 = x1 x15 (x1 x16 (x2 x15 x4)))) (x11 x15 x16 = x1 (x1 (x3 x4 x15) x16) x15)) (x12 x15 x16 = x1 (x2 x15 x16) (x2 (x2 x15 x4) x4))) (x13 x15 x16 = x1 (x3 x4 (x3 x4 x15)) (x3 x16 x15))) ⟶ (∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ and (x8 x15 x16 x17 = x2 (x1 x16 x15) (x1 x16 (x1 x15 x17))) (x9 x15 x16 x17 = x3 (x1 (x1 x17 x15) x16) (x1 x15 x16))) ⟶ x14) ⟶ x14 (proof)
Known c779b..^{Loop_with_defs_cex1_def} : Loop_with_defs_cex1 = λ x1 . λ x2 x3 x4 : ι → ι → ι . λ x5 . λ x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι . λ x8 : ι → ι → ι . λ x9 x10 : ι → ι → ι → ι . λ x11 x12 x13 x14 : ι → ι → ι . and (Loop_with_defs x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) (∀ x15 : ο . (∀ x16 . and (In x16 x1) (∀ x17 : ο . (∀ x18 . and (In x18 x1) (∀ x19 : ο . (∀ x20 . and (In x20 x1) (∀ x21 : ο . (∀ x22 . and (In x22 x1) (not (x6 (x2 (x3 (x9 x18 x20 x16) x5) x16) x22 = x5)) ⟶ x21) ⟶ x21) ⟶ x19) ⟶ x19) ⟶ x17) ⟶ x17) ⟶ x15) ⟶ x15)
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem c7614..^{Loop_with_defs_cex1_I0} : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ (∀ x14 : ο . (∀ x15 . and (In x15 x0) (∀ x16 : ο . (∀ x17 . and (In x17 x0) (∀ x18 : ο . (∀ x19 . and (In x19 x0) (∀ x20 : ο . (∀ x21 . and (In x21 x0) (not (x5 (x1 (x2 (x8 x17 x19 x15) x4) x15) x21 = x4)) ⟶ x20) ⟶ x20) ⟶ x18) ⟶ x18) ⟶ x16) ⟶ x16) ⟶ x14) ⟶ x14) ⟶ Loop_with_defs_cex1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 (proof)
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem 051f2..^{Loop_with_defs_cex1_E0} : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs_cex1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ ∀ x14 : ο . (Loop_with_defs x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ (∀ x15 : ο . (∀ x16 . and (In x16 x0) (∀ x17 : ο . (∀ x18 . and (In x18 x0) (∀ x19 : ο . (∀ x20 . and (In x20 x0) (∀ x21 : ο . (∀ x22 . and (In x22 x0) (not (x5 (x1 (x2 (x8 x18 x20 x16) x4) x16) x22 = x4)) ⟶ x21) ⟶ x21) ⟶ x19) ⟶ x19) ⟶ x17) ⟶ x17) ⟶ x15) ⟶ x15) ⟶ x14) ⟶ x14 (proof)
Theorem 9d0a4..^{Loop_with_defs_cex1_I} : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . ∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ Loop_with_defs x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ not (x5 (x1 (x2 (x8 x15 x16 x14) x4) x14) x17 = x4) ⟶ Loop_with_defs_cex1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 (proof)
Theorem 0ef46..^andE_imp : ∀ x0 x1 x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ and x0 x1 ⟶ x2 (proof)
Known 37124..^orE : ∀ x0 x1 : ο . or x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Theorem 60f50..^orE_imp : ∀ x0 x1 x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ or x0 x1 ⟶ x2 (proof)
Theorem 1449b..^{Loop_with_defs_cex1_E} : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs_cex1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ ∀ x14 : ο . (∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ Loop_with_defs x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ not (x5 (x1 (x2 (x8 x16 x17 x15) x4) x15) x18 = x4) ⟶ x14) ⟶ x14 (proof)
Known 3ab3c..^{Loop_with_defs_cex2_def} : Loop_with_defs_cex2 = λ x1 . λ x2 x3 x4 : ι → ι → ι . λ x5 . λ x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι . λ x8 : ι → ι → ι . λ x9 x10 : ι → ι → ι → ι . λ x11 x12 x13 x14 : ι → ι → ι . and (Loop_with_defs x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) (∀ x15 : ο . (∀ x16 . and (In x16 x1) (∀ x17 : ο . (∀ x18 . and (In x18 x1) (∀ x19 : ο . (∀ x20 . and (In x20 x1) (∀ x21 : ο . (∀ x22 . and (In x22 x1) (∀ x23 : ο . (∀ x24 . and (In x24 x1) (not (x7 x24 (x2 (x4 x5 x16) (x10 x18 x20 x16)) x22 = x5)) ⟶ x23) ⟶ x23) ⟶ x21) ⟶ x21) ⟶ x19) ⟶ x19) ⟶ x17) ⟶ x17) ⟶ x15) ⟶ x15)
Theorem 0e1bb..^{Loop_with_defs_cex2_I0} : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ (∀ x14 : ο . (∀ x15 . and (In x15 x0) (∀ x16 : ο . (∀ x17 . and (In x17 x0) (∀ x18 : ο . (∀ x19 . and (In x19 x0) (∀ x20 : ο . (∀ x21 . and (In x21 x0) (∀ x22 : ο . (∀ x23 . and (In x23 x0) (not (x6 x23 (x1 (x3 x4 x15) (x9 x17 x19 x15)) x21 = x4)) ⟶ x22) ⟶ x22) ⟶ x20) ⟶ x20) ⟶ x18) ⟶ x18) ⟶ x16) ⟶ x16) ⟶ x14) ⟶ x14) ⟶ Loop_with_defs_cex2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 (proof)
Theorem 37059..^{Loop_with_defs_cex2_E0} : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs_cex2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ ∀ x14 : ο . (Loop_with_defs x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ (∀ x15 : ο . (∀ x16 . and (In x16 x0) (∀ x17 : ο . (∀ x18 . and (In x18 x0) (∀ x19 : ο . (∀ x20 . and (In x20 x0) (∀ x21 : ο . (∀ x22 . and (In x22 x0) (∀ x23 : ο . (∀ x24 . and (In x24 x0) (not (x6 x24 (x1 (x3 x4 x16) (x9 x18 x20 x16)) x22 = x4)) ⟶ x23) ⟶ x23) ⟶ x21) ⟶ x21) ⟶ x19) ⟶ x19) ⟶ x17) ⟶ x17) ⟶ x15) ⟶ x15) ⟶ x14) ⟶ x14 (proof)
Theorem 7054a..^{Loop_with_defs_cex2_I} : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . ∀ x14 . In x14 x0 ⟶ ∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ Loop_with_defs x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ not (x6 x18 (x1 (x3 x4 x14) (x9 x15 x16 x14)) x17 = x4) ⟶ Loop_with_defs_cex2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 (proof)
Theorem 9c580..^{Loop_with_defs_cex2_E} : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs_cex2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ ∀ x14 : ο . (∀ x15 . In x15 x0 ⟶ ∀ x16 . In x16 x0 ⟶ ∀ x17 . In x17 x0 ⟶ ∀ x18 . In x18 x0 ⟶ ∀ x19 . In x19 x0 ⟶ Loop_with_defs x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ not (x6 x19 (x1 (x3 x4 x15) (x9 x16 x17 x15)) x18 = x4) ⟶ x14) ⟶ x14 (proof)
Known 86824..^binop_on_I : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ In (x1 x2 x3) x0) ⟶ binop_on x0 x1
Known 0978b..^In_0_1 : In 0 1
Theorem d5c68..^binop_on_1 : binop_on 1 (λ x0 x1 . 0) (proof)
Known e51a8..^cases_1 : ∀ x0 . In x0 1 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 x0
Known 22d81..^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Theorem 2b4af..^Trivial_Loop : Loop 1 (λ x0 x1 . 0) (λ x0 x1 . 0) (λ x0 x1 . 0) 0 (proof)
Definition b97a8..^{binop_table_2} := λ x0 x1 x2 x3 x4 . ap (ap (lam 2 (λ x5 . If_i (x5 = 0) (lam 2 (λ x6 . If_i (x6 = 0) x0 x1)) (lam 2 (λ x6 . If_i (x6 = 0) x2 x3)))) x4)
Known 08193..^tuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Theorem 3a021..^{binop_table_2_0_0} : ∀ x0 x1 x2 x3 . b97a8.. x0 x1 x2 x3 0 0 = x0 (proof)
Known 66870..^tuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Theorem 44801..^{binop_table_2_0_1} : ∀ x0 x1 x2 x3 . b97a8.. x0 x1 x2 x3 0 1 = x1 (proof)
Theorem 80777..^{binop_table_2_1_0} : ∀ x0 x1 x2 x3 . b97a8.. x0 x1 x2 x3 1 0 = x2 (proof)
Theorem 263ce..^{binop_table_2_1_1} : ∀ x0 x1 x2 x3 . b97a8.. x0 x1 x2 x3 1 1 = x3 (proof)
Known 3ad28..^cases_2 : ∀ x0 . In x0 2 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 x0
Theorem be9c9..^{binop_table_on_2} : ∀ x0 . In x0 2 ⟶ ∀ x1 . In x1 2 ⟶ ∀ x2 . In x2 2 ⟶ ∀ x3 . In x3 2 ⟶ binop_on 2 (b97a8.. x0 x1 x2 x3) (proof)
Known 0863e..^In_0_2 : In 0 2
Known 0a117..^In_1_2 : In 1 2
Theorem 1f439..^{Z2_table_binop_on_2} : binop_on 2 (b97a8.. 0 1 1 0) (proof)
Theorem e7c7b..^Z2_Loop : Loop 2 (b97a8.. 0 1 1 0) (b97a8.. 0 1 1 0) (b97a8.. 0 1 1 0) 0 (proof)
Definition 17ce0..^{binop_table_3} := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . ap (ap (lam 3 (λ x10 . If_i (x10 = 0) (lam 3 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) x1 x2))) (If_i (x10 = 1) (lam 3 (λ x11 . If_i (x11 = 0) x3 (If_i (x11 = 1) x4 x5))) (lam 3 (λ x11 . If_i (x11 = 0) x6 (If_i (x11 = 1) x7 x8)))))) x9)
Known bfdfa..^tuple_3_0_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 0 = x0
Theorem 32a3f..^{binop_table_3_0_0} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . 17ce0.. x0 x1 x2 x3 x4 x5 x6 x7 x8 0 0 = x0 (proof)
Known 96b06..^tuple_3_1_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 1 = x1
Theorem d4f93..^{binop_table_3_0_1} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . 17ce0.. x0 x1 x2 x3 x4 x5 x6 x7 x8 0 1 = x1 (proof)
Known 1edca..^tuple_3_2_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 2 = x2
Theorem 7375f..^{binop_table_3_0_2} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . 17ce0.. x0 x1 x2 x3 x4 x5 x6 x7 x8 0 2 = x2 (proof)
Theorem 2eb00..^{binop_table_3_1_0} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . 17ce0.. x0 x1 x2 x3 x4 x5 x6 x7 x8 1 0 = x3 (proof)
Theorem 5d42d..^{binop_table_3_1_1} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . 17ce0.. x0 x1 x2 x3 x4 x5 x6 x7 x8 1 1 = x4 (proof)
Theorem d9aa8..^{binop_table_3_1_2} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . 17ce0.. x0 x1 x2 x3 x4 x5 x6 x7 x8 1 2 = x5 (proof)
Theorem 491c6..^{binop_table_3_2_0} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . 17ce0.. x0 x1 x2 x3 x4 x5 x6 x7 x8 2 0 = x6 (proof)
Theorem 83a99..^{binop_table_3_2_1} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . 17ce0.. x0 x1 x2 x3 x4 x5 x6 x7 x8 2 1 = x7 (proof)
Theorem a6cff..^{binop_table_3_2_2} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . 17ce0.. x0 x1 x2 x3 x4 x5 x6 x7 x8 2 2 = x8 (proof)
Known 416bd..^cases_3 : ∀ x0 . In x0 3 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 x0
Theorem 479d5..^{binop_table_on_3} : ∀ x0 . In x0 3 ⟶ ∀ x1 . In x1 3 ⟶ ∀ x2 . In x2 3 ⟶ ∀ x3 . In x3 3 ⟶ ∀ x4 . In x4 3 ⟶ ∀ x5 . In x5 3 ⟶ ∀ x6 . In x6 3 ⟶ ∀ x7 . In x7 3 ⟶ ∀ x8 . In x8 3 ⟶ binop_on 3 (17ce0.. x0 x1 x2 x3 x4 x5 x6 x7 x8) (proof)
Definition 44bc7..^{binop_table_4} := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . ap (ap (lam 4 (λ x17 . If_i (x17 = 0) (lam 4 (λ x18 . If_i (x18 = 0) x0 (If_i (x18 = 1) x1 (If_i (x18 = 2) x2 x3)))) (If_i (x17 = 1) (lam 4 (λ x18 . If_i (x18 = 0) x4 (If_i (x18 = 1) x5 (If_i (x18 = 2) x6 x7)))) (If_i (x17 = 2) (lam 4 (λ x18 . If_i (x18 = 0) x8 (If_i (x18 = 1) x9 (If_i (x18 = 2) x10 x11)))) (lam 4 (λ x18 . If_i (x18 = 0) x12 (If_i (x18 = 1) x13 (If_i (x18 = 2) x14 x15)))))))) x16)
Known c2555..^tuple_4_0_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 0 = x0
Theorem 990fb..^{binop_table_4_0_0} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . 44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 0 0 = x0 (proof)
Known 751a0..^tuple_4_1_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 1 = x1
Theorem f3bca..^{binop_table_4_0_1} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . 44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 0 1 = x1 (proof)
Known 0a38e..^tuple_4_2_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 2 = x2
Theorem 9a100..^{binop_table_4_0_2} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . 44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 0 2 = x2 (proof)
Known 9ff59..^tuple_4_3_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 3 = x3
Theorem 668de..^{binop_table_4_0_3} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . 44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 0 3 = x3 (proof)
Theorem f3f9b..^{binop_table_4_1_0} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . 44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 1 0 = x4 (proof)
Theorem b5c6f..^{binop_table_4_1_1} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . 44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 1 1 = x5 (proof)
Theorem 5c220..^{binop_table_4_1_2} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . 44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 1 2 = x6 (proof)
Theorem 64639..^{binop_table_4_1_3} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . 44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 1 3 = x7 (proof)
Theorem a84db..^{binop_table_4_2_0} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . 44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 2 0 = x8 (proof)
Theorem 8b2c6..^{binop_table_4_2_1} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . 44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 2 1 = x9 (proof)
Theorem 8362a..^{binop_table_4_2_2} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . 44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 2 2 = x10 (proof)
Theorem 8f335..^{binop_table_4_2_3} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . 44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 2 3 = x11 (proof)
Theorem ed781..^{binop_table_4_3_0} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . 44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 3 0 = x12 (proof)
Theorem fd50e..^{binop_table_4_3_1} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . 44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 3 1 = x13 (proof)
Theorem 19e8a..^{binop_table_4_3_2} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . 44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 3 2 = x14 (proof)
Theorem 0e1bd..^{binop_table_4_3_3} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . 44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 3 3 = x15 (proof)
Known 8b3d1..^cases_4 : ∀ x0 . In x0 4 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 x0
Theorem d1a06..^{binop_table_on_4} : ∀ x0 . In x0 4 ⟶ ∀ x1 . In x1 4 ⟶ ∀ x2 . In x2 4 ⟶ ∀ x3 . In x3 4 ⟶ ∀ x4 . In x4 4 ⟶ ∀ x5 . In x5 4 ⟶ ∀ x6 . In x6 4 ⟶ ∀ x7 . In x7 4 ⟶ ∀ x8 . In x8 4 ⟶ ∀ x9 . In x9 4 ⟶ ∀ x10 . In x10 4 ⟶ ∀ x11 . In x11 4 ⟶ ∀ x12 . In x12 4 ⟶ ∀ x13 . In x13 4 ⟶ ∀ x14 . In x14 4 ⟶ ∀ x15 . In x15 4 ⟶ binop_on 4 (44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) (proof)
Definition a80b3..^{binop_table_5} := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 . ap (ap (lam 5 (λ x26 . If_i (x26 = 0) (lam 5 (λ x27 . If_i (x27 = 0) x0 (If_i (x27 = 1) x1 (If_i (x27 = 2) x2 (If_i (x27 = 3) x3 x4))))) (If_i (x26 = 1) (lam 5 (λ x27 . If_i (x27 = 0) x5 (If_i (x27 = 1) x6 (If_i (x27 = 2) x7 (If_i (x27 = 3) x8 x9))))) (If_i (x26 = 2) (lam 5 (λ x27 . If_i (x27 = 0) x10 (If_i (x27 = 1) x11 (If_i (x27 = 2) x12 (If_i (x27 = 3) x13 x14))))) (If_i (x26 = 3) (lam 5 (λ x27 . If_i (x27 = 0) x15 (If_i (x27 = 1) x16 (If_i (x27 = 2) x17 (If_i (x27 = 3) x18 x19))))) (lam 5 (λ x27 . If_i (x27 = 0) x20 (If_i (x27 = 1) x21 (If_i (x27 = 2) x22 (If_i (x27 = 3) x23 x24)))))))))) x25)
Known e53d3..^tuple_5_0_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 0 = x0
Theorem b1f8d..^{binop_table_5_0_0} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 0 0 = x0 (proof)
Known ad54e..^tuple_5_1_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 1 = x1
Theorem 8e3a9..^{binop_table_5_0_1} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 0 1 = x1 (proof)
Known 3b439..^tuple_5_2_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 2 = x2
Theorem 700a7..^{binop_table_5_0_2} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 0 2 = x2 (proof)
Known 0bd54..^tuple_5_3_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 3 = x3
Theorem 6cf44..^{binop_table_5_0_3} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 0 3 = x3 (proof)
Known 75457..^tuple_5_4_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 4 = x4
Theorem 6e1cc..^{binop_table_5_0_4} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 0 4 = x4 (proof)
Theorem 064c0..^{binop_table_5_1_0} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 1 0 = x5 (proof)
Theorem 0dd90..^{binop_table_5_1_1} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 1 1 = x6 (proof)
Theorem 4218e..^{binop_table_5_1_2} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 1 2 = x7 (proof)
Theorem aede3..^{binop_table_5_1_3} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 1 3 = x8 (proof)
Theorem 2bc50..^{binop_table_5_1_4} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 1 4 = x9 (proof)
Theorem 77ec0..^{binop_table_5_2_0} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 2 0 = x10 (proof)
Theorem 0dede..^{binop_table_5_2_1} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 2 1 = x11 (proof)
Theorem 3d7a2..^{binop_table_5_2_2} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 2 2 = x12 (proof)
Theorem 756e7..^{binop_table_5_2_3} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 2 3 = x13 (proof)
Theorem bbcd6..^{binop_table_5_2_4} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 2 4 = x14 (proof)
Theorem e3920..^{binop_table_5_3_0} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 3 0 = x15 (proof)
Theorem d5015..^{binop_table_5_3_1} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 3 1 = x16 (proof)
Theorem ffb1d..^{binop_table_5_3_2} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 3 2 = x17 (proof)
Theorem afcdb..^{binop_table_5_3_3} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 3 3 = x18 (proof)
Theorem d4f6d..^{binop_table_5_3_4} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 3 4 = x19 (proof)
Theorem e1a9d..^{binop_table_5_4_0} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 4 0 = x20 (proof)
Theorem 6f293..^{binop_table_5_4_1} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 4 1 = x21 (proof)
Theorem 9a4ee..^{binop_table_5_4_2} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 4 2 = x22 (proof)
Theorem 963f4..^{binop_table_5_4_3} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 4 3 = x23 (proof)
Theorem 0414a..^{binop_table_5_4_4} : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 4 4 = x24 (proof)
Known 2d26c..^cases_5 : ∀ x0 . In x0 5 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 4 ⟶ x1 x0
Theorem 25bf5..^{binop_table_on_5} : ∀ x0 . In x0 5 ⟶ ∀ x1 . In x1 5 ⟶ ∀ x2 . In x2 5 ⟶ ∀ x3 . In x3 5 ⟶ ∀ x4 . In x4 5 ⟶ ∀ x5 . In x5 5 ⟶ ∀ x6 . In x6 5 ⟶ ∀ x7 . In x7 5 ⟶ ∀ x8 . In x8 5 ⟶ ∀ x9 . In x9 5 ⟶ ∀ x10 . In x10 5 ⟶ ∀ x11 . In x11 5 ⟶ ∀ x12 . In x12 5 ⟶ ∀ x13 . In x13 5 ⟶ ∀ x14 . In x14 5 ⟶ ∀ x15 . In x15 5 ⟶ ∀ x16 . In x16 5 ⟶ ∀ x17 . In x17 5 ⟶ ∀ x18 . In x18 5 ⟶ ∀ x19 . In x19 5 ⟶ ∀ x20 . In x20 5 ⟶ ∀ x21 . In x21 5 ⟶ ∀ x22 . In x22 5 ⟶ ∀ x23 . In x23 5 ⟶ ∀ x24 . In x24 5 ⟶ binop_on 5 (a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24) (proof)