:: EXCHSORT semantic presentation begin theorem :: EXCHSORT:1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "a")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "b")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "a")))) "iff" (Bool "ex" (Set (Var "c")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "c")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) ")" )) ")" ))) ; theorem :: EXCHSORT:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "d"))) & (Bool "not" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "d"))) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "c"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ))) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "d"))) ")" )) ; theorem :: EXCHSORT:3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"nin"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "(" (Set (Var "y")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: EXCHSORT:4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "x")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: EXCHSORT:5 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "r")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set (Var "r")))) "iff" (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "r"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) ")" )))) ; theorem :: EXCHSORT:6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "a")) ($#k6_subset_1 :::"\"::: ) (Set (Var "b"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k2_ordinal2 :::"inf"::: ) (Set "(" (Set (Var "a")) ($#k6_subset_1 :::"\"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k3_ordinal2 :::"sup"::: ) (Set "(" (Set (Var "a")) ($#k6_subset_1 :::"\"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" (Set (Var "a")) ($#k6_subset_1 :::"\"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "a")))) ")" )) ; theorem :: EXCHSORT:7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Bool "not" (Set (Set (Var "a")) ($#k6_subset_1 :::"\"::: ) (Set (Var "b"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Set (Var "a")) ($#k6_subset_1 :::"\"::: ) (Set (Var "b"))) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "n")))))) ; begin definitionlet "f" be ($#m1_hidden :::"set"::: ) ; attr "f" is :::"segmental"::: means :: EXCHSORT:def 1 (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) "f") ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_subset_1 :::"\"::: ) (Set (Var "b"))))); end; :: deftheorem defines :::"segmental"::: EXCHSORT:def 1 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_exchsort :::"segmental"::: ) ) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_subset_1 :::"\"::: ) (Set (Var "b"))))) ")" )); theorem :: EXCHSORT:8 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "f")) "is" ($#v1_exchsort :::"segmental"::: ) )) "holds" (Bool (Set (Var "g")) "is" ($#v1_exchsort :::"segmental"::: ) )) ; theorem :: EXCHSORT:9 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_exchsort :::"segmental"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "c"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))))) ; registration cluster ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) -> ($#v1_exchsort :::"segmental"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) -> ($#v1_exchsort :::"segmental"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "a" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; let "s" be ($#m1_hidden :::"set"::: ) ; attr "s" is "a" :::"-based"::: means :: EXCHSORT:def 2 (Bool "for" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) "s"))) "holds" (Bool "(" (Bool "a" ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) "s")) & (Bool "a" ($#r1_ordinal1 :::"c="::: ) (Set (Var "b"))) ")" )); attr "s" is "a" :::"-limited"::: means :: EXCHSORT:def 3 (Bool "a" ($#r1_hidden :::"="::: ) (Set ($#k3_ordinal2 :::"sup"::: ) (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) "s" ")" ))); end; :: deftheorem defines :::"-based"::: EXCHSORT:def 2 : (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "s")) "is" (Set (Var "a")) ($#v2_exchsort :::"-based"::: ) ) "iff" (Bool "for" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "s"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "s")))) & (Bool (Set (Var "a")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "b"))) ")" )) ")" ))); :: deftheorem defines :::"-limited"::: EXCHSORT:def 3 : (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "s")) "is" (Set (Var "a")) ($#v3_exchsort :::"-limited"::: ) ) "iff" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k3_ordinal2 :::"sup"::: ) (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "s")) ")" ))) ")" ))); theorem :: EXCHSORT:10 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "f")) "is" (Set (Var "a")) ($#v2_exchsort :::"-based"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_exchsort :::"segmental"::: ) ) ")" ) "iff" (Bool "ex" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_subset_1 :::"\"::: ) (Set (Var "a")))) & (Bool (Set (Var "a")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "b"))) ")" )) ")" ))) ; theorem :: EXCHSORT:11 (Bool "for" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "f")) "is" (Set (Var "b")) ($#v3_exchsort :::"-limited"::: ) ) & (Bool (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "f")) "is" ($#v1_exchsort :::"segmental"::: ) ) ")" ) "iff" (Bool "ex" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_subset_1 :::"\"::: ) (Set (Var "a")))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) ")" )) ")" ))) ; registration cluster ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) -> (Set ($#k1_xboole_0 :::"0"::: ) ) ($#v2_exchsort :::"-based"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) -> (Num 1) ($#v2_exchsort :::"-based"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: EXCHSORT:12 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Var "f")) "is" (Set ($#k2_ordinal2 :::"inf"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" )) ($#v2_exchsort :::"-based"::: ) )) ; theorem :: EXCHSORT:13 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Var "f")) "is" (Set ($#k3_ordinal2 :::"sup"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" )) ($#v3_exchsort :::"-limited"::: ) )) ; theorem :: EXCHSORT:14 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "is" (Set (Var "b")) ($#v3_exchsort :::"-limited"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))))) ; definitionlet "f" be ($#m1_hidden :::"Function":::); func :::"base-"::: "f" -> ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) means :: EXCHSORT:def 4 (Bool "f" "is" it ($#v2_exchsort :::"-based"::: ) ) if (Bool "ex" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )); func :::"limit-"::: "f" -> ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) means :: EXCHSORT:def 5 (Bool "f" "is" it ($#v3_exchsort :::"-limited"::: ) ) if (Bool "ex" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )); end; :: deftheorem defines :::"base-"::: EXCHSORT:def 4 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "(" (Bool (Bool "ex" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_exchsort :::"base-"::: ) (Set (Var "f")))) "iff" (Bool (Set (Var "f")) "is" (Set (Var "b2")) ($#v2_exchsort :::"-based"::: ) ) ")" ) ")" & "(" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) ")" )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_exchsort :::"base-"::: ) (Set (Var "f")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" ) ")" ")" ))); :: deftheorem defines :::"limit-"::: EXCHSORT:def 5 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "(" (Bool (Bool "ex" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_exchsort :::"limit-"::: ) (Set (Var "f")))) "iff" (Bool (Set (Var "f")) "is" (Set (Var "b2")) ($#v3_exchsort :::"-limited"::: ) ) ")" ) ")" & "(" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) ")" )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_exchsort :::"limit-"::: ) (Set (Var "f")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" ) ")" ")" ))); definitionlet "f" be ($#m1_hidden :::"Function":::); func :::"len-"::: "f" -> ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) equals :: EXCHSORT:def 6 (Set (Set "(" ($#k2_exchsort :::"limit-"::: ) "f" ")" ) ($#k5_ordinal3 :::"-^"::: ) (Set "(" ($#k1_exchsort :::"base-"::: ) "f" ")" )); end; :: deftheorem defines :::"len-"::: EXCHSORT:def 6 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k3_exchsort :::"len-"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_exchsort :::"limit-"::: ) (Set (Var "f")) ")" ) ($#k5_ordinal3 :::"-^"::: ) (Set "(" ($#k1_exchsort :::"base-"::: ) (Set (Var "f")) ")" )))); theorem :: EXCHSORT:15 (Bool "(" (Bool (Set ($#k1_exchsort :::"base-"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool (Set ($#k2_exchsort :::"limit-"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool (Set ($#k3_exchsort :::"len-"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" ) ; theorem :: EXCHSORT:16 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k2_exchsort :::"limit-"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_ordinal2 :::"sup"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" )))) ; theorem :: EXCHSORT:17 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Var "f")) "is" (Set ($#k2_exchsort :::"limit-"::: ) (Set (Var "f"))) ($#v3_exchsort :::"-limited"::: ) )) ; theorem :: EXCHSORT:18 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "A")) "is" (Set (Var "a")) ($#v2_exchsort :::"-based"::: ) ))) ; registrationlet "a" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; let "X", "Y" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_relat_1 :::"Relation-like"::: ) "Y" ($#v4_relat_1 :::"-defined"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_exchsort :::"segmental"::: ) "a" ($#v2_exchsort :::"-based"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#v2_exchsort :::"-based"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode array is ($#v1_exchsort :::"segmental"::: ) ($#m1_hidden :::"Function":::); end; registrationlet "A" be ($#m1_hidden :::"array":::); cluster (Set ($#k9_xtuple_0 :::"proj1"::: ) "A") -> ($#v1_ordinal6 :::"ordinal-membered"::: ) ; end; theorem :: EXCHSORT:19 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"array":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" (Set ($#k1_xboole_0 :::"0"::: ) ) ($#v3_exchsort :::"-limited"::: ) ) "iff" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) ; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_exchsort :::"segmental"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#v2_exchsort :::"-based"::: ) -> ($#v5_ordinal1 :::"T-Sequence-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode array of "X" is "X" ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"array":::); end; definitionlet "X" be ($#l1_struct_0 :::"1-sorted"::: ) ; mode array of "X" is ($#m1_hidden :::"array":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X"); end; definitionlet "a" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; let "X" be ($#m1_hidden :::"set"::: ) ; mode array of "a" "," "X" is "a" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"array":::) "of" "X"; end; theorem :: EXCHSORT:20 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k1_exchsort :::"base-"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_ordinal2 :::"inf"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" )))) ; theorem :: EXCHSORT:21 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Var "f")) "is" (Set ($#k1_exchsort :::"base-"::: ) (Set (Var "f"))) ($#v2_exchsort :::"-based"::: ) )) ; theorem :: EXCHSORT:22 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"array":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_exchsort :::"limit-"::: ) (Set (Var "A")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k1_exchsort :::"base-"::: ) (Set (Var "A")) ")" )))) ; theorem :: EXCHSORT:23 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"array":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_subset_1 :::"\"::: ) (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "A")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k1_exchsort :::"base-"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k2_exchsort :::"limit-"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ; theorem :: EXCHSORT:24 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"T-Sequence":::) "holds" (Bool "(" (Bool (Set ($#k1_exchsort :::"base-"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool (Set ($#k2_exchsort :::"limit-"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_exchsort :::"len-"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) ")" )) ; registrationlet "a", "b" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; let "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "a" ($#v4_relat_1 :::"-defined"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v4_valued_0 :::"natural-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_exchsort :::"segmental"::: ) "b" ($#v2_exchsort :::"-based"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "a" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "a" "," "x" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) -> ($#v1_exchsort :::"segmental"::: ) ; end; registrationlet "a" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; let "x" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "a" "," "x" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) -> ($#v4_valued_0 :::"natural-valued"::: ) for ($#m1_hidden :::"array":::); end; registrationlet "a" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; let "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "a" "," "x" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) -> ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_hidden :::"array":::); end; registrationlet "a" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); cluster (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "a" "," "x" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) -> "X" ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"array":::); end; registrationlet "a" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "a" "," "x" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) -> "a" ($#v2_exchsort :::"-based"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "a") ($#v3_exchsort :::"-limited"::: ) for ($#m1_hidden :::"array":::); end; registrationlet "b" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v4_valued_0 :::"natural-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_exchsort :::"segmental"::: ) "b" ($#v2_exchsort :::"-based"::: ) for ($#m1_hidden :::"set"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_exchsort :::"segmental"::: ) "b" ($#v2_exchsort :::"-based"::: ) for ($#m1_hidden :::"set"::: ) ; end; notationlet "s" be ($#m1_hidden :::"T-Sequence":::); synonym "s" :::"last"::: for :::"last"::: "s"; end; definitionlet "A" be ($#m1_hidden :::"array":::); func :::"last"::: "A" -> ($#m1_hidden :::"set"::: ) equals :: EXCHSORT:def 7 (Set "A" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "A" ")" ) ")" )); end; :: deftheorem defines :::"last"::: EXCHSORT:def 7 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"array":::) "holds" (Bool (Set ($#k4_exchsort :::"last"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A")) ")" ) ")" )))); registrationlet "A" be ($#m1_hidden :::"T-Sequence":::); identify ; end; begin definitionlet "f" be ($#m1_hidden :::"Function":::); attr "f" is :::"descending"::: means :: EXCHSORT:def 8 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r2_xboole_0 :::"c<"::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))); end; :: deftheorem defines :::"descending"::: EXCHSORT:def 8 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_exchsort :::"descending"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r2_xboole_0 :::"c<"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) ")" )); theorem :: EXCHSORT:25 (Bool "for" (Set (Var "f")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"array":::) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a")) ")" )) ($#r2_xboole_0 :::"c<"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v4_exchsort :::"descending"::: ) )) ; theorem :: EXCHSORT:26 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"array":::) "st" (Bool (Bool (Set ($#k3_exchsort :::"len-"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) & (Bool "(" "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a")) ")" )) ($#r2_xboole_0 :::"c<"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v4_exchsort :::"descending"::: ) )) ; theorem :: EXCHSORT:27 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_exchsort :::"descending"::: ) ) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v1_finset_1 :::"finite"::: ) )) ; theorem :: EXCHSORT:28 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_exchsort :::"descending"::: ) ) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool "(" "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) ")" )) "holds" (Bool (Set ($#k4_exchsort :::"last"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; scheme :: EXCHSORT:sch 1 A{ F1() -> ($#m1_hidden :::"T-Sequence":::), F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool (Set F1 "(" ")" ) "is" ($#v1_finset_1 :::"finite"::: ) ) provided (Bool (Set F2 "(" (Set "(" (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ")" ) ")" ) "is" ($#v1_finset_1 :::"finite"::: ) ) and (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set F1 "(" ")" ))) & (Bool (Set F2 "(" (Set "(" (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ")" ) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set F2 "(" (Set "(" (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#r2_xboole_0 :::"c<"::: ) (Set F2 "(" (Set "(" (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ")" ))) proof end; begin registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); let "a", "b" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k10_funct_7 :::"Swap"::: ) "(" "f" "," "a" "," "b" ")" ) -> "X" ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "X")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k10_funct_7 :::"Swap"::: ) "(" "f" "," "x" "," "y" ")" ) -> "X" ($#v5_relat_1 :::"-valued"::: ) ; end; theorem :: EXCHSORT:29 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))))) ; theorem :: EXCHSORT:30 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "y")))))) ; theorem :: EXCHSORT:31 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; theorem :: EXCHSORT:32 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")))))) ; theorem :: EXCHSORT:33 (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z")))))) ; theorem :: EXCHSORT:34 (Bool "for" (Set (Var "X")) "," (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "z")))))) ; theorem :: EXCHSORT:35 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "y")) "," (Set (Var "x")) ")" )))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_funct_2 :::"onto"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Const "X")) ($#v5_relat_1 :::"-valued"::: ) ($#v2_funct_2 :::"onto"::: ) ($#m1_hidden :::"Function":::); let "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Const "f"))); cluster (Set ($#k10_funct_7 :::"Swap"::: ) "(" "f" "," "x" "," "y" ")" ) -> ($#v2_funct_2 :::"onto"::: ) ; end; registrationlet "A" be ($#m1_hidden :::"array":::); let "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k10_funct_7 :::"Swap"::: ) "(" "A" "," "x" "," "y" ")" ) -> ($#v1_exchsort :::"segmental"::: ) ; end; theorem :: EXCHSORT:36 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"array":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#k10_funct_7 :::"Swap"::: ) "(" (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; registrationlet "A" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"array":::); let "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k10_funct_7 :::"Swap"::: ) "(" "A" "," "x" "," "y" ")" ) -> ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_hidden :::"array":::); end; begin definitionlet "A" be ($#m1_hidden :::"array":::); mode :::"permutation"::: "of" "A" -> ($#m1_hidden :::"array":::) means :: EXCHSORT:def 9 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "A" ")" ) "st" (Bool it ($#r1_hidden :::"="::: ) (Set "A" ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))); end; :: deftheorem defines :::"permutation"::: EXCHSORT:def 9 : (Bool "for" (Set (Var "A")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"array":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_exchsort :::"permutation"::: ) "of" (Set (Var "A"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A")) ")" ) "st" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) ")" )); theorem :: EXCHSORT:37 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"array":::) (Bool "for" (Set (Var "B")) "being" ($#m1_exchsort :::"permutation"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "A")))) ")" ))) ; theorem :: EXCHSORT:38 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"array":::) "holds" (Bool (Set (Var "A")) "is" ($#m1_exchsort :::"permutation"::: ) "of" (Set (Var "A")))) ; theorem :: EXCHSORT:39 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"array":::) "st" (Bool (Bool (Set (Var "A")) "is" ($#m1_exchsort :::"permutation"::: ) "of" (Set (Var "B")))) "holds" (Bool (Set (Var "B")) "is" ($#m1_exchsort :::"permutation"::: ) "of" (Set (Var "A")))) ; theorem :: EXCHSORT:40 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"array":::) "st" (Bool (Bool (Set (Var "A")) "is" ($#m1_exchsort :::"permutation"::: ) "of" (Set (Var "B"))) & (Bool (Set (Var "B")) "is" ($#m1_exchsort :::"permutation"::: ) "of" (Set (Var "C")))) "holds" (Bool (Set (Var "A")) "is" ($#m1_exchsort :::"permutation"::: ) "of" (Set (Var "C")))) ; theorem :: EXCHSORT:41 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_funct_7 :::"Swap"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); cluster (Set ($#k10_funct_7 :::"Swap"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) "X" ")" ) "," "x" "," "y" ")" ) -> "X" ($#v4_relat_1 :::"-defined"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ($#v2_funct_1 :::"one-to-one"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); cluster (Set ($#k10_funct_7 :::"Swap"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) "X" ")" ) "," "x" "," "y" ")" ) -> ($#v1_partfun1 :::"total"::: ) ($#v2_funct_2 :::"onto"::: ) ; end; definitionlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); :: original: :::"Swap"::: redefine func :::"Swap"::: "(" "f" "," "x" "," "y" ")" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," "Y"; end; theorem :: EXCHSORT:42 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"array":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k10_funct_7 :::"Swap"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) "," (Set (Var "y")) ")" )) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))))) ; theorem :: EXCHSORT:43 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"array":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) "is" ($#m1_exchsort :::"permutation"::: ) "of" (Set (Var "A"))) & (Bool (Set (Var "A")) "is" ($#m1_exchsort :::"permutation"::: ) "of" (Set ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ))) ; theorem :: EXCHSORT:44 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"array":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set (Var "A")) "is" ($#m1_exchsort :::"permutation"::: ) "of" (Set (Var "B")))) "holds" (Bool "(" (Bool (Set ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) "is" ($#m1_exchsort :::"permutation"::: ) "of" (Set (Var "B"))) & (Bool (Set (Var "A")) "is" ($#m1_exchsort :::"permutation"::: ) "of" (Set ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "B")) "," (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ))) ; begin definitionlet "O" be ($#l1_orders_2 :::"RelStr"::: ) ; let "A" be ($#m1_hidden :::"array":::) "of" (Set (Const "O")); attr "A" is :::"ascending"::: means :: EXCHSORT:def 10 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "A")) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "A")) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set "A" ($#k7_partfun1 :::"/."::: ) (Set (Var "a"))) ($#r1_orders_2 :::"<="::: ) (Set "A" ($#k7_partfun1 :::"/."::: ) (Set (Var "b"))))); func :::"inversions"::: "A" -> ($#m1_hidden :::"set"::: ) equals :: EXCHSORT:def 11 "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) where a, b "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) "A") : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Bool "not" (Set "A" ($#k7_partfun1 :::"/."::: ) (Set (Var "a"))) ($#r1_orders_2 :::"<="::: ) (Set "A" ($#k7_partfun1 :::"/."::: ) (Set (Var "b"))))) ")" ) "}" ; end; :: deftheorem defines :::"ascending"::: EXCHSORT:def 10 : (Bool "for" (Set (Var "O")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v5_exchsort :::"ascending"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "A")) ($#k7_partfun1 :::"/."::: ) (Set (Var "a"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "A")) ($#k7_partfun1 :::"/."::: ) (Set (Var "b"))))) ")" ))); :: deftheorem defines :::"inversions"::: EXCHSORT:def 11 : (Bool "for" (Set (Var "O")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "holds" (Bool (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) where a, b "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A"))) : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Bool "not" (Set (Set (Var "A")) ($#k7_partfun1 :::"/."::: ) (Set (Var "a"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "A")) ($#k7_partfun1 :::"/."::: ) (Set (Var "b"))))) ")" ) "}" ))); registrationlet "O" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "O") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_exchsort :::"segmental"::: ) -> ($#v1_xboole_0 :::"empty"::: ) ($#v5_exchsort :::"ascending"::: ) for ($#m1_hidden :::"set"::: ) ; let "A" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"array":::) "of" (Set (Const "O")); cluster (Set ($#k6_exchsort :::"inversions"::: ) "A") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: EXCHSORT:45 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "O")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_orders_2 :::">"::: ) (Set (Var "y"))) "iff" (Bool (Bool "not" (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y")))) ")" ))) ; definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); let "R" be ($#m1_hidden :::"array":::) "of" (Set (Const "O")); redefine func :::"inversions"::: "R" equals :: EXCHSORT:def 12 "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) where a, b "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) "R") : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set "R" ($#k7_partfun1 :::"/."::: ) (Set (Var "a"))) ($#r2_orders_2 :::">"::: ) (Set "R" ($#k7_partfun1 :::"/."::: ) (Set (Var "b")))) ")" ) "}" ; end; :: deftheorem defines :::"inversions"::: EXCHSORT:def 12 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "holds" (Bool (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) where a, b "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Set (Var "R")) ($#k7_partfun1 :::"/."::: ) (Set (Var "a"))) ($#r2_orders_2 :::">"::: ) (Set (Set (Var "R")) ($#k7_partfun1 :::"/."::: ) (Set (Var "b")))) ")" ) "}" ))); theorem :: EXCHSORT:46 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "y"))) & (Bool (Set (Set (Var "R")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r2_orders_2 :::">"::: ) (Set (Set (Var "R")) ($#k7_partfun1 :::"/."::: ) (Set (Var "y")))) ")" ) ")" )))) ; theorem :: EXCHSORT:47 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "holds" (Bool (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) "," (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )))) ; registrationlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); let "R" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"array":::) "of" (Set (Const "O")); cluster (Set ($#k6_exchsort :::"inversions"::: ) "R") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: EXCHSORT:48 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v5_exchsort :::"ascending"::: ) ) "iff" (Bool (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: EXCHSORT:49 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"nin"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))))))) ; theorem :: EXCHSORT:50 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))))))) ; registrationlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); let "R" be ($#m1_hidden :::"array":::) "of" (Set (Const "O")); cluster (Set ($#k6_exchsort :::"inversions"::: ) "R") -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; registrationlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); let "R" be ($#m1_hidden :::"array":::) "of" (Set (Const "O")); cluster (Set ($#k6_exchsort :::"inversions"::: ) "R") -> ($#v5_relat_2 :::"asymmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) for ($#m1_hidden :::"Relation":::); end; definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "O")); :: original: :::"<"::: redefine pred "a" :::"<"::: "b"; asymmetry (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "O")) "st" (Bool (Bool bbbadR2_ORDERS_2((Set (Const "O")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds" (Bool "not" (Bool bbbadR2_ORDERS_2((Set (Const "O")) "," (Set (Var "b2")) "," (Set (Var "b1")))))) ; end; theorem :: EXCHSORT:51 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"nin"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" )))))) ; theorem :: EXCHSORT:52 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) & (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R")))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))) ")" )))) ; theorem :: EXCHSORT:53 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))))) "holds" (Bool "(" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R")))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) ")" ) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))) ")" )))) ; theorem :: EXCHSORT:54 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R")))) "iff" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))) ")" ) ")" )))) ; theorem :: EXCHSORT:55 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R")))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "y"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" )))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))))))) ; theorem :: EXCHSORT:56 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "z"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" )))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))))))) ; theorem :: EXCHSORT:57 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "z"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" )))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))))))) ; theorem :: EXCHSORT:58 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "z"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R")))) ")" ) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))) ")" )))) ; definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); let "R" be ($#m1_hidden :::"array":::) "of" (Set (Const "O")); let "x", "y" be ($#m1_hidden :::"set"::: ) ; func "(" "R" "," "x" "," "y" ")" :::"incl"::: -> ($#m1_hidden :::"Function":::) equals :: EXCHSORT:def 13 (Set (Set ($#k15_funct_3 :::"[:"::: ) (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "R" ")" ) ")" ) "," "x" "," "y" ")" ")" ) "," (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "R" ")" ) ")" ) "," "x" "," "y" ")" ")" ) ($#k15_funct_3 :::":]"::: ) ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Set "(" ($#k1_ordinal1 :::"succ"::: ) "y" ")" ) ($#k6_subset_1 :::"\"::: ) "x" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set "(" ($#k1_ordinal1 :::"succ"::: ) "y" ")" ) ($#k6_subset_1 :::"\"::: ) "x" ")" ) "," (Set ($#k1_tarski :::"{"::: ) "y" ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ")" )); end; :: deftheorem defines :::"incl"::: EXCHSORT:def 13 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "(" (Set (Var "R")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ($#k7_exchsort :::"incl"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k15_funct_3 :::"[:"::: ) (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "," (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")) ")" ) ")" ) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k15_funct_3 :::":]"::: ) ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "y")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "x")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "y")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "x")) ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ")" )))))); theorem :: EXCHSORT:59 (Bool "for" (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "b")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "a")))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "c"))) & (Bool (Set (Var "c")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "b"))) ")" ) ")" )) ; theorem :: EXCHSORT:60 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "T")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "holds" (Bool (Set (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "q")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))))))) ; theorem :: EXCHSORT:61 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "T")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T")) ")" ) "," (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T")) ")" ) "," (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )))) ; theorem :: EXCHSORT:62 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "T")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "st" (Bool (Bool (Set (Var "p")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "q")))) "holds" (Bool "(" (Bool (Set (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "r")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "r")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) )) ")" )))) ; theorem :: EXCHSORT:63 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "T")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set (Var "p"))) & (Bool (Set (Var "s")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k5_exchsort :::"Swap"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T")) ")" ) ")" ) "," (Set (Var "p")) "," (Set (Var "q")) ")" ))) "holds" (Bool (Set (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")) ")" ) ($#k4_tarski :::"]"::: ) )))))) ; theorem :: EXCHSORT:64 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "T")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "p"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k5_exchsort :::"Swap"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T")) ")" ) ")" ) "," (Set (Var "p")) "," (Set (Var "q")) ")" ))) "holds" (Bool "(" (Bool (Set (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "q")) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k4_tarski :::"]"::: ) )) ")" ))))) ; theorem :: EXCHSORT:65 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "T")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "r"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k5_exchsort :::"Swap"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T")) ")" ) ")" ) "," (Set (Var "p")) "," (Set (Var "q")) ")" ))) "holds" (Bool "(" (Bool (Set (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "p")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "r")) ")" ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "r")) ")" ) ($#k4_tarski :::"]"::: ) )) ")" ))))) ; theorem :: EXCHSORT:66 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "T")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "q")))) "holds" (Bool (Set (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) ))))) ; theorem :: EXCHSORT:67 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "T")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "q"))) & (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set (Var "p"))) & (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "s")) ($#r1_hidden :::"<>"::: ) (Set (Var "p"))) & (Bool (Set (Var "s")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool (Set (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))))) ; theorem :: EXCHSORT:68 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "T")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "q")))) "holds" (Bool "(" (Bool (Set (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "r")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "r")) "," (Set (Var "p")) ($#k4_tarski :::"]"::: ) )) ")" )))) ; theorem :: EXCHSORT:69 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "T")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "q")))) "holds" (Bool "(" (Bool (Set (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "s")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "s")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) )) ")" )))) ; theorem :: EXCHSORT:70 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "T")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "s")))) "holds" (Bool "(" (Bool (Set (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "q")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )) ")" )))) ; theorem :: EXCHSORT:71 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "T")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "q")))) "holds" (Bool (Set (Set "(" "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k6_exchsort :::"inversions"::: ) (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "T")) "," (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ")" )) "is" ($#v2_funct_1 :::"one-to-one"::: ) )))) ; registrationlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); let "R" be ($#m1_hidden :::"array":::) "of" (Set (Const "O")); let "x", "y", "z" be ($#m1_hidden :::"set"::: ) ; cluster (Set (Set "(" "(" "R" "," "x" "," "y" ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k7_relat_1 :::".:"::: ) "z") -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; begin theorem :: EXCHSORT:72 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Set "(" "(" (Set (Var "R")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ($#k7_exchsort :::"incl"::: ) ")" ) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k6_exchsort :::"inversions"::: ) (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" )) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))))))) ; registrationlet "R" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); let "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k10_funct_7 :::"Swap"::: ) "(" "R" "," "x" "," "y" ")" ) -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: EXCHSORT:73 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R")))) & (Bool (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k6_exchsort :::"inversions"::: ) (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k6_exchsort :::"inversions"::: ) (Set (Var "R")) ")" )))))) ; theorem :: EXCHSORT:74 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k6_exchsort :::"inversions"::: ) (Set "(" ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k6_exchsort :::"inversions"::: ) (Set (Var "R")) ")" )))))) ; definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); let "R" be ($#m1_hidden :::"array":::) "of" (Set (Const "O")); mode :::"arr_computation"::: "of" "R" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"array":::) means :: EXCHSORT:def 14 (Bool "(" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_exchsort :::"base-"::: ) it ")" )) ($#r1_hidden :::"="::: ) "R") & (Bool "(" "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) "is" ($#m1_hidden :::"array":::) "of" "O") ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it)) & (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool "ex" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" "O"(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R")))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "R"))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"arr_computation"::: EXCHSORT:def 14 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "b3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"array":::) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_exchsort :::"arr_computation"::: ) "of" (Set (Var "R"))) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_exchsort :::"base-"::: ) (Set (Var "b3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "R"))) & (Bool "(" "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) "is" ($#m1_hidden :::"array":::) "of" (Set (Var "O"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3")))) & (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool "ex" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O"))(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_exchsort :::"inversions"::: ) (Set (Var "R")))) & (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "R"))) & (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_funct_7 :::"Swap"::: ) "(" (Set (Var "R")) "," (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ))) ")" ) ")" ) ")" )))); theorem :: EXCHSORT:75 (Bool "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "R")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) "is" ($#m2_exchsort :::"arr_computation"::: ) "of" (Set (Var "R")))))) ; registrationlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); let "R" be ($#m1_hidden :::"array":::) "of" (Set (Const "O")); let "a" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_exchsort :::"segmental"::: ) "a" ($#v2_exchsort :::"-based"::: ) for ($#m2_exchsort :::"arr_computation"::: ) "of" "R"; end; registrationlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); let "R" be ($#m1_hidden :::"array":::) "of" (Set (Const "O")); let "C" be ($#m2_exchsort :::"arr_computation"::: ) "of" (Set (Const "R")); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "C" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_exchsort :::"segmental"::: ) ; end; registrationlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); let "R" be ($#m1_hidden :::"array":::) "of" (Set (Const "O")); let "C" be ($#m2_exchsort :::"arr_computation"::: ) "of" (Set (Const "R")); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "C" ($#k1_funct_1 :::"."::: ) "x") -> (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "O") ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); let "R" be ($#m1_hidden :::"array":::) "of" (Set (Const "O")); let "C" be ($#m2_exchsort :::"arr_computation"::: ) "of" (Set (Const "R")); cluster (Set ($#k4_exchsort :::"last"::: ) "C") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_exchsort :::"segmental"::: ) ; end; registrationlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); let "R" be ($#m1_hidden :::"array":::) "of" (Set (Const "O")); let "C" be ($#m2_exchsort :::"arr_computation"::: ) "of" (Set (Const "R")); cluster (Set ($#k4_exchsort :::"last"::: ) "C") -> (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "O") ($#v5_relat_1 :::"-valued"::: ) ; end; definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); let "R" be ($#m1_hidden :::"array":::) "of" (Set (Const "O")); let "C" be ($#m2_exchsort :::"arr_computation"::: ) "of" (Set (Const "R")); attr "C" is :::"complete"::: means :: EXCHSORT:def 15 (Bool (Set ($#k4_exchsort :::"last"::: ) "C") "is" ($#v5_exchsort :::"ascending"::: ) ); end; :: deftheorem defines :::"complete"::: EXCHSORT:def 15 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "C")) "being" ($#m2_exchsort :::"arr_computation"::: ) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v6_exchsort :::"complete"::: ) ) "iff" (Bool (Set ($#k4_exchsort :::"last"::: ) (Set (Var "C"))) "is" ($#v5_exchsort :::"ascending"::: ) ) ")" )))); theorem :: EXCHSORT:76 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "C")) "being" (Set ($#k1_xboole_0 :::"0"::: ) ) ($#v2_exchsort :::"-based"::: ) ($#m2_exchsort :::"arr_computation"::: ) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"array":::) "of" (Set (Var "O")))) "holds" (Bool (Set (Var "C")) "is" ($#v1_finset_1 :::"finite"::: ) )))) ; theorem :: EXCHSORT:77 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "C")) "being" (Set ($#k1_xboole_0 :::"0"::: ) ) ($#v2_exchsort :::"-based"::: ) ($#m2_exchsort :::"arr_computation"::: ) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"array":::) "of" (Set (Var "O"))) & (Bool "(" "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_exchsort :::"inversions"::: ) (Set "(" (Set (Var "C")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "C")))) ")" )) "holds" (Bool (Set (Var "C")) "is" ($#v6_exchsort :::"complete"::: ) )))) ; theorem :: EXCHSORT:78 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m2_exchsort :::"arr_computation"::: ) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set ($#k4_exchsort :::"last"::: ) (Set (Var "C"))) "is" ($#m1_exchsort :::"permutation"::: ) "of" (Set (Var "R"))) & (Bool "(" "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "C"))))) "holds" (Bool (Set (Set (Var "C")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) "is" ($#m1_exchsort :::"permutation"::: ) "of" (Set (Var "R"))) ")" ) ")" )))) ; begin theorem :: EXCHSORT:79 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#v2_exchsort :::"-based"::: ) ($#m1_hidden :::"array":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k4_exchsort :::"last"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ; theorem :: EXCHSORT:80 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_exchsort :::"last"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: EXCHSORT:81 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#v2_exchsort :::"-based"::: ) ($#m1_hidden :::"array":::) "holds" (Bool (Set ($#k4_exchsort :::"last"::: ) (Set "(" (Set (Var "A")) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster -> "X" ($#v5_relat_1 :::"-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "X" ($#k8_afinsq_1 :::"^omega"::: ) ); end; scheme :: EXCHSORT:sch 2 A{ F1( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], F3() -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#v2_exchsort :::"-based"::: ) ($#m1_hidden :::"array":::)(Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k4_exchsort :::"last"::: ) (Set (Var "f")))) & (Bool (Set F1 "(" (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool "(" "for" (Set (Var "a")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "a")) ")" ))) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) ")" )) ")" ) ")" ))) provided (Bool (Set F3 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) and (Bool (Set F1 "(" (Set F3 "(" ")" ) ")" ) "is" ($#v1_finset_1 :::"finite"::: ) ) and (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set F1 "(" (Set (Var "x")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool "(" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) & (Bool (Set F1 "(" (Set (Var "y")) ")" ) ($#r2_xboole_0 :::"c<"::: ) (Set F1 "(" (Set (Var "x")) ")" )) ")" ))) proof end; theorem :: EXCHSORT:82 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"array":::) (Bool "for" (Set (Var "B")) "being" ($#m1_exchsort :::"permutation"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "A")) ")" ) ")" )))) ; registrationlet "A" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"array":::); cluster -> ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_exchsort :::"permutation"::: ) "of" "A"; end; registrationlet "a" be ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v5_ordinal1 :::"T-Sequence-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "a" "," "X" ")" ); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_membered :::"real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "X" "," "Y" ")" ); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"array":::) "of" (Set (Const "X")); cluster -> "X" ($#v5_relat_1 :::"-valued"::: ) for ($#m1_exchsort :::"permutation"::: ) "of" "A"; end; registrationlet "X", "Z" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Z")); cluster -> "Z" ($#v5_relat_1 :::"-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "X" "," "Y" ")" ); end; theorem :: EXCHSORT:83 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) (Set (Var "b2")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Var "r")) "is" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y"))))) ; theorem :: EXCHSORT:84 (Bool "for" (Set (Var "a")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) "or" (Bool "ex" (Set (Var "b")) "being" ($#v3_ordinal1 :::"ordinal"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "b"))))) ")" ))) ; theorem :: EXCHSORT:85 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#v2_exchsort :::"-based"::: ) ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "ex" (Set (Var "C")) "being" (Set ($#k1_xboole_0 :::"0"::: ) ) ($#v2_exchsort :::"-based"::: ) ($#m2_exchsort :::"arr_computation"::: ) "of" (Set (Var "A")) "st" (Bool (Set (Var "C")) "is" ($#v6_exchsort :::"complete"::: ) )))) ; theorem :: EXCHSORT:86 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#v2_exchsort :::"-based"::: ) ($#m1_hidden :::"array":::) "of" (Set (Var "O")) (Bool "ex" (Set (Var "B")) "being" ($#m1_exchsort :::"permutation"::: ) "of" (Set (Var "A")) "st" (Bool (Set (Var "B")) "is" ($#v5_exchsort :::"ascending"::: ) )))) ; registrationlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); let "A" be ($#v1_finset_1 :::"finite"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ($#v2_exchsort :::"-based"::: ) ($#m1_hidden :::"array":::) "of" (Set (Const "O")); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "O") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_exchsort :::"segmental"::: ) ($#v5_exchsort :::"ascending"::: ) for ($#m1_exchsort :::"permutation"::: ) "of" "A"; end;