:: CONMETR semantic presentation begin definitionlet "X" be ($#l1_analmetr :::"OrtAfPl":::); attr "X" is :::"satisfying_OPAP"::: means :: CONMETR:def 1 (Bool "for" (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Bool "not" (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Set (Var "M")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "N"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a3"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b3"))) & (Bool (Set (Var "a3")) "," (Set (Var "b2")) ($#r2_analoaf :::"//"::: ) (Set (Var "a2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a3")) "," (Set (Var "b3")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "b1")))) "holds" (Bool (Set (Var "a1")) "," (Set (Var "b2")) ($#r2_analoaf :::"//"::: ) (Set (Var "a2")) "," (Set (Var "b3"))))); attr "X" is :::"satisfying_PAP"::: means :: CONMETR:def 2 (Bool "for" (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "M")) "is" ($#v4_analmetr :::"being_line"::: ) ) & (Bool (Set (Var "N")) "is" ($#v4_analmetr :::"being_line"::: ) ) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Bool "not" (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a3"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b3"))) & (Bool (Set (Var "a3")) "," (Set (Var "b2")) ($#r2_analoaf :::"//"::: ) (Set (Var "a2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a3")) "," (Set (Var "b3")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "b1")))) "holds" (Bool (Set (Var "a1")) "," (Set (Var "b2")) ($#r2_analoaf :::"//"::: ) (Set (Var "a2")) "," (Set (Var "b3"))))); attr "X" is :::"satisfying_MH1"::: means :: CONMETR:def 3 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "M")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "N"))) & (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "a4")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Bool "not" (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "a4")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Set (Var "a1")) "," (Set (Var "a2")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b1")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a3")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b2")) "," (Set (Var "b3"))) & (Bool (Set (Var "a3")) "," (Set (Var "a4")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b3")) "," (Set (Var "b4")))) "holds" (Bool (Set (Var "a1")) "," (Set (Var "a4")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b1")) "," (Set (Var "b4"))))); attr "X" is :::"satisfying_MH2"::: means :: CONMETR:def 4 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "M")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "N"))) & (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "a4")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Bool "not" (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "a4")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Set (Var "a1")) "," (Set (Var "a2")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b1")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a3")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b2")) "," (Set (Var "b3"))) & (Bool (Set (Var "a3")) "," (Set (Var "a4")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b3")) "," (Set (Var "b4")))) "holds" (Bool (Set (Var "a1")) "," (Set (Var "a4")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b1")) "," (Set (Var "b4"))))); attr "X" is :::"satisfying_TDES"::: means :: CONMETR:def 5 (Bool "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a1")) "," (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "c")) "," (Set (Var "c1")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c1"))) & (Bool (Bool "not" ($#r5_analmetr :::"LIN"::: ) (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "a")))) & (Bool (Bool "not" ($#r5_analmetr :::"LIN"::: ) (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "c")))) & (Bool ($#r5_analmetr :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a1"))) & (Bool ($#r5_analmetr :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b1"))) & (Bool ($#r5_analmetr :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "c1"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "c"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b1")) "," (Set (Var "c1")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "c1")))); attr "X" is :::"satisfying_SCH"::: means :: CONMETR:def 6 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "M")) "is" ($#v4_analmetr :::"being_line"::: ) ) & (Bool (Set (Var "N")) "is" ($#v4_analmetr :::"being_line"::: ) ) & (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "a4")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Bool "not" (Set (Var "a4")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Bool "not" (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Bool "not" (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Bool "not" (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Set (Var "a3")) "," (Set (Var "a2")) ($#r2_analoaf :::"//"::: ) (Set (Var "b3")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a1")) ($#r2_analoaf :::"//"::: ) (Set (Var "b2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a1")) "," (Set (Var "a4")) ($#r2_analoaf :::"//"::: ) (Set (Var "b1")) "," (Set (Var "b4")))) "holds" (Bool (Set (Var "a3")) "," (Set (Var "a4")) ($#r2_analoaf :::"//"::: ) (Set (Var "b3")) "," (Set (Var "b4"))))); attr "X" is :::"satisfying_OSCH"::: means :: CONMETR:def 7 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "M")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "N"))) & (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "a4")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Bool "not" (Set (Var "a4")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Bool "not" (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Bool "not" (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Bool "not" (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Set (Var "a3")) "," (Set (Var "a2")) ($#r2_analoaf :::"//"::: ) (Set (Var "b3")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a1")) ($#r2_analoaf :::"//"::: ) (Set (Var "b2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a1")) "," (Set (Var "a4")) ($#r2_analoaf :::"//"::: ) (Set (Var "b1")) "," (Set (Var "b4")))) "holds" (Bool (Set (Var "a3")) "," (Set (Var "a4")) ($#r2_analoaf :::"//"::: ) (Set (Var "b3")) "," (Set (Var "b4"))))); attr "X" is :::"satisfying_des"::: means :: CONMETR:def 8 (Bool "for" (Set (Var "a")) "," (Set (Var "a1")) "," (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "c")) "," (Set (Var "c1")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool (Bool (Bool "not" ($#r5_analmetr :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "a1")) "," (Set (Var "b")))) & (Bool (Bool "not" ($#r5_analmetr :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "a1")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "a1")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "a1")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c1"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "c1")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b1")) "," (Set (Var "c1")))); end; :: deftheorem defines :::"satisfying_OPAP"::: CONMETR:def 1 : (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_conmetr :::"satisfying_OPAP"::: ) ) "iff" (Bool "for" (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Bool "not" (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Set (Var "M")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "N"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a3"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b3"))) & (Bool (Set (Var "a3")) "," (Set (Var "b2")) ($#r2_analoaf :::"//"::: ) (Set (Var "a2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a3")) "," (Set (Var "b3")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "b1")))) "holds" (Bool (Set (Var "a1")) "," (Set (Var "b2")) ($#r2_analoaf :::"//"::: ) (Set (Var "a2")) "," (Set (Var "b3"))))) ")" )); :: deftheorem defines :::"satisfying_PAP"::: CONMETR:def 2 : (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_conmetr :::"satisfying_PAP"::: ) ) "iff" (Bool "for" (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v4_analmetr :::"being_line"::: ) ) & (Bool (Set (Var "N")) "is" ($#v4_analmetr :::"being_line"::: ) ) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Bool "not" (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a3"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b3"))) & (Bool (Set (Var "a3")) "," (Set (Var "b2")) ($#r2_analoaf :::"//"::: ) (Set (Var "a2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a3")) "," (Set (Var "b3")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "b1")))) "holds" (Bool (Set (Var "a1")) "," (Set (Var "b2")) ($#r2_analoaf :::"//"::: ) (Set (Var "a2")) "," (Set (Var "b3"))))) ")" )); :: deftheorem defines :::"satisfying_MH1"::: CONMETR:def 3 : (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_conmetr :::"satisfying_MH1"::: ) ) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "N"))) & (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "a4")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Bool "not" (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "a4")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Set (Var "a1")) "," (Set (Var "a2")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b1")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a3")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b2")) "," (Set (Var "b3"))) & (Bool (Set (Var "a3")) "," (Set (Var "a4")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b3")) "," (Set (Var "b4")))) "holds" (Bool (Set (Var "a1")) "," (Set (Var "a4")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b1")) "," (Set (Var "b4"))))) ")" )); :: deftheorem defines :::"satisfying_MH2"::: CONMETR:def 4 : (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_conmetr :::"satisfying_MH2"::: ) ) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "N"))) & (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "a4")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Bool "not" (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "a4")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Set (Var "a1")) "," (Set (Var "a2")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b1")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a3")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b2")) "," (Set (Var "b3"))) & (Bool (Set (Var "a3")) "," (Set (Var "a4")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b3")) "," (Set (Var "b4")))) "holds" (Bool (Set (Var "a1")) "," (Set (Var "a4")) ($#r4_analmetr :::"_|_"::: ) (Set (Var "b1")) "," (Set (Var "b4"))))) ")" )); :: deftheorem defines :::"satisfying_TDES"::: CONMETR:def 5 : (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v5_conmetr :::"satisfying_TDES"::: ) ) "iff" (Bool "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a1")) "," (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "c")) "," (Set (Var "c1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c1"))) & (Bool (Bool "not" ($#r5_analmetr :::"LIN"::: ) (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "a")))) & (Bool (Bool "not" ($#r5_analmetr :::"LIN"::: ) (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "c")))) & (Bool ($#r5_analmetr :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a1"))) & (Bool ($#r5_analmetr :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b1"))) & (Bool ($#r5_analmetr :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "c1"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "o")) "," (Set (Var "c"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b1")) "," (Set (Var "c1")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "c1")))) ")" )); :: deftheorem defines :::"satisfying_SCH"::: CONMETR:def 6 : (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v6_conmetr :::"satisfying_SCH"::: ) ) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v4_analmetr :::"being_line"::: ) ) & (Bool (Set (Var "N")) "is" ($#v4_analmetr :::"being_line"::: ) ) & (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "a4")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Bool "not" (Set (Var "a4")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Bool "not" (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Bool "not" (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Bool "not" (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Set (Var "a3")) "," (Set (Var "a2")) ($#r2_analoaf :::"//"::: ) (Set (Var "b3")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a1")) ($#r2_analoaf :::"//"::: ) (Set (Var "b2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a1")) "," (Set (Var "a4")) ($#r2_analoaf :::"//"::: ) (Set (Var "b1")) "," (Set (Var "b4")))) "holds" (Bool (Set (Var "a3")) "," (Set (Var "a4")) ($#r2_analoaf :::"//"::: ) (Set (Var "b3")) "," (Set (Var "b4"))))) ")" )); :: deftheorem defines :::"satisfying_OSCH"::: CONMETR:def 7 : (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v7_conmetr :::"satisfying_OSCH"::: ) ) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "N"))) & (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "a4")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Bool "not" (Set (Var "a4")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) & (Bool (Bool "not" (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Bool "not" (Set (Var "a3")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Bool "not" (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Bool "not" (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) & (Bool (Set (Var "a3")) "," (Set (Var "a2")) ($#r2_analoaf :::"//"::: ) (Set (Var "b3")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a1")) ($#r2_analoaf :::"//"::: ) (Set (Var "b2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a1")) "," (Set (Var "a4")) ($#r2_analoaf :::"//"::: ) (Set (Var "b1")) "," (Set (Var "b4")))) "holds" (Bool (Set (Var "a3")) "," (Set (Var "a4")) ($#r2_analoaf :::"//"::: ) (Set (Var "b3")) "," (Set (Var "b4"))))) ")" )); :: deftheorem defines :::"satisfying_des"::: CONMETR:def 8 : (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v8_conmetr :::"satisfying_des"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "a1")) "," (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "c")) "," (Set (Var "c1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Bool "not" ($#r5_analmetr :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "a1")) "," (Set (Var "b")))) & (Bool (Bool "not" ($#r5_analmetr :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "a1")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "a1")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "a1")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c1"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a1")) "," (Set (Var "c1")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b1")) "," (Set (Var "c1")))) ")" )); theorem :: CONMETR:1 (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool ($#r5_analmetr :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) ")" ))) ; theorem :: CONMETR:2 (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool ($#r5_analmetr :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) ")" )))) ; theorem :: CONMETR:3 (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_analmetr :::"being_line"::: ) )) "holds" (Bool "ex" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "A")) ($#r10_analmetr :::"_|_"::: ) (Set (Var "K"))) ")" ))))) ; theorem :: CONMETR:4 (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_analmetr :::"being_line"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool ($#r5_analmetr :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))))) ; theorem :: CONMETR:5 (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "," (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_analmetr :::"being_line"::: ) ) & (Bool (Set (Var "M")) "is" ($#v4_analmetr :::"being_line"::: ) ) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "M")))))) ; theorem :: CONMETR:6 (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_analmetr :::"Af"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "c9")) "," (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_analmetr :::"Af"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "c9"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "d9"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Var "M9"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "c9")) "," (Set (Var "d9")) ($#r2_aff_1 :::"//"::: ) (Set (Var "M9")))) "holds" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "a")) "," (Set (Var "b")))))))) ; theorem :: CONMETR:7 (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v5_conmetr :::"satisfying_TDES"::: ) )) "holds" (Bool (Set ($#k3_analmetr :::"Af"::: ) (Set (Var "X"))) "is" ($#v7_aff_2 :::"Moufangian"::: ) )) ; theorem :: CONMETR:8 (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) "st" (Bool (Bool (Set ($#k3_analmetr :::"Af"::: ) (Set (Var "X"))) "is" ($#v11_aff_2 :::"translational"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v8_conmetr :::"satisfying_des"::: ) )) ; theorem :: CONMETR:9 (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_conmetr :::"satisfying_MH1"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v7_conmetr :::"satisfying_OSCH"::: ) )) ; theorem :: CONMETR:10 (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v4_conmetr :::"satisfying_MH2"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v7_conmetr :::"satisfying_OSCH"::: ) )) ; theorem :: CONMETR:11 (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v2_conaffm :::"satisfying_AH"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v5_conmetr :::"satisfying_TDES"::: ) )) ; theorem :: CONMETR:12 (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v7_conmetr :::"satisfying_OSCH"::: ) ) & (Bool (Set (Var "X")) "is" ($#v5_conmetr :::"satisfying_TDES"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v6_conmetr :::"satisfying_SCH"::: ) )) ; theorem :: CONMETR:13 (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_conmetr :::"satisfying_OPAP"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_conaffm :::"satisfying_DES"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v2_conmetr :::"satisfying_PAP"::: ) )) ; theorem :: CONMETR:14 (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_conmetr :::"satisfying_MH1"::: ) ) & (Bool (Set (Var "X")) "is" ($#v4_conmetr :::"satisfying_MH2"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v1_conmetr :::"satisfying_OPAP"::: ) )) ; theorem :: CONMETR:15 (Bool "for" (Set (Var "X")) "being" ($#l1_analmetr :::"OrtAfPl":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_conaffm :::"satisfying_3H"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v1_conmetr :::"satisfying_OPAP"::: ) )) ;