:: CHAIN_1 semantic presentation begin theorem :: CHAIN_1:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "y")))) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "z"))) & (Bool (Set (Var "z")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "y"))) ")" ))) ; theorem :: CHAIN_1:2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "z"))) & (Bool (Set (Var "y")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "z"))) ")" ))) ; scheme :: CHAIN_1:sch 1 FrSet12{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) } : (Bool "{" (Set F3 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) where x, y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) "}" ($#r1_tarski :::"c="::: ) (Set F1 "(" ")" )) proof end; definitionlet "B" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "B")); :: original: :::"bool"::: redefine func :::"bool"::: "A" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "B"; end; definitionlet "d" be ($#v1_xreal_0 :::"real"::: ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); redefine attr "d" is :::"empty"::: means :: CHAIN_1:def 1 (Bool (Bool "not" "d" ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))); end; :: deftheorem defines :::"zero"::: CHAIN_1:def 1 : (Bool "for" (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"zero"::: ) ) "iff" (Bool (Bool "not" (Set (Var "d")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )); definitionlet "d" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); redefine attr "d" is :::"empty"::: means :: CHAIN_1:def 2 (Bool (Bool "not" "d" ($#r1_xxreal_0 :::">="::: ) (Num 1))); end; :: deftheorem defines :::"zero"::: CHAIN_1:def 2 : (Bool "for" (Set (Var "d")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "d")) "is" ($#v1_xboole_0 :::"zero"::: ) ) "iff" (Bool (Bool "not" (Set (Var "d")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) ")" )); theorem :: CHAIN_1:3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) ; registration cluster ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k2_xboole_0 :::"\/"::: ) "Y") -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ; cluster (Set "Y" ($#k2_xboole_0 :::"\/"::: ) "X") -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ; end; registrationlet "X" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "X"); end; theorem :: CHAIN_1:4 (Bool "for" (Set (Var "X")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ) & (Bool (Bool "not" (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))) ; scheme :: CHAIN_1:sch 2 NonEmptyFinite{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool P1[(Set F2 "(" ")" )]) provided (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) "holds" (Bool P1[(Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )])) and (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set F2 "(" ")" )) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) & (Bool P1[(Set (Var "B"))])) "holds" (Bool P1[(Set (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))]))) proof end; scheme :: CHAIN_1:sch 3 NonTrivialFinite{ F1() -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool P1[(Set F2 "(" ")" )]) provided (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool P1[(Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) )])) and (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "B")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set F2 "(" ")" )) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) & (Bool P1[(Set (Var "B"))])) "holds" (Bool P1[(Set (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))]))) proof end; theorem :: CHAIN_1:5 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Num 2)) "iff" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "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 "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "or" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) "or" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) ")" ) ")" )) ")" )) ; theorem :: CHAIN_1:6 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "m")) "is" ($#v1_abian :::"even"::: ) ) "iff" (Bool (Set (Var "n")) "is" ($#v1_abian :::"even"::: ) ) ")" ) "iff" (Bool (Set (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n"))) "is" ($#v1_abian :::"even"::: ) ) ")" )) ; theorem :: CHAIN_1:7 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y")))) "holds" (Bool "(" (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X"))) "is" ($#v1_abian :::"even"::: ) ) "iff" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Y"))) "is" ($#v1_abian :::"even"::: ) ) ")" ) "iff" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" )) "is" ($#v1_abian :::"even"::: ) ) ")" )) ; theorem :: CHAIN_1:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X"))) "is" ($#v1_abian :::"even"::: ) ) "iff" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Y"))) "is" ($#v1_abian :::"even"::: ) ) ")" ) "iff" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "X")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "Y")) ")" )) "is" ($#v1_abian :::"even"::: ) ) ")" )) ; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); redefine func :::"REAL"::: "n" means :: CHAIN_1:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "n" ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) )) ")" )); end; :: deftheorem defines :::"REAL"::: CHAIN_1:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_finseq_2 :::"FinSequenceSet"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) )) ")" )) ")" ))); begin definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); mode :::"Grating"::: "of" "d" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "d" ")" ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) means :: CHAIN_1:def 4 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) "d") "holds" (Bool "(" (Bool (Bool "not" (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" )); end; :: deftheorem defines :::"Grating"::: CHAIN_1:def 4 : (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d")) ")" ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool (Bool "not" (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )) & (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" )) ")" ))); registrationlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster -> bbbadV2_FINSET_1() for ($#m1_chain_1 :::"Grating"::: ) "of" "d"; end; definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Const "d"))); :: original: :::"."::: redefine func "G" :::"."::: "i" -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: CHAIN_1:9 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i"))))) ")" )))) ; theorem :: CHAIN_1:10 canceled; theorem :: CHAIN_1:11 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "ex" (Set (Var "ri")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "ri")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "xi")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "ri")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "xi"))) ")" ) ")" ))) ; theorem :: CHAIN_1:12 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "ex" (Set (Var "li")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "li")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "xi")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "li")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "xi"))) ")" ) ")" ))) ; theorem :: CHAIN_1:13 (Bool "for" (Set (Var "Gi")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "ex" (Set (Var "li")) "," (Set (Var "ri")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "li")) ($#r2_hidden :::"in"::: ) (Set (Var "Gi"))) & (Bool (Set (Var "ri")) ($#r2_hidden :::"in"::: ) (Set (Var "Gi"))) & (Bool (Set (Var "li")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "ri"))) & (Bool "(" "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "xi")) ($#r2_hidden :::"in"::: ) (Set (Var "Gi"))) & (Bool (Set (Var "li")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "xi")))) "holds" (Bool "not" (Bool (Set (Var "xi")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "ri")))) ")" ) ")" ))) ; theorem :: CHAIN_1:14 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "ex" (Set (Var "ri")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "ri")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "xi")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "ri")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "xi"))) ")" ) ")" ))) ; theorem :: CHAIN_1:15 (Bool "for" (Set (Var "Gi")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "ex" (Set (Var "li")) "," (Set (Var "ri")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "li")) ($#r2_hidden :::"in"::: ) (Set (Var "Gi"))) & (Bool (Set (Var "ri")) ($#r2_hidden :::"in"::: ) (Set (Var "Gi"))) & (Bool (Set (Var "ri")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "li"))) & (Bool "(" "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "xi")) ($#r2_hidden :::"in"::: ) (Set (Var "Gi")))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "xi")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "ri")))) & (Bool (Bool "not" (Set (Var "li")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "xi")))) ")" ) ")" ) ")" ))) ; definitionlet "Gi" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); mode :::"Gap"::: "of" "Gi" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) means :: CHAIN_1:def 5 (Bool "ex" (Set (Var "li")) "," (Set (Var "ri")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "li")) "," (Set (Var "ri")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "li")) ($#r2_hidden :::"in"::: ) "Gi") & (Bool (Set (Var "ri")) ($#r2_hidden :::"in"::: ) "Gi") & (Bool "(" (Bool "(" (Bool (Set (Var "li")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "ri"))) & (Bool "(" "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "xi")) ($#r2_hidden :::"in"::: ) "Gi") & (Bool (Set (Var "li")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "xi")))) "holds" (Bool "not" (Bool (Set (Var "xi")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "ri")))) ")" ) ")" ) "or" (Bool "(" (Bool (Set (Var "ri")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "li"))) & (Bool "(" "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "xi")) ($#r2_hidden :::"in"::: ) "Gi")) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "li")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "xi")))) & (Bool (Bool "not" (Set (Var "xi")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "ri")))) ")" ) ")" ) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"Gap"::: CHAIN_1:def 5 : (Bool "for" (Set (Var "Gi")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Var "Gi"))) "iff" (Bool "ex" (Set (Var "li")) "," (Set (Var "ri")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "li")) "," (Set (Var "ri")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "li")) ($#r2_hidden :::"in"::: ) (Set (Var "Gi"))) & (Bool (Set (Var "ri")) ($#r2_hidden :::"in"::: ) (Set (Var "Gi"))) & (Bool "(" (Bool "(" (Bool (Set (Var "li")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "ri"))) & (Bool "(" "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "xi")) ($#r2_hidden :::"in"::: ) (Set (Var "Gi"))) & (Bool (Set (Var "li")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "xi")))) "holds" (Bool "not" (Bool (Set (Var "xi")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "ri")))) ")" ) ")" ) "or" (Bool "(" (Bool (Set (Var "ri")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "li"))) & (Bool "(" "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "xi")) ($#r2_hidden :::"in"::: ) (Set (Var "Gi")))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "li")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "xi")))) & (Bool (Bool "not" (Set (Var "xi")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "ri")))) ")" ) ")" ) ")" ) ")" ) ")" )) ")" ))); theorem :: CHAIN_1:16 (Bool "for" (Set (Var "Gi")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "li")) "," (Set (Var "ri")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "li")) "," (Set (Var "ri")) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Var "Gi"))) "iff" (Bool "(" (Bool (Set (Var "li")) ($#r2_hidden :::"in"::: ) (Set (Var "Gi"))) & (Bool (Set (Var "ri")) ($#r2_hidden :::"in"::: ) (Set (Var "Gi"))) & (Bool "(" (Bool "(" (Bool (Set (Var "li")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "ri"))) & (Bool "(" "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "xi")) ($#r2_hidden :::"in"::: ) (Set (Var "Gi"))) & (Bool (Set (Var "li")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "xi")))) "holds" (Bool "not" (Bool (Set (Var "xi")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "ri")))) ")" ) ")" ) "or" (Bool "(" (Bool (Set (Var "ri")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "li"))) & (Bool "(" "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "xi")) ($#r2_hidden :::"in"::: ) (Set (Var "Gi")))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "li")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "xi")))) & (Bool (Bool "not" (Set (Var "xi")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "ri")))) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ))) ; theorem :: CHAIN_1:17 (Bool "for" (Set (Var "Gi")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "li")) "," (Set (Var "ri")) "," (Set (Var "li9")) "," (Set (Var "ri9")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "Gi")) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "li")) "," (Set (Var "ri")) ($#k7_domain_1 :::"}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "li9")) "," (Set (Var "ri9")) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Var "Gi"))) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "li9")) ($#r1_hidden :::"="::: ) (Set (Var "li"))) & (Bool (Set (Var "ri9")) ($#r1_hidden :::"="::: ) (Set (Var "ri"))) ")" ) "or" (Bool "(" (Bool (Set (Var "li9")) ($#r1_hidden :::"="::: ) (Set (Var "ri"))) & (Bool (Set (Var "ri9")) ($#r1_hidden :::"="::: ) (Set (Var "li"))) ")" ) ")" ) ")" ))) ; theorem :: CHAIN_1:18 (Bool "for" (Set (Var "Gi")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "xi")) ($#r2_hidden :::"in"::: ) (Set (Var "Gi")))) "holds" (Bool "ex" (Set (Var "ri")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "xi")) "," (Set (Var "ri")) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Var "Gi")))))) ; theorem :: CHAIN_1:19 (Bool "for" (Set (Var "Gi")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "xi")) ($#r2_hidden :::"in"::: ) (Set (Var "Gi")))) "holds" (Bool "ex" (Set (Var "li")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "li")) "," (Set (Var "xi")) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Var "Gi")))))) ; theorem :: CHAIN_1:20 (Bool "for" (Set (Var "Gi")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "li")) "," (Set (Var "ri")) "," (Set (Var "ri9")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "li")) "," (Set (Var "ri")) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Var "Gi"))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "li")) "," (Set (Var "ri9")) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Var "Gi")))) "holds" (Bool (Set (Var "ri")) ($#r1_hidden :::"="::: ) (Set (Var "ri9"))))) ; theorem :: CHAIN_1:21 (Bool "for" (Set (Var "Gi")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "li")) "," (Set (Var "ri")) "," (Set (Var "li9")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "li")) "," (Set (Var "ri")) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Var "Gi"))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "li9")) "," (Set (Var "ri")) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Var "Gi")))) "holds" (Bool (Set (Var "li")) ($#r1_hidden :::"="::: ) (Set (Var "li9"))))) ; theorem :: CHAIN_1:22 (Bool "for" (Set (Var "Gi")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "ri")) "," (Set (Var "li")) "," (Set (Var "ri9")) "," (Set (Var "li9")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "ri")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "li"))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "li")) "," (Set (Var "ri")) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Var "Gi"))) & (Bool (Set (Var "ri9")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "li9"))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "li9")) "," (Set (Var "ri9")) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Var "Gi")))) "holds" (Bool "(" (Bool (Set (Var "li")) ($#r1_hidden :::"="::: ) (Set (Var "li9"))) & (Bool (Set (Var "ri")) ($#r1_hidden :::"="::: ) (Set (Var "ri9"))) ")" ))) ; definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "l", "r" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "d"))); func :::"cell"::: "(" "l" "," "r" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "d" ")" ) equals :: CHAIN_1:def 6 "{" (Set (Var "x")) where x "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "d") : (Bool "(" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) "d") "holds" (Bool "(" (Bool (Set "l" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set "r" ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" )) "or" (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) "d") "st" (Bool "(" (Bool (Set "r" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set "l" ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set "r" ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) "or" (Bool (Set "l" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" )) ")" ) "}" ; end; :: deftheorem defines :::"cell"::: CHAIN_1:def 6 : (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) "holds" (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) : (Bool "(" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" )) "or" (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "st" (Bool "(" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) "or" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" )) ")" ) "}" ))); theorem :: CHAIN_1:23 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" )) "iff" (Bool "(" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" )) "or" (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "st" (Bool "(" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) "or" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" )) ")" ) ")" ))) ; theorem :: CHAIN_1:24 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "," (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" )) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" )) ")" ))) ; theorem :: CHAIN_1:25 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "," (Set (Var "l")) "," (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) "st" (Bool (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "st" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" )) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "st" (Bool "(" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) "or" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" )) ")" ))) ; theorem :: CHAIN_1:26 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" )) & (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" )) ")" ))) ; theorem :: CHAIN_1:27 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) "holds" (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "x")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: CHAIN_1:28 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l9")) "," (Set (Var "r9")) "," (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool "(" (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l9")) "," (Set (Var "r9")) ")" )) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" )) ")" ))) ; theorem :: CHAIN_1:29 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "," (Set (Var "l")) "," (Set (Var "l9")) "," (Set (Var "r9")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool "(" (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l9")) "," (Set (Var "r9")) ")" )) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" )) ")" ))) ; theorem :: CHAIN_1:30 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "," (Set (Var "r9")) "," (Set (Var "l9")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool "(" (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l9")) "," (Set (Var "r9")) ")" )) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "st" (Bool "(" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) "or" (Bool (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" )) ")" ))) ; theorem :: CHAIN_1:31 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "," (Set (Var "l9")) "," (Set (Var "r9")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) "st" (Bool (Bool "(" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))) "or" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))) ")" )) "holds" (Bool "(" (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l9")) "," (Set (Var "r9")) ")" )) "iff" (Bool "(" (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Var "l9"))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Var "r9"))) ")" ) ")" ))) ; definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); assume (Bool (Set (Const "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Const "d"))) ; func :::"cells"::: "(" "k" "," "G" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "d" ")" ) equals :: CHAIN_1:def 7 "{" (Set "(" ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ")" ) where l, r "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "d") : (Bool "(" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "d" ")" ) "st" (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "k") & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) "d") "holds" (Bool "(" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set "G" ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set "G" ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" ) ")" )) "or" (Bool "(" (Bool "k" ($#r1_hidden :::"="::: ) "d") & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) "d") "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set "G" ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" ) ")" ) "}" ; end; :: deftheorem defines :::"cells"::: CHAIN_1:def 7 : (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d")))) "holds" (Bool (Set ($#k4_chain_1 :::"cells"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ")" ) where l, r "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) : (Bool "(" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d")) ")" ) "st" (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" ) ")" )) "or" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Var "d"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" ) ")" ) "}" )))); theorem :: CHAIN_1:32 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "d")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" )) "iff" (Bool "ex" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" )) & (Bool "(" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d")) ")" ) "st" (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" ) ")" )) "or" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Var "d"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" ) ")" ) ")" )) ")" ))))) ; theorem :: CHAIN_1:33 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d")))) "holds" (Bool "(" (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" )) "iff" (Bool "(" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d")) ")" ) "st" (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" ) ")" )) "or" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Var "d"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" ) ")" ) ")" ))))) ; theorem :: CHAIN_1:34 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d"))) & (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" )) & (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "st" (Bool "(" (Bool "not" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" )) ")" ))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" )))))) ; theorem :: CHAIN_1:35 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d"))) & (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" ))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" )))))) ; theorem :: CHAIN_1:36 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d"))) & (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" )) & (Bool "not" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))))))) ; theorem :: CHAIN_1:37 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "d")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "G")) ")" )) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "x")) "," (Set (Var "x")) ")" )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" )) ")" )))) ; theorem :: CHAIN_1:38 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "holds" (Bool "(" (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "G")) ")" )) "iff" (Bool "(" (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" )))) ; theorem :: CHAIN_1:39 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "d")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Set (Var "d")) "," (Set (Var "G")) ")" )) "iff" (Bool "ex" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) & (Bool "(" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))) "or" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))) ")" ) ")" )) ")" )))) ; theorem :: CHAIN_1:40 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "holds" (Bool "(" (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Set (Var "d")) "," (Set (Var "G")) ")" )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) & (Bool "(" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))) "or" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))) ")" ) ")" ) ")" )))) ; theorem :: CHAIN_1:41 (Bool "for" (Set (Var "d9")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "st" (Bool (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "d9")) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "d")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Set (Var "d9")) "," (Set (Var "G")) ")" )) "iff" (Bool "ex" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d")))(Bool "ex" (Set (Var "i0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" )) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0")))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i0")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "i0")))) "holds" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" ))) ")" ))))) ; theorem :: CHAIN_1:42 (Bool "for" (Set (Var "d9")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "st" (Bool (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "d9")) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "(" (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Set (Var "d9")) "," (Set (Var "G")) ")" )) "iff" (Bool "ex" (Set (Var "i0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "st" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0")))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i0")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "i0")))) "holds" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" )) ")" ))))) ; theorem :: CHAIN_1:43 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "d")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Num 1) "," (Set (Var "G")) ")" )) "iff" (Bool "ex" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d")))(Bool "ex" (Set (Var "i0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" )) & (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0")))) "or" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0")))) ")" ) ")" ) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i0")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "i0")))) "holds" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" ))) ")" )))) ; theorem :: CHAIN_1:44 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "holds" (Bool "(" (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Num 1) "," (Set (Var "G")) ")" )) "iff" (Bool "ex" (Set (Var "i0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "st" (Bool "(" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0")))) "or" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0")))) ")" ) ")" ) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i0")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i0")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "i0")))) "holds" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" )) ")" )))) ; theorem :: CHAIN_1:45 (Bool "for" (Set (Var "k")) "," (Set (Var "k9")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "," (Set (Var "l9")) "," (Set (Var "r9")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d"))) & (Bool (Set (Var "k9")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d"))) & (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" )) & (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l9")) "," (Set (Var "r9")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Set (Var "k9")) "," (Set (Var "G")) ")" )) & (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l9")) "," (Set (Var "r9")) ")" ))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" )))))) ; theorem :: CHAIN_1:46 (Bool "for" (Set (Var "k")) "," (Set (Var "k9")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "," (Set (Var "l9")) "," (Set (Var "r9")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k9"))) & (Bool (Set (Var "k9")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d"))) & (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" )) & (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l9")) "," (Set (Var "r9")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Set (Var "k9")) "," (Set (Var "G")) ")" )) & (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l9")) "," (Set (Var "r9")) ")" ))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "st" (Bool "(" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) "or" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" )))))) ; theorem :: CHAIN_1:47 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "," (Set (Var "l9")) "," (Set (Var "r9")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "X")) "," (Set (Var "X9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d")) ")" ) "st" (Bool (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l9")) "," (Set (Var "r9")) ")" )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X9"))) & (Bool (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X9")))) & (Bool (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "X9"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "st" (Bool (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "or" "not" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X9"))) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "st" (Bool (Bool (Bool "not" (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X9"))) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "l9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ))) "holds" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r9")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" ))))) ; definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); mode Cell of "k" "," "G" is ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_chain_1 :::"cells"::: ) "(" "k" "," "G" ")" ); end; definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); mode Chain of "k" "," "G" is ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_chain_1 :::"cells"::: ) "(" "k" "," "G" ")" ")" ); end; definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"0_"::: "(" "k" "," "G" ")" -> ($#m1_subset_1 :::"Chain":::) "of" "k" "," "G" equals :: CHAIN_1:def 8 (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"0_"::: CHAIN_1:def 8 : (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_chain_1 :::"0_"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))); definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); func :::"Omega"::: "G" -> ($#m1_subset_1 :::"Chain":::) "of" "d" "," "G" equals :: CHAIN_1:def 9 (Set ($#k4_chain_1 :::"cells"::: ) "(" "d" "," "G" ")" ); end; :: deftheorem defines :::"Omega"::: CHAIN_1:def 9 : (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "holds" (Bool (Set ($#k6_chain_1 :::"Omega"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k4_chain_1 :::"cells"::: ) "(" (Set (Var "d")) "," (Set (Var "G")) ")" )))); notationlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "C1", "C2" be ($#m1_subset_1 :::"Chain":::) "of" (Set (Const "k")) "," (Set (Const "G")); synonym "C1" :::"+"::: "C2" for "d" :::"\+\"::: "G"; end; definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "C1", "C2" be ($#m1_subset_1 :::"Chain":::) "of" (Set (Const "k")) "," (Set (Const "G")); :: original: :::"+"::: redefine func "C1" :::"+"::: "C2" -> ($#m1_subset_1 :::"Chain":::) "of" "k" "," "G"; end; definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); func :::"infinite-cell"::: "G" -> ($#m2_subset_1 :::"Cell":::) "of" "d" "," "G" means :: CHAIN_1:def 10 (Bool "ex" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "d") "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) "d") "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set "G" ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"infinite-cell"::: CHAIN_1:def 10 : (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "b3")) "being" ($#m2_subset_1 :::"Cell":::) "of" (Set (Var "d")) "," (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_chain_1 :::"infinite-cell"::: ) (Set (Var "G")))) "iff" (Bool "ex" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" )) ")" )))); theorem :: CHAIN_1:48 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "st" (Bool (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) "is" ($#m2_subset_1 :::"Cell":::) "of" (Set (Var "d")) "," (Set (Var "G")))) "holds" (Bool "(" (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_chain_1 :::"infinite-cell"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))) ")" )))) ; theorem :: CHAIN_1:49 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "d"))) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "holds" (Bool "(" (Bool (Set ($#k3_chain_1 :::"cell"::: ) "(" (Set (Var "l")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_chain_1 :::"infinite-cell"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "d"))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "is" ($#m2_chain_1 :::"Gap"::: ) "of" (Set (Set (Var "G")) ($#k2_chain_1 :::"."::: ) (Set (Var "i")))) ")" )) ")" )))) ; scheme :: CHAIN_1:sch 4 ChainInd{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F2() -> ($#m1_chain_1 :::"Grating"::: ) "of" (Set F1 "(" ")" ), F3() -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F4() -> ($#m1_subset_1 :::"Chain":::) "of" (Set F3 "(" ")" ) "," (Set F2 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool P1[(Set F4 "(" ")" )]) provided (Bool P1[(Set ($#k5_chain_1 :::"0_"::: ) "(" (Set F3 "(" ")" ) "," (Set F2 "(" ")" ) ")" )]) and (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Cell":::) "of" (Set F3 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set F4 "(" ")" ))) "holds" (Bool P1[(Set ($#k6_domain_1 :::"{"::: ) (Set (Var "A")) ($#k6_domain_1 :::"}"::: ) )])) and (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set F3 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "C1")) ($#r1_tarski :::"c="::: ) (Set F4 "(" ")" )) & (Bool (Set (Var "C2")) ($#r1_tarski :::"c="::: ) (Set F4 "(" ")" )) & (Bool P1[(Set (Var "C1"))]) & (Bool P1[(Set (Var "C2"))])) "holds" (Bool P1[(Set (Set (Var "C1")) ($#k7_chain_1 :::"+"::: ) (Set (Var "C2")))])) proof end; definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "A" be ($#m2_subset_1 :::"Cell":::) "of" (Set (Const "k")) "," (Set (Const "G")); func :::"star"::: "A" -> ($#m1_subset_1 :::"Chain":::) "of" (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "G" equals :: CHAIN_1:def 11 "{" (Set (Var "B")) where B "is" ($#m2_subset_1 :::"Cell":::) "of" (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "G" : (Bool "A" ($#r1_tarski :::"c="::: ) (Set (Var "B"))) "}" ; end; :: deftheorem defines :::"star"::: CHAIN_1:def 11 : (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Cell":::) "of" (Set (Var "k")) "," (Set (Var "G")) "holds" (Bool (Set ($#k9_chain_1 :::"star"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m2_subset_1 :::"Cell":::) "of" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "G")) : (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) "}" ))))); theorem :: CHAIN_1:50 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Cell":::) "of" (Set (Var "k")) "," (Set (Var "G")) (Bool "for" (Set (Var "B")) "being" ($#m2_subset_1 :::"Cell":::) "of" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k9_chain_1 :::"star"::: ) (Set (Var "A")))) "iff" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) ")" )))))) ; definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "C" be ($#m1_subset_1 :::"Chain":::) "of" (Set "(" (Set (Const "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Const "G")); func :::"del"::: "C" -> ($#m1_subset_1 :::"Chain":::) "of" "k" "," "G" equals :: CHAIN_1:def 12 "{" (Set (Var "A")) where A "is" ($#m2_subset_1 :::"Cell":::) "of" "k" "," "G" : (Bool "(" (Bool (Set "k" ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) "d") & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" ($#k9_chain_1 :::"star"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) "C" ")" )) "is" ($#v1_abian :::"odd"::: ) ) ")" ) "}" ; end; :: deftheorem defines :::"del"::: CHAIN_1:def 12 : (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "G")) "holds" (Bool (Set ($#k10_chain_1 :::"del"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "A")) where A "is" ($#m2_subset_1 :::"Cell":::) "of" (Set (Var "k")) "," (Set (Var "G")) : (Bool "(" (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d"))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" ($#k9_chain_1 :::"star"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C")) ")" )) "is" ($#v1_abian :::"odd"::: ) ) ")" ) "}" ))))); notationlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "C" be ($#m1_subset_1 :::"Chain":::) "of" (Set "(" (Set (Const "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Const "G")); synonym :::"."::: "C" for :::"del"::: "C"; end; definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "C" be ($#m1_subset_1 :::"Chain":::) "of" (Set "(" (Set (Const "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Const "G")); let "C9" be ($#m1_subset_1 :::"Chain":::) "of" (Set (Const "k")) "," (Set (Const "G")); pred "C9" :::"bounds"::: "C" means :: CHAIN_1:def 13 (Bool "C9" ($#r1_hidden :::"="::: ) (Set ($#k10_chain_1 :::"del"::: ) "C")); end; :: deftheorem defines :::"bounds"::: CHAIN_1:def 13 : (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "G")) (Bool "for" (Set (Var "C9")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "k")) "," (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "C9")) ($#r1_chain_1 :::"bounds"::: ) (Set (Var "C"))) "iff" (Bool (Set (Var "C9")) ($#r1_hidden :::"="::: ) (Set ($#k10_chain_1 :::"del"::: ) (Set (Var "C")))) ")" )))))); theorem :: CHAIN_1:51 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Cell":::) "of" (Set (Var "k")) "," (Set (Var "G")) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k10_chain_1 :::"del"::: ) (Set (Var "C")))) "iff" (Bool "(" (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d"))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" ($#k9_chain_1 :::"star"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C")) ")" )) "is" ($#v1_abian :::"odd"::: ) ) ")" ) ")" )))))) ; theorem :: CHAIN_1:52 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "st" (Bool (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::">"::: ) (Set (Var "d")))) "holds" (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "G")) "holds" (Bool (Set ($#k10_chain_1 :::"del"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_chain_1 :::"0_"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" )))))) ; theorem :: CHAIN_1:53 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "st" (Bool (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Cell":::) "of" (Set (Var "k")) "," (Set (Var "G")) (Bool "for" (Set (Var "B")) "being" ($#m2_subset_1 :::"Cell":::) "of" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k10_chain_1 :::"del"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "B")) ($#k6_domain_1 :::"}"::: ) ))) "iff" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) ")" )))))) ; theorem :: CHAIN_1:54 (Bool "for" (Set (Var "d9")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "st" (Bool (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "d9")) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Cell":::) "of" (Set (Var "d9")) "," (Set (Var "G")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k9_chain_1 :::"star"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Num 2)))))) ; theorem :: CHAIN_1:55 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "B")) "being" ($#m2_subset_1 :::"Cell":::) "of" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "G")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k10_chain_1 :::"del"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "B")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 2))))) ; theorem :: CHAIN_1:56 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "holds" (Bool "(" (Bool (Set ($#k6_chain_1 :::"Omega"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_chain_1 :::"0_"::: ) "(" (Set (Var "d")) "," (Set (Var "G")) ")" ")" ) ($#k3_subset_1 :::"`"::: ) )) & (Bool (Set ($#k5_chain_1 :::"0_"::: ) "(" (Set (Var "d")) "," (Set (Var "G")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_chain_1 :::"Omega"::: ) (Set (Var "G")) ")" ) ($#k3_subset_1 :::"`"::: ) )) ")" ))) ; theorem :: CHAIN_1:57 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "k")) "," (Set (Var "G")) "holds" (Bool (Set (Set (Var "C")) ($#k7_chain_1 :::"+"::: ) (Set "(" ($#k5_chain_1 :::"0_"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "C"))))))) ; theorem :: CHAIN_1:58 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "d")) "," (Set (Var "G")) "holds" (Bool (Set (Set (Var "C")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k7_chain_1 :::"+"::: ) (Set "(" ($#k6_chain_1 :::"Omega"::: ) (Set (Var "G")) ")" )))))) ; theorem :: CHAIN_1:59 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "holds" (Bool (Set ($#k10_chain_1 :::"del"::: ) (Set "(" ($#k5_chain_1 :::"0_"::: ) "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "G")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_chain_1 :::"0_"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" ))))) ; theorem :: CHAIN_1:60 (Bool "for" (Set (Var "d9")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Set (Var "d9")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "holds" (Bool (Set ($#k10_chain_1 :::"del"::: ) (Set "(" ($#k6_chain_1 :::"Omega"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_chain_1 :::"0_"::: ) "(" (Set (Var "d9")) "," (Set (Var "G")) ")" )))) ; theorem :: CHAIN_1:61 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "G")) "holds" (Bool (Set ($#k10_chain_1 :::"del"::: ) (Set "(" (Set (Var "C1")) ($#k7_chain_1 :::"+"::: ) (Set (Var "C2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_chain_1 :::"del"::: ) (Set (Var "C1")) ")" ) ($#k7_chain_1 :::"+"::: ) (Set "(" ($#k10_chain_1 :::"del"::: ) (Set (Var "C2")) ")" ))))))) ; theorem :: CHAIN_1:62 (Bool "for" (Set (Var "d9")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Set (Var "d9")) ($#k2_nat_1 :::"+"::: ) (Num 1)) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set "(" (Set (Var "d9")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "G")) "holds" (Bool (Set ($#k10_chain_1 :::"del"::: ) (Set "(" (Set (Var "C")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_chain_1 :::"del"::: ) (Set (Var "C"))))))) ; theorem :: CHAIN_1:63 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "G")) "holds" (Bool (Set ($#k10_chain_1 :::"del"::: ) (Set "(" ($#k10_chain_1 :::"del"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_chain_1 :::"0_"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" )))))) ; definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); mode :::"Cycle"::: "of" "k" "," "G" -> ($#m1_subset_1 :::"Chain":::) "of" "k" "," "G" means :: CHAIN_1:def 14 (Bool "(" (Bool "(" (Bool "k" ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k5_card_1 :::"card"::: ) it) "is" ($#v1_abian :::"even"::: ) ) ")" ) "or" (Bool "ex" (Set (Var "k9")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool "k" ($#r1_hidden :::"="::: ) (Set (Set (Var "k9")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set "(" (Set (Var "k9")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "G" "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) it) & (Bool (Set ($#k10_chain_1 :::"del"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_chain_1 :::"0_"::: ) "(" (Set (Var "k9")) "," "G" ")" )) ")" )) ")" )) ")" ); end; :: deftheorem defines :::"Cycle"::: CHAIN_1:def 14 : (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "k")) "," (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m3_chain_1 :::"Cycle"::: ) "of" (Set (Var "k")) "," (Set (Var "G"))) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "b4"))) "is" ($#v1_abian :::"even"::: ) ) ")" ) "or" (Bool "ex" (Set (Var "k9")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set (Var "k9")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set "(" (Set (Var "k9")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Var "b4"))) & (Bool (Set ($#k10_chain_1 :::"del"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_chain_1 :::"0_"::: ) "(" (Set (Var "k9")) "," (Set (Var "G")) ")" )) ")" )) ")" )) ")" ) ")" ))))); theorem :: CHAIN_1:64 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#m3_chain_1 :::"Cycle"::: ) "of" (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "," (Set (Var "G"))) "iff" (Bool (Set ($#k10_chain_1 :::"del"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_chain_1 :::"0_"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" )) ")" ))))) ; theorem :: CHAIN_1:65 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "d")))) "holds" (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "k")) "," (Set (Var "G")) "holds" (Bool (Set (Var "C")) "is" ($#m3_chain_1 :::"Cycle"::: ) "of" (Set (Var "k")) "," (Set (Var "G"))))))) ; theorem :: CHAIN_1:66 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#m3_chain_1 :::"Cycle"::: ) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "G"))) "iff" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) "is" ($#v1_abian :::"even"::: ) ) ")" )))) ; definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "C" be ($#m3_chain_1 :::"Cycle"::: ) "of" (Set (Set (Const "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "," (Set (Const "G")); redefine func :::"del"::: "C" equals :: CHAIN_1:def 15 (Set ($#k5_chain_1 :::"0_"::: ) "(" "k" "," "G" ")" ); end; :: deftheorem defines :::"del"::: CHAIN_1:def 15 : (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#m3_chain_1 :::"Cycle"::: ) "of" (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "," (Set (Var "G")) "holds" (Bool (Set ($#k10_chain_1 :::"del"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_chain_1 :::"0_"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" )))))); definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"0_"::: redefine func :::"0_"::: "(" "k" "," "G" ")" -> ($#m3_chain_1 :::"Cycle"::: ) "of" "k" "," "G"; end; definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); :: original: :::"Omega"::: redefine func :::"Omega"::: "G" -> ($#m3_chain_1 :::"Cycle"::: ) "of" "d" "," "G"; end; definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "C1", "C2" be ($#m3_chain_1 :::"Cycle"::: ) "of" (Set (Const "k")) "," (Set (Const "G")); :: original: :::"+"::: redefine func "C1" :::"+"::: "C2" -> ($#m3_chain_1 :::"Cycle"::: ) "of" "k" "," "G"; end; theorem :: CHAIN_1:67 (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "C")) "being" ($#m3_chain_1 :::"Cycle"::: ) "of" (Set (Var "d")) "," (Set (Var "G")) "holds" (Bool (Set (Set (Var "C")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#m3_chain_1 :::"Cycle"::: ) "of" (Set (Var "d")) "," (Set (Var "G")))))) ; definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "C" be ($#m1_subset_1 :::"Chain":::) "of" (Set "(" (Set (Const "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Const "G")); :: original: :::"del"::: redefine func :::"del"::: "C" -> ($#m3_chain_1 :::"Cycle"::: ) "of" "k" "," "G"; end; begin definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Chains"::: "(" "k" "," "G" ")" -> ($#v8_algstr_0 :::"strict"::: ) ($#l2_algstr_0 :::"AbGroup":::) means :: CHAIN_1:def 16 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_chain_1 :::"bool"::: ) (Set "(" ($#k4_chain_1 :::"cells"::: ) "(" "k" "," "G" ")" ")" ))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k11_chain_1 :::"0_"::: ) "(" "k" "," "G" ")" )) & (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element":::) "of" it (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m1_subset_1 :::"Chain":::) "of" "k" "," "G" "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "A9"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "B9")))) "holds" (Bool (Set (Set (Var "A")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A9")) ($#k7_chain_1 :::"+"::: ) (Set (Var "B9"))))) ")" ) ")" ); end; :: deftheorem defines :::"Chains"::: CHAIN_1:def 16 : (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#v8_algstr_0 :::"strict"::: ) ($#l2_algstr_0 :::"AbGroup":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k15_chain_1 :::"Chains"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k1_chain_1 :::"bool"::: ) (Set "(" ($#k4_chain_1 :::"cells"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" ")" ))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k11_chain_1 :::"0_"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" )) & (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b4")) (Bool "for" (Set (Var "A9")) "," (Set (Var "B9")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "k")) "," (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "A9"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "B9")))) "holds" (Bool (Set (Set (Var "A")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A9")) ($#k7_chain_1 :::"+"::: ) (Set (Var "B9"))))) ")" ) ")" ) ")" ))))); definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); mode GrChain of "k" "," "G" is ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_chain_1 :::"Chains"::: ) "(" "k" "," "G" ")" ")" ); end; theorem :: CHAIN_1:68 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "k")) "," (Set (Var "G"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"GrChain":::) "of" (Set (Var "k")) "," (Set (Var "G"))) ")" ))))) ; definitionlet "d" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "G" be ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Const "d")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"del"::: "(" "k" "," "G" ")" -> ($#m1_subset_1 :::"Homomorphism":::) "of" (Set "(" ($#k15_chain_1 :::"Chains"::: ) "(" (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "G" ")" ")" ) "," (Set "(" ($#k15_chain_1 :::"Chains"::: ) "(" "k" "," "G" ")" ")" ) means :: CHAIN_1:def 17 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_chain_1 :::"Chains"::: ) "(" (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "G" ")" ")" ) (Bool "for" (Set (Var "A9")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set "(" "k" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "G" "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "A9")))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k14_chain_1 :::"del"::: ) (Set (Var "A9")))))); end; :: deftheorem defines :::"del"::: CHAIN_1:def 17 : (Bool "for" (Set (Var "d")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_chain_1 :::"Grating"::: ) "of" (Set (Var "d")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set "(" ($#k15_chain_1 :::"Chains"::: ) "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "G")) ")" ")" ) "," (Set "(" ($#k15_chain_1 :::"Chains"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k16_chain_1 :::"del"::: ) "(" (Set (Var "k")) "," (Set (Var "G")) ")" )) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_chain_1 :::"Chains"::: ) "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "G")) ")" ")" ) (Bool "for" (Set (Var "A9")) "being" ($#m1_subset_1 :::"Chain":::) "of" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "A9")))) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k14_chain_1 :::"del"::: ) (Set (Var "A9")))))) ")" )))));