:: REWRITE1 semantic presentation begin definitionlet "p", "q" be ($#m1_hidden :::"FinSequence":::); func "p" :::"$^"::: "q" -> ($#m1_hidden :::"FinSequence":::) means :: REWRITE1:def 1 (Bool it ($#r1_hidden :::"="::: ) (Set "p" ($#k7_finseq_1 :::"^"::: ) "q")) if (Bool "(" (Bool "p" ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool "q" ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) otherwise (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "p") ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set "p" ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ))) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k7_finseq_1 :::"^"::: ) "q")) ")" ))); end; :: deftheorem defines :::"$^"::: REWRITE1:def 1 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_rewrite1 :::"$^"::: ) (Set (Var "q")))) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")))) ")" ) ")" & (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_rewrite1 :::"$^"::: ) (Set (Var "q")))) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")))) ")" ))) ")" ) ")" ) ")" )); theorem :: REWRITE1:1 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_rewrite1 :::"$^"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "p")) ($#k1_rewrite1 :::"$^"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) ")" )) ; theorem :: REWRITE1:2 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k1_rewrite1 :::"$^"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")))))) ; theorem :: REWRITE1:3 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k1_rewrite1 :::"$^"::: ) (Set "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")))))) ; theorem :: REWRITE1:4 (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k1_rewrite1 :::"$^"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "q"))))) ; theorem :: REWRITE1:5 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" )))) ; scheme :: REWRITE1:sch 1 PathCatenation{ P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], F1() -> ($#m1_hidden :::"FinSequence":::), F2() -> ($#m1_hidden :::"FinSequence":::) } : (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set F1 "(" ")" ) ($#k1_rewrite1 :::"$^"::: ) (Set F2 "(" ")" ) ")" ))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set F1 "(" ")" ) ($#k1_rewrite1 :::"$^"::: ) (Set F2 "(" ")" ) ")" )))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set F1 "(" ")" ) ($#k1_rewrite1 :::"$^"::: ) (Set F2 "(" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set F1 "(" ")" ) ($#k1_rewrite1 :::"$^"::: ) (Set F2 "(" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]))) provided (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set F1 "(" ")" ))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set F1 "(" ")" )))) "holds" (Bool P1[(Set (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "," (Set (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))])) and (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set F2 "(" ")" ))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set F2 "(" ")" )))) "holds" (Bool P1[(Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "," (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))])) and (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set F1 "(" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set F2 "(" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set F1 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set F1 "(" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1))) ")" ) proof end; definitionlet "R" be ($#m1_hidden :::"Relation":::); mode :::"RedSequence"::: "of" "R" -> ($#m1_hidden :::"FinSequence":::) means :: REWRITE1:def 2 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it)) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" it ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" ) ")" ); end; :: deftheorem defines :::"RedSequence"::: REWRITE1:def 2 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b2")))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b2"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" ) ")" ))); registrationlet "R" be ($#m1_hidden :::"Relation":::); cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_rewrite1 :::"RedSequence"::: ) "of" "R"; end; theorem :: REWRITE1:6 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R"))))) ; theorem :: REWRITE1:7 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R"))))) ; theorem :: REWRITE1:8 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "p")) ($#k1_rewrite1 :::"$^"::: ) (Set (Var "q"))) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R"))))) ; theorem :: REWRITE1:9 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "p")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R")) "holds" (Bool (Set ($#k3_finseq_5 :::"Rev"::: ) (Set (Var "p"))) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) )))) ; theorem :: REWRITE1:10 (Bool "for" (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Var "Q")))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R")) "holds" (Bool (Set (Var "p")) "is" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "Q"))))) ; begin definitionlet "R" be ($#m1_hidden :::"Relation":::); let "a", "b" be ($#m1_hidden :::"set"::: ) ; pred "R" :::"reduces"::: "a" "," "b" means :: REWRITE1:def 3 (Bool "ex" (Set (Var "p")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" "R" "st" (Bool "(" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) "a") & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) "b") ")" )); end; :: deftheorem defines :::"reduces"::: REWRITE1:def 3 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" )) ")" ))); definitionlet "R" be ($#m1_hidden :::"Relation":::); let "a", "b" be ($#m1_hidden :::"set"::: ) ; pred "a" "," "b" :::"are_convertible_wrt"::: "R" means :: REWRITE1:def 4 (Bool (Set "R" ($#k2_xboole_0 :::"\/"::: ) (Set "(" "R" ($#k2_relat_1 :::"~"::: ) ")" )) ($#r1_rewrite1 :::"reduces"::: ) "a" "," "b"); end; :: deftheorem defines :::"are_convertible_wrt"::: REWRITE1:def 4 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))) "iff" (Bool (Set (Set (Var "R")) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ")" )) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ))); theorem :: REWRITE1:11 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" )) ")" ))) ; theorem :: REWRITE1:12 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "a"))))) ; theorem :: REWRITE1:13 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ; theorem :: REWRITE1:14 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: REWRITE1:15 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))))) ; theorem :: REWRITE1:16 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "b")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "c"))))) ; theorem :: REWRITE1:17 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "p")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "," (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))))) ; theorem :: REWRITE1:18 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) ")" ))) ; theorem :: REWRITE1:19 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) "iff" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) ")" ))) ; theorem :: REWRITE1:20 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) "or" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R")) ($#k18_finseq_1 :::"[*]"::: ) )) ")" ) ")" ))) ; theorem :: REWRITE1:21 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) "iff" (Bool (Set (Set (Var "R")) ($#k18_finseq_1 :::"[*]"::: ) ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ))) ; theorem :: REWRITE1:22 (Bool "for" (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Var "Q")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b")))) "holds" (Bool (Set (Var "Q")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))))) ; theorem :: REWRITE1:23 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "X")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) "iff" (Bool (Set (Set (Var "R")) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" )) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ))) ; theorem :: REWRITE1:24 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "b")) "," (Set (Var "a"))))) ; theorem :: REWRITE1:25 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))) ")" ))) ; theorem :: REWRITE1:26 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "a")) "," (Set (Var "a")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))))) ; theorem :: REWRITE1:27 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ; theorem :: REWRITE1:28 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: REWRITE1:29 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))))) ; theorem :: REWRITE1:30 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))))) ; theorem :: REWRITE1:31 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))))) ; theorem :: REWRITE1:32 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) ")" ))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); let "a" be ($#m1_hidden :::"set"::: ) ; pred "a" :::"is_a_normal_form_wrt"::: "R" means :: REWRITE1:def 5 (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Bool "not" (Set ($#k4_tarski :::"["::: ) "a" "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R"))); end; :: deftheorem defines :::"is_a_normal_form_wrt"::: REWRITE1:def 5 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r3_rewrite1 :::"is_a_normal_form_wrt"::: ) (Set (Var "R"))) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Bool "not" (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))))) ")" ))); theorem :: REWRITE1:33 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r3_rewrite1 :::"is_a_normal_form_wrt"::: ) (Set (Var "R"))) & (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: REWRITE1:34 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))))) "holds" (Bool (Set (Var "a")) ($#r3_rewrite1 :::"is_a_normal_form_wrt"::: ) (Set (Var "R"))))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); let "a", "b" be ($#m1_hidden :::"set"::: ) ; pred "b" :::"is_a_normal_form_of"::: "a" "," "R" means :: REWRITE1:def 6 (Bool "(" (Bool "b" ($#r3_rewrite1 :::"is_a_normal_form_wrt"::: ) "R") & (Bool "R" ($#r1_rewrite1 :::"reduces"::: ) "a" "," "b") ")" ); pred "a" "," "b" :::"are_convergent_wrt"::: "R" means :: REWRITE1:def 7 (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "R" ($#r1_rewrite1 :::"reduces"::: ) "a" "," (Set (Var "c"))) & (Bool "R" ($#r1_rewrite1 :::"reduces"::: ) "b" "," (Set (Var "c"))) ")" )); pred "a" "," "b" :::"are_divergent_wrt"::: "R" means :: REWRITE1:def 8 (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "R" ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "c")) "," "a") & (Bool "R" ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "c")) "," "b") ")" )); pred "a" "," "b" :::"are_convergent<=1_wrt"::: "R" means :: REWRITE1:def 9 (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) "a" "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") "or" (Bool "a" ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) & (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) "b" "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") "or" (Bool "b" ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) ")" )); pred "a" "," "b" :::"are_divergent<=1_wrt"::: "R" means :: REWRITE1:def 10 (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," "a" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") "or" (Bool "a" ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) & (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," "b" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") "or" (Bool "b" ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) ")" )); end; :: deftheorem defines :::"is_a_normal_form_of"::: REWRITE1:def 6 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b")) ($#r4_rewrite1 :::"is_a_normal_form_of"::: ) (Set (Var "a")) "," (Set (Var "R"))) "iff" (Bool "(" (Bool (Set (Var "b")) ($#r3_rewrite1 :::"is_a_normal_form_wrt"::: ) (Set (Var "R"))) & (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) ")" ) ")" ))); :: deftheorem defines :::"are_convergent_wrt"::: REWRITE1:def 7 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "R"))) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "c"))) & (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "b")) "," (Set (Var "c"))) ")" )) ")" ))); :: deftheorem defines :::"are_divergent_wrt"::: REWRITE1:def 8 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r6_rewrite1 :::"are_divergent_wrt"::: ) (Set (Var "R"))) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "c")) "," (Set (Var "a"))) & (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "c")) "," (Set (Var "b"))) ")" )) ")" ))); :: deftheorem defines :::"are_convergent<=1_wrt"::: REWRITE1:def 9 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r7_rewrite1 :::"are_convergent<=1_wrt"::: ) (Set (Var "R"))) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) & (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) ")" )) ")" ))); :: deftheorem defines :::"are_divergent<=1_wrt"::: REWRITE1:def 10 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r8_rewrite1 :::"are_divergent<=1_wrt"::: ) (Set (Var "R"))) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) & (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) ")" )) ")" ))); theorem :: REWRITE1:35 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))))) "holds" (Bool (Set (Var "a")) ($#r4_rewrite1 :::"is_a_normal_form_of"::: ) (Set (Var "a")) "," (Set (Var "R"))))) ; theorem :: REWRITE1:36 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "R"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r6_rewrite1 :::"are_divergent_wrt"::: ) (Set (Var "R"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "R"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r6_rewrite1 :::"are_divergent_wrt"::: ) (Set (Var "R"))) ")" ))) ; theorem :: REWRITE1:37 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "R"))) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r6_rewrite1 :::"are_divergent_wrt"::: ) (Set (Var "R"))) ")" )) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))))) ; theorem :: REWRITE1:38 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "a")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "R"))) & (Bool (Set (Var "a")) "," (Set (Var "a")) ($#r6_rewrite1 :::"are_divergent_wrt"::: ) (Set (Var "R"))) ")" ))) ; theorem :: REWRITE1:39 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r6_rewrite1 :::"are_divergent_wrt"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ; theorem :: REWRITE1:40 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "R"))))) ; theorem :: REWRITE1:41 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r6_rewrite1 :::"are_divergent_wrt"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r6_rewrite1 :::"are_divergent_wrt"::: ) (Set (Var "R"))))) ; theorem :: REWRITE1:42 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool "(" (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "R"))) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "R"))) & (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "c")) "," (Set (Var "b"))) ")" ) ")" )) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "R"))))) ; theorem :: REWRITE1:43 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool "(" (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r6_rewrite1 :::"are_divergent_wrt"::: ) (Set (Var "R"))) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r6_rewrite1 :::"are_divergent_wrt"::: ) (Set (Var "R"))) & (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "b")) "," (Set (Var "c"))) ")" ) ")" )) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r6_rewrite1 :::"are_divergent_wrt"::: ) (Set (Var "R"))))) ; theorem :: REWRITE1:44 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r7_rewrite1 :::"are_convergent<=1_wrt"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "R"))))) ; theorem :: REWRITE1:45 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r8_rewrite1 :::"are_divergent<=1_wrt"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r6_rewrite1 :::"are_divergent_wrt"::: ) (Set (Var "R"))))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); let "a" be ($#m1_hidden :::"set"::: ) ; pred "a" :::"has_a_normal_form_wrt"::: "R" means :: REWRITE1:def 11 (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "b")) ($#r4_rewrite1 :::"is_a_normal_form_of"::: ) "a" "," "R")); end; :: deftheorem defines :::"has_a_normal_form_wrt"::: REWRITE1:def 11 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r9_rewrite1 :::"has_a_normal_form_wrt"::: ) (Set (Var "R"))) "iff" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "b")) ($#r4_rewrite1 :::"is_a_normal_form_of"::: ) (Set (Var "a")) "," (Set (Var "R")))) ")" ))); theorem :: REWRITE1:46 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))))) "holds" (Bool (Set (Var "a")) ($#r9_rewrite1 :::"has_a_normal_form_wrt"::: ) (Set (Var "R"))))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); let "a" be ($#m1_hidden :::"set"::: ) ; assume that (Bool (Set (Const "a")) ($#r9_rewrite1 :::"has_a_normal_form_wrt"::: ) (Set (Const "R"))) and (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r4_rewrite1 :::"is_a_normal_form_of"::: ) (Set (Const "a")) "," (Set (Const "R"))) & (Bool (Set (Var "c")) ($#r4_rewrite1 :::"is_a_normal_form_of"::: ) (Set (Const "a")) "," (Set (Const "R")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c")))) ; func :::"nf"::: "(" "a" "," "R" ")" -> ($#m1_hidden :::"set"::: ) means :: REWRITE1:def 12 (Bool it ($#r4_rewrite1 :::"is_a_normal_form_of"::: ) "a" "," "R"); end; :: deftheorem defines :::"nf"::: REWRITE1:def 12 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r9_rewrite1 :::"has_a_normal_form_wrt"::: ) (Set (Var "R"))) & (Bool "(" "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r4_rewrite1 :::"is_a_normal_form_of"::: ) (Set (Var "a")) "," (Set (Var "R"))) & (Bool (Set (Var "c")) ($#r4_rewrite1 :::"is_a_normal_form_of"::: ) (Set (Var "a")) "," (Set (Var "R")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_rewrite1 :::"nf"::: ) "(" (Set (Var "a")) "," (Set (Var "R")) ")" )) "iff" (Bool (Set (Var "b3")) ($#r4_rewrite1 :::"is_a_normal_form_of"::: ) (Set (Var "a")) "," (Set (Var "R"))) ")" )))); begin definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"co-well_founded"::: means :: REWRITE1:def 13 (Bool (Set "R" ($#k2_relat_1 :::"~"::: ) ) "is" ($#v1_wellord1 :::"well_founded"::: ) ); attr "R" is :::"weakly-normalizing"::: means :: REWRITE1:def 14 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) "R"))) "holds" (Bool (Set (Var "a")) ($#r9_rewrite1 :::"has_a_normal_form_wrt"::: ) "R")); attr "R" is :::"strongly-normalizing"::: means :: REWRITE1:def 15 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "not" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R")))); end; :: deftheorem defines :::"co-well_founded"::: REWRITE1:def 13 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_rewrite1 :::"co-well_founded"::: ) ) "iff" (Bool (Set (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ) "is" ($#v1_wellord1 :::"well_founded"::: ) ) ")" )); :: deftheorem defines :::"weakly-normalizing"::: REWRITE1:def 14 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_rewrite1 :::"weakly-normalizing"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Var "a")) ($#r9_rewrite1 :::"has_a_normal_form_wrt"::: ) (Set (Var "R")))) ")" )); :: deftheorem defines :::"strongly-normalizing"::: REWRITE1:def 15 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_rewrite1 :::"strongly-normalizing"::: ) ) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "not" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))))) ")" )); definitionlet "R" be ($#m1_hidden :::"Relation":::); redefine attr "R" is :::"co-well_founded"::: means :: REWRITE1:def 16 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relat_1 :::"field"::: ) "R")) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "not" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R")) ")" ) ")" ))); end; :: deftheorem defines :::"co-well_founded"::: REWRITE1:def 16 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_rewrite1 :::"co-well_founded"::: ) ) "iff" (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "not" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) ")" ) ")" ))) ")" )); scheme :: REWRITE1:sch 2 coNoetherianInduction{ F1() -> ($#m1_hidden :::"Relation":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set F1 "(" ")" )))) "holds" (Bool P1[(Set (Var "a"))])) provided (Bool (Set F1 "(" ")" ) "is" ($#v1_rewrite1 :::"co-well_founded"::: ) ) and (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool P1[(Set (Var "b"))]) ")" )) "holds" (Bool P1[(Set (Var "a"))])) proof end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v3_rewrite1 :::"strongly-normalizing"::: ) -> ($#v2_relat_2 :::"irreflexive"::: ) ($#v1_rewrite1 :::"co-well_founded"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_2 :::"irreflexive"::: ) ($#v1_rewrite1 :::"co-well_founded"::: ) -> ($#v3_rewrite1 :::"strongly-normalizing"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) -> ($#v2_rewrite1 :::"weakly-normalizing"::: ) ($#v3_rewrite1 :::"strongly-normalizing"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: REWRITE1:47 (Bool "for" (Set (Var "Q")) "being" ($#v1_rewrite1 :::"co-well_founded"::: ) ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set (Var "Q")))) "holds" (Bool (Set (Var "R")) "is" ($#v1_rewrite1 :::"co-well_founded"::: ) ))) ; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v3_rewrite1 :::"strongly-normalizing"::: ) -> ($#v2_rewrite1 :::"weakly-normalizing"::: ) for ($#m1_hidden :::"set"::: ) ; end; begin definitionlet "R", "Q" be ($#m1_hidden :::"Relation":::); pred "R" :::"commutes-weakly_with"::: "Q" means :: REWRITE1:def 17 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "Q")) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "Q" ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "b")) "," (Set (Var "d"))) & (Bool "R" ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ))); symmetry (Bool "for" (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "Q")))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Q")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )) ")" )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Set (Var "Q")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )))) ; pred "R" :::"commutes_with"::: "Q" means :: REWRITE1:def 18 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "R" ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool "Q" ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "c")))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "Q" ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "b")) "," (Set (Var "d"))) & (Bool "R" ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ))); symmetry (Bool "for" (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "Q")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "c")))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Q")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )) ")" )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Q")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "c")))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Set (Var "Q")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" )))) ; end; :: deftheorem defines :::"commutes-weakly_with"::: REWRITE1:def 17 : (Bool "for" (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r10_rewrite1 :::"commutes-weakly_with"::: ) (Set (Var "Q"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "Q")))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Q")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ))) ")" )); :: deftheorem defines :::"commutes_with"::: REWRITE1:def 18 : (Bool "for" (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r11_rewrite1 :::"commutes_with"::: ) (Set (Var "Q"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "Q")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "c")))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Q")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ))) ")" )); theorem :: REWRITE1:48 (Bool "for" (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r11_rewrite1 :::"commutes_with"::: ) (Set (Var "Q")))) "holds" (Bool (Set (Var "R")) ($#r10_rewrite1 :::"commutes-weakly_with"::: ) (Set (Var "Q")))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"with_UN_property"::: means :: REWRITE1:def 19 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r3_rewrite1 :::"is_a_normal_form_wrt"::: ) "R") & (Bool (Set (Var "b")) ($#r3_rewrite1 :::"is_a_normal_form_wrt"::: ) "R") & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) "R")) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))); attr "R" is :::"with_NF_property"::: means :: REWRITE1:def 20 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r3_rewrite1 :::"is_a_normal_form_wrt"::: ) "R") & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) "R")) "holds" (Bool "R" ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "b")) "," (Set (Var "a")))); attr "R" is :::"subcommutative"::: means :: REWRITE1:def 21 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R")) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r7_rewrite1 :::"are_convergent<=1_wrt"::: ) "R")); attr "R" is :::"confluent"::: means :: REWRITE1:def 22 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r6_rewrite1 :::"are_divergent_wrt"::: ) "R")) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) "R")); attr "R" is :::"with_Church-Rosser_property"::: means :: REWRITE1:def 23 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) "R")) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) "R")); attr "R" is :::"locally-confluent"::: means :: REWRITE1:def 24 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R")) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) "R")); end; :: deftheorem defines :::"with_UN_property"::: REWRITE1:def 19 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v4_rewrite1 :::"with_UN_property"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r3_rewrite1 :::"is_a_normal_form_wrt"::: ) (Set (Var "R"))) & (Bool (Set (Var "b")) ($#r3_rewrite1 :::"is_a_normal_form_wrt"::: ) (Set (Var "R"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" )); :: deftheorem defines :::"with_NF_property"::: REWRITE1:def 20 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v5_rewrite1 :::"with_NF_property"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r3_rewrite1 :::"is_a_normal_form_wrt"::: ) (Set (Var "R"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "b")) "," (Set (Var "a")))) ")" )); :: deftheorem defines :::"subcommutative"::: REWRITE1:def 21 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v6_rewrite1 :::"subcommutative"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r7_rewrite1 :::"are_convergent<=1_wrt"::: ) (Set (Var "R")))) ")" )); :: deftheorem defines :::"confluent"::: REWRITE1:def 22 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v7_rewrite1 :::"confluent"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r6_rewrite1 :::"are_divergent_wrt"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "R")))) ")" )); :: deftheorem defines :::"with_Church-Rosser_property"::: REWRITE1:def 23 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v8_rewrite1 :::"with_Church-Rosser_property"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "R")))) ")" )); :: deftheorem defines :::"locally-confluent"::: REWRITE1:def 24 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v9_rewrite1 :::"locally-confluent"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "R")))) ")" )); theorem :: REWRITE1:49 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) "is" ($#v6_rewrite1 :::"subcommutative"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "R"))))) ; theorem :: REWRITE1:50 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v7_rewrite1 :::"confluent"::: ) ) "iff" (Bool (Set (Var "R")) ($#r11_rewrite1 :::"commutes_with"::: ) (Set (Var "R"))) ")" )) ; theorem :: REWRITE1:51 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v7_rewrite1 :::"confluent"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "R")))) ")" )) ; theorem :: REWRITE1:52 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v9_rewrite1 :::"locally-confluent"::: ) ) "iff" (Bool (Set (Var "R")) ($#r10_rewrite1 :::"commutes-weakly_with"::: ) (Set (Var "R"))) ")" )) ; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v8_rewrite1 :::"with_Church-Rosser_property"::: ) -> ($#v7_rewrite1 :::"confluent"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v7_rewrite1 :::"confluent"::: ) -> ($#v8_rewrite1 :::"with_Church-Rosser_property"::: ) ($#v9_rewrite1 :::"locally-confluent"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v6_rewrite1 :::"subcommutative"::: ) -> ($#v7_rewrite1 :::"confluent"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v8_rewrite1 :::"with_Church-Rosser_property"::: ) -> ($#v5_rewrite1 :::"with_NF_property"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v5_rewrite1 :::"with_NF_property"::: ) -> ($#v4_rewrite1 :::"with_UN_property"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_rewrite1 :::"weakly-normalizing"::: ) ($#v4_rewrite1 :::"with_UN_property"::: ) -> ($#v8_rewrite1 :::"with_Church-Rosser_property"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) -> ($#v6_rewrite1 :::"subcommutative"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: REWRITE1:53 (Bool "for" (Set (Var "R")) "being" ($#v4_rewrite1 :::"with_UN_property"::: ) ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r4_rewrite1 :::"is_a_normal_form_of"::: ) (Set (Var "a")) "," (Set (Var "R"))) & (Bool (Set (Var "c")) ($#r4_rewrite1 :::"is_a_normal_form_of"::: ) (Set (Var "a")) "," (Set (Var "R")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))))) ; theorem :: REWRITE1:54 (Bool "for" (Set (Var "R")) "being" ($#v2_rewrite1 :::"weakly-normalizing"::: ) ($#v4_rewrite1 :::"with_UN_property"::: ) ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_rewrite1 :::"nf"::: ) "(" (Set (Var "a")) "," (Set (Var "R")) ")" ) ($#r4_rewrite1 :::"is_a_normal_form_of"::: ) (Set (Var "a")) "," (Set (Var "R"))))) ; theorem :: REWRITE1:55 (Bool "for" (Set (Var "R")) "being" ($#v2_rewrite1 :::"weakly-normalizing"::: ) ($#v4_rewrite1 :::"with_UN_property"::: ) ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R")))) "holds" (Bool (Set ($#k2_rewrite1 :::"nf"::: ) "(" (Set (Var "a")) "," (Set (Var "R")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_rewrite1 :::"nf"::: ) "(" (Set (Var "b")) "," (Set (Var "R")) ")" )))) ; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v3_rewrite1 :::"strongly-normalizing"::: ) ($#v9_rewrite1 :::"locally-confluent"::: ) -> ($#v7_rewrite1 :::"confluent"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"complete"::: means :: REWRITE1:def 25 (Bool "(" (Bool "R" "is" ($#v7_rewrite1 :::"confluent"::: ) ) & (Bool "R" "is" ($#v3_rewrite1 :::"strongly-normalizing"::: ) ) ")" ); end; :: deftheorem defines :::"complete"::: REWRITE1:def 25 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v10_rewrite1 :::"complete"::: ) ) "iff" (Bool "(" (Bool (Set (Var "R")) "is" ($#v7_rewrite1 :::"confluent"::: ) ) & (Bool (Set (Var "R")) "is" ($#v3_rewrite1 :::"strongly-normalizing"::: ) ) ")" ) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v10_rewrite1 :::"complete"::: ) -> ($#v3_rewrite1 :::"strongly-normalizing"::: ) ($#v7_rewrite1 :::"confluent"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v3_rewrite1 :::"strongly-normalizing"::: ) ($#v7_rewrite1 :::"confluent"::: ) -> ($#v10_rewrite1 :::"complete"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v10_rewrite1 :::"complete"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: REWRITE1:56 (Bool "for" (Set (Var "R")) "," (Set (Var "Q")) "being" ($#v8_rewrite1 :::"with_Church-Rosser_property"::: ) ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) ($#r11_rewrite1 :::"commutes_with"::: ) (Set (Var "Q")))) "holds" (Bool (Set (Set (Var "R")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Q"))) "is" ($#v8_rewrite1 :::"with_Church-Rosser_property"::: ) )) ; theorem :: REWRITE1:57 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v7_rewrite1 :::"confluent"::: ) ) "iff" (Bool (Set (Set (Var "R")) ($#k18_finseq_1 :::"[*]"::: ) ) "is" ($#v9_rewrite1 :::"locally-confluent"::: ) ) ")" )) ; theorem :: REWRITE1:58 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v7_rewrite1 :::"confluent"::: ) ) "iff" (Bool (Set (Set (Var "R")) ($#k18_finseq_1 :::"[*]"::: ) ) "is" ($#v6_rewrite1 :::"subcommutative"::: ) ) ")" )) ; begin definitionlet "R", "Q" be ($#m1_hidden :::"Relation":::); pred "R" "," "Q" :::"are_equivalent"::: means :: REWRITE1:def 26 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) "R") "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) "Q") ")" )); symmetry (Bool "for" (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "Q"))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "Q"))) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))) ")" ))) ; end; :: deftheorem defines :::"are_equivalent"::: REWRITE1:def 26 : (Bool "for" (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "," (Set (Var "Q")) ($#r12_rewrite1 :::"are_equivalent"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "Q"))) ")" )) ")" )); definitionlet "R" be ($#m1_hidden :::"Relation":::); let "a", "b" be ($#m1_hidden :::"set"::: ) ; pred "a" "," "b" :::"are_critical_wrt"::: "R" means :: REWRITE1:def 27 (Bool "(" (Bool "a" "," "b" ($#r8_rewrite1 :::"are_divergent<=1_wrt"::: ) "R") & (Bool (Bool "not" "a" "," "b" ($#r5_rewrite1 :::"are_convergent_wrt"::: ) "R")) ")" ); end; :: deftheorem defines :::"are_critical_wrt"::: REWRITE1:def 27 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r13_rewrite1 :::"are_critical_wrt"::: ) (Set (Var "R"))) "iff" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r8_rewrite1 :::"are_divergent<=1_wrt"::: ) (Set (Var "R"))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "R")))) ")" ) ")" ))); theorem :: REWRITE1:59 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r13_rewrite1 :::"are_critical_wrt"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))))) ; theorem :: REWRITE1:60 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r13_rewrite1 :::"are_critical_wrt"::: ) (Set (Var "R")))) ")" )) "holds" (Bool (Set (Var "R")) "is" ($#v9_rewrite1 :::"locally-confluent"::: ) )) ; theorem :: REWRITE1:61 (Bool "for" (Set (Var "R")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "Q")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r13_rewrite1 :::"are_critical_wrt"::: ) (Set (Var "R"))) ")" )) "holds" (Bool (Set (Var "R")) "," (Set (Set (Var "R")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Q"))) ($#r12_rewrite1 :::"are_equivalent"::: ) )) ; theorem :: REWRITE1:62 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "ex" (Set (Var "Q")) "being" ($#v10_rewrite1 :::"complete"::: ) ($#m1_hidden :::"Relation":::) "st" (Bool "(" (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "Q"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R")))) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "Q"))) ")" ) ")" ) ")" ))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); mode :::"Completion"::: "of" "R" -> ($#v10_rewrite1 :::"complete"::: ) ($#m1_hidden :::"Relation":::) means :: REWRITE1:def 28 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) "R") "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) it) ")" )); end; :: deftheorem defines :::"Completion"::: REWRITE1:def 28 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "b2")) "being" ($#v10_rewrite1 :::"complete"::: ) ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_rewrite1 :::"Completion"::: ) "of" (Set (Var "R"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set (Var "b2"))) ")" )) ")" ))); theorem :: REWRITE1:63 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "C")) "being" ($#m2_rewrite1 :::"Completion"::: ) "of" (Set (Var "R")) "holds" (Bool (Set (Var "R")) "," (Set (Var "C")) ($#r12_rewrite1 :::"are_equivalent"::: ) ))) ; theorem :: REWRITE1:64 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "Q")) "being" ($#v10_rewrite1 :::"complete"::: ) ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) "," (Set (Var "Q")) ($#r12_rewrite1 :::"are_equivalent"::: ) )) "holds" (Bool (Set (Var "Q")) "is" ($#m2_rewrite1 :::"Completion"::: ) "of" (Set (Var "R"))))) ; theorem :: REWRITE1:65 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "C")) "being" ($#m2_rewrite1 :::"Completion"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set (Var "R"))) "iff" (Bool (Set ($#k2_rewrite1 :::"nf"::: ) "(" (Set (Var "a")) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_rewrite1 :::"nf"::: ) "(" (Set (Var "b")) "," (Set (Var "C")) ")" )) ")" )))) ;