:: NAT_LAT semantic presentation begin definitionfunc :::"hcflat"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: NAT_LAT:def 1 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "n"))))); func :::"lcmlat"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: NAT_LAT:def 2 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k5_nat_d :::"lcm"::: ) (Set (Var "n"))))); end; :: deftheorem defines :::"hcflat"::: NAT_LAT:def 1 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_nat_lat :::"hcflat"::: ) )) "iff" (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "n"))))) ")" )); :: deftheorem defines :::"lcmlat"::: NAT_LAT:def 2 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k2_nat_lat :::"lcmlat"::: ) )) "iff" (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k5_nat_d :::"lcm"::: ) (Set (Var "n"))))) ")" )); definitionfunc :::"Nat_Lattice"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ($#l3_lattices :::"LattStr"::: ) equals :: NAT_LAT:def 3 (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k2_nat_lat :::"lcmlat"::: ) ) "," (Set ($#k1_nat_lat :::"hcflat"::: ) ) "#)" ); end; :: deftheorem defines :::"Nat_Lattice"::: NAT_LAT:def 3 : (Bool (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k2_nat_lat :::"lcmlat"::: ) ) "," (Set ($#k1_nat_lat :::"hcflat"::: ) ) "#)" )); registration cluster (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) )) -> ($#v6_membered :::"natural-membered"::: ) ; end; registrationlet "p", "q" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ); identify ; identify ; end; theorem :: NAT_LAT:1 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k1_lattices :::""\/""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k5_nat_d :::"lcm"::: ) (Set (Var "q"))))) ; theorem :: NAT_LAT:2 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k2_lattices :::""/\""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "q"))))) ; theorem :: NAT_LAT:3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_lattices :::"[="::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "a")) ($#r1_nat_d :::"divides"::: ) (Set (Var "b")))) ; definitionfunc :::"0_NN"::: -> ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ) equals :: NAT_LAT:def 4 (Num 1); func :::"1_NN"::: -> ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ) equals :: NAT_LAT:def 5 (Set ($#k6_numbers :::"0"::: ) ); end; :: deftheorem defines :::"0_NN"::: NAT_LAT:def 4 : (Bool (Set ($#k4_nat_lat :::"0_NN"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)); :: deftheorem defines :::"1_NN"::: NAT_LAT:def 5 : (Bool (Set ($#k5_nat_lat :::"1_NN"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); theorem :: NAT_LAT:4 (Bool (Set ($#k4_nat_lat :::"0_NN"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ; registration cluster (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ($#v10_lattices :::"Lattice-like"::: ) ; end; registration cluster (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ; end; registration cluster (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ($#v13_lattices :::"lower-bounded"::: ) ; end; theorem :: NAT_LAT:5 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ) "holds" (Bool (Set (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ))) ; theorem :: NAT_LAT:6 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ) "holds" (Bool (Set (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ))) ; theorem :: NAT_LAT:7 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ) "holds" (Bool (Set (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "r")) ")" ))) ; theorem :: NAT_LAT:8 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "r")) ")" )) & (Bool (Set (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" ) "," (Set (Var "q")) ")" )) & (Bool (Set (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "p")) ")" )) & (Bool (Set (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "q")) ")" )) ")" )) ; theorem :: NAT_LAT:9 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ) "holds" (Bool (Set (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "r")) ")" ))) ; theorem :: NAT_LAT:10 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "r")) ")" )) & (Bool (Set (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" ) "," (Set (Var "q")) ")" )) & (Bool (Set (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "p")) ")" )) & (Bool (Set (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "q")) ")" )) ")" )) ; theorem :: NAT_LAT:11 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set "(" (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set "(" (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" )) ; theorem :: NAT_LAT:12 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set "(" (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set "(" (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set ($#k2_nat_lat :::"lcmlat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k1_nat_lat :::"hcflat"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" )) ; definitionfunc :::"NATPLUS"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: NAT_LAT:def 6 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) ")" )); end; :: deftheorem defines :::"NATPLUS"::: NAT_LAT:def 6 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_nat_lat :::"NATPLUS"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) ")" )) ")" )); registration cluster (Set ($#k6_nat_lat :::"NATPLUS"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "D")); let "N" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "S")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "N" -> ($#m2_subset_1 :::"Element"::: ) "of" "S"; end; registrationlet "D" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster -> ($#v1_xreal_0 :::"real"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "D"; end; registrationlet "D" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster -> ($#v1_xreal_0 :::"real"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "D"; end; definitionmode NatPlus is ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k6_nat_lat :::"NATPLUS"::: ) ); end; definitionlet "k" be ($#m1_hidden :::"Nat":::); assume (Bool (Set (Const "k")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ; func :::"@"::: "k" -> ($#m2_subset_1 :::"NatPlus":::) equals :: NAT_LAT:def 7 "k"; end; :: deftheorem defines :::"@"::: NAT_LAT:def 7 : (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k7_nat_lat :::"@"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "k")))); registration cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v7_ordinal1 :::"natural"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_nat_lat :::"NATPLUS"::: ) ); end; definitionfunc :::"hcflatplus"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k6_nat_lat :::"NATPLUS"::: ) ) means :: NAT_LAT:def 8 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"NatPlus":::) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "n"))))); func :::"lcmlatplus"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k6_nat_lat :::"NATPLUS"::: ) ) means :: NAT_LAT:def 9 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"NatPlus":::) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k5_nat_d :::"lcm"::: ) (Set (Var "n"))))); end; :: deftheorem defines :::"hcflatplus"::: NAT_LAT:def 8 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k6_nat_lat :::"NATPLUS"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k8_nat_lat :::"hcflatplus"::: ) )) "iff" (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"NatPlus":::) "holds" (Bool (Set (Set (Var "b1")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "n"))))) ")" )); :: deftheorem defines :::"lcmlatplus"::: NAT_LAT:def 9 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k6_nat_lat :::"NATPLUS"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k9_nat_lat :::"lcmlatplus"::: ) )) "iff" (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"NatPlus":::) "holds" (Bool (Set (Set (Var "b1")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k5_nat_d :::"lcm"::: ) (Set (Var "n"))))) ")" )); definitionfunc :::"NatPlus_Lattice"::: -> ($#v3_lattices :::"strict"::: ) ($#l3_lattices :::"LattStr"::: ) equals :: NAT_LAT:def 10 (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set ($#k6_nat_lat :::"NATPLUS"::: ) ) "," (Set ($#k9_nat_lat :::"lcmlatplus"::: ) ) "," (Set ($#k8_nat_lat :::"hcflatplus"::: ) ) "#)" ); end; :: deftheorem defines :::"NatPlus_Lattice"::: NAT_LAT:def 10 : (Bool (Set ($#k10_nat_lat :::"NatPlus_Lattice"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set ($#k6_nat_lat :::"NATPLUS"::: ) ) "," (Set ($#k9_nat_lat :::"lcmlatplus"::: ) ) "," (Set ($#k8_nat_lat :::"hcflatplus"::: ) ) "#)" )); registration cluster (Set ($#k10_nat_lat :::"NatPlus_Lattice"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ; end; definitionlet "m" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k10_nat_lat :::"NatPlus_Lattice"::: ) ); func :::"@"::: "m" -> ($#m2_subset_1 :::"NatPlus":::) equals :: NAT_LAT:def 11 "m"; end; :: deftheorem defines :::"@"::: NAT_LAT:def 11 : (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k10_nat_lat :::"NatPlus_Lattice"::: ) ) "holds" (Bool (Set ($#k11_nat_lat :::"@"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Var "m")))); registration cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v7_ordinal1 :::"natural"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k10_nat_lat :::"NatPlus_Lattice"::: ) )); end; registrationlet "p", "q" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k10_nat_lat :::"NatPlus_Lattice"::: ) ); identify ; identify ; end; theorem :: NAT_LAT:13 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k10_nat_lat :::"NatPlus_Lattice"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k1_lattices :::""\/""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_nat_lat :::"@"::: ) (Set (Var "p")) ")" ) ($#k5_nat_d :::"lcm"::: ) (Set "(" ($#k11_nat_lat :::"@"::: ) (Set (Var "q")) ")" )))) ; theorem :: NAT_LAT:14 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k10_nat_lat :::"NatPlus_Lattice"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k2_lattices :::""/\""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_nat_lat :::"@"::: ) (Set (Var "p")) ")" ) ($#k6_nat_d :::"gcd"::: ) (Set "(" ($#k11_nat_lat :::"@"::: ) (Set (Var "q")) ")" )))) ; registration cluster (Set ($#k10_nat_lat :::"NatPlus_Lattice"::: ) ) -> ($#v3_lattices :::"strict"::: ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ; end; definitionlet "L" be ($#l3_lattices :::"Lattice":::); mode :::"SubLattice"::: "of" "L" -> ($#l3_lattices :::"Lattice":::) means :: NAT_LAT:def 12 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) & (Bool (Set "the" ($#u2_lattices :::"L_join"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" "L") ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) & (Bool (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" "L") ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) ")" ); end; :: deftheorem defines :::"SubLattice"::: NAT_LAT:def 12 : (Bool "for" (Set (Var "L")) "," (Set (Var "b2")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_nat_lat :::"SubLattice"::: ) "of" (Set (Var "L"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) & (Bool (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))))) & (Bool (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))))) ")" ) ")" )); registrationlet "L" be ($#l3_lattices :::"Lattice":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v10_lattices :::"Lattice-like"::: ) for ($#m2_nat_lat :::"SubLattice"::: ) "of" "L"; end; theorem :: NAT_LAT:15 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool (Set (Var "L")) "is" ($#m2_nat_lat :::"SubLattice"::: ) "of" (Set (Var "L")))) ; theorem :: NAT_LAT:16 (Bool (Set ($#k10_nat_lat :::"NatPlus_Lattice"::: ) ) "is" ($#m2_nat_lat :::"SubLattice"::: ) "of" (Set ($#k3_nat_lat :::"Nat_Lattice"::: ) )) ;