:: CONAFFM  semantic presentation begin  






















definitionlet "X" be   ($#l1_analmetr :::"OrtAfPl":::); attr "X" is  :::"satisfying_DES":::  means :: CONAFFM:def 1 (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 "a")) "," (Set (Var "a1")) "," (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 "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")))); attr "X" is  :::"satisfying_AH":::  means :: CONAFFM:def 2 (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")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "b1"))) & (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "c1"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "c1"))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "a")))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b"))))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b1")) "," (Set (Var "c1")))); attr "X" is  :::"satisfying_3H":::  means :: CONAFFM:def 3 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" "X"  "st" (Bool (Bool (Bool  "not"   ($#r5_analmetr :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))) "holds"  (Bool  "ex" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" "X" "st"  (Bool  "("  (Bool (Set (Var "d")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "d")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a")) "," (Set (Var "c"))) & (Bool (Set (Var "d")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a")) "," (Set (Var "b")))  ")" ))); attr "X" is  :::"satisfying_ODES":::  means :: CONAFFM:def 4 (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")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "b1"))) & (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "c1"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "c1"))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "a")))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b"))))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b1")) "," (Set (Var "c1")))); attr "X" is  :::"satisfying_LIN":::  means :: CONAFFM: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 (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "c1"))) & (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "b1"))) & (Bool (Bool  "not"   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "a")))) & (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b"))) & (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "c1"))) & (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b1")) "," (Set (Var "c1")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "b1")))); attr "X" is  :::"satisfying_LIN1":::  means :: CONAFFM:def 6 (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 (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "c1"))) & (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "b1"))) & (Bool (Bool  "not"   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "a")))) & (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b"))) & (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "c1"))) & (Bool (Set (Var "a")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "b1")))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b1")) "," (Set (Var "c1")))); attr "X" is  :::"satisfying_LIN2":::  means :: CONAFFM:def 7 (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 (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "b1"))) & (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "b1"))) & (Bool (Bool  "not"   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "a")))) & (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b"))) & (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "c1"))) & (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b1")) "," (Set (Var "c1")))) "holds"  (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "c1")))); end; 




























:: deftheorem    defines :::"satisfying_DES"::: CONAFFM:def 1 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v1_conaffm :::"satisfying_DES"::: )  ) "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 "a")) "," (Set (Var "a1")) "," (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 "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"))))  ")" )); 
 
:: deftheorem    defines :::"satisfying_AH"::: CONAFFM:def 2 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v2_conaffm :::"satisfying_AH"::: )  ) "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")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "b1"))) & (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "c1"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "c1"))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "a")))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b"))))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b1")) "," (Set (Var "c1"))))  ")" )); 
 
:: deftheorem    defines :::"satisfying_3H"::: CONAFFM:def 3 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v3_conaffm :::"satisfying_3H"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Bool  "not"   ($#r5_analmetr :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))) "holds"  (Bool  "ex" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set (Var "d")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "d")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a")) "," (Set (Var "c"))) & (Bool (Set (Var "d")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a")) "," (Set (Var "b")))  ")" )))  ")" )); 
 
:: deftheorem    defines :::"satisfying_ODES"::: CONAFFM:def 4 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v4_conaffm :::"satisfying_ODES"::: )  ) "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")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "b1"))) & (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "c1"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "c1"))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "a")))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b"))))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b1")) "," (Set (Var "c1"))))  ")" )); 
 
:: deftheorem    defines :::"satisfying_LIN"::: CONAFFM:def 5 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v5_conaffm :::"satisfying_LIN"::: )  ) "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 (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "c1"))) & (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "b1"))) & (Bool (Bool  "not"   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "a")))) & (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b"))) & (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "c1"))) & (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b1")) "," (Set (Var "c1")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "b1"))))  ")" )); 
 
:: deftheorem    defines :::"satisfying_LIN1"::: CONAFFM:def 6 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v6_conaffm :::"satisfying_LIN1"::: )  ) "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 (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "c1"))) & (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "b1"))) & (Bool (Bool  "not"   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "a")))) & (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b"))) & (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "c1"))) & (Bool (Set (Var "a")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "b1")))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b1")) "," (Set (Var "c1"))))  ")" )); 
 
:: deftheorem    defines :::"satisfying_LIN2"::: CONAFFM:def 7 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v7_conaffm :::"satisfying_LIN2"::: )  ) "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 (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "b1"))) & (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "b1"))) & (Bool (Bool  "not"   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "a")))) & (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b"))) & (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "c1"))) & (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b1")) "," (Set (Var "c1")))) "holds"  (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "c1"))))  ")" )); 
 
theorem :: CONAFFM:1 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v4_conaffm :::"satisfying_ODES"::: )  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v1_conaffm :::"satisfying_DES"::: )  )) ; 
 
theorem :: CONAFFM:2 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v4_conaffm :::"satisfying_ODES"::: )  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v2_conaffm :::"satisfying_AH"::: )  )) ; 
 
theorem :: CONAFFM:3 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v5_conaffm :::"satisfying_LIN"::: )  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v6_conaffm :::"satisfying_LIN1"::: )  )) ; 
 
theorem :: CONAFFM:4 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v6_conaffm :::"satisfying_LIN1"::: )  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v7_conaffm :::"satisfying_LIN2"::: )  )) ; 
 
theorem :: CONAFFM:5 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v5_conaffm :::"satisfying_LIN"::: )  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v4_conaffm :::"satisfying_ODES"::: )  )) ; 
 
theorem :: CONAFFM:6 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v5_conaffm :::"satisfying_LIN"::: )  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v3_conaffm :::"satisfying_3H"::: )  )) ;