:: PARSP_1 semantic presentation begin definitionlet "F" be ($#l6_algstr_0 :::"Field":::); func :::"c3add"::: "F" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ($#k3_zfmisc_1 :::":]"::: ) ) means :: PARSP_1:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "x")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "x")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))); end; :: deftheorem defines :::"c3add"::: PARSP_1:def 1 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_parsp_1 :::"c3add"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "x")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "x")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))) ")" ))); definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "F"))) ($#k3_zfmisc_1 :::":]"::: ) ); func "x" :::"+"::: "y" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ($#k3_zfmisc_1 :::":]"::: ) ) equals :: PARSP_1:def 2 (Set (Set "(" ($#k1_parsp_1 :::"c3add"::: ) "F" ")" ) ($#k5_binop_1 :::"."::: ) "(" "x" "," "y" ")" ); end; :: deftheorem defines :::"+"::: PARSP_1:def 2 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "x")) ($#k2_parsp_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_parsp_1 :::"c3add"::: ) (Set (Var "F")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); theorem :: PARSP_1:1 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "x")) ($#k2_parsp_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "x")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "x")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) )))) ; theorem :: PARSP_1:2 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool (Set (Set ($#k4_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k4_domain_1 :::"]"::: ) ) ($#k2_parsp_1 :::"+"::: ) (Set ($#k4_domain_1 :::"["::: ) (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ($#k4_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "f")) ")" ) "," (Set "(" (Set (Var "b")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "c")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "h")) ")" ) ($#k4_domain_1 :::"]"::: ) )))) ; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); func :::"c3compl"::: "F" -> ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ($#k3_zfmisc_1 :::":]"::: ) ) means :: PARSP_1:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))); end; :: deftheorem defines :::"c3compl"::: PARSP_1:def 3 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_parsp_1 :::"c3compl"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) ))) ")" ))); definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "F"))) ($#k3_zfmisc_1 :::":]"::: ) ); func :::"-"::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ($#k3_zfmisc_1 :::":]"::: ) ) equals :: PARSP_1:def 4 (Set (Set "(" ($#k3_parsp_1 :::"c3compl"::: ) "F" ")" ) ($#k3_funct_2 :::"."::: ) "x"); end; :: deftheorem defines :::"-"::: PARSP_1:def 4 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set ($#k4_parsp_1 :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_parsp_1 :::"c3compl"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))))); theorem :: PARSP_1:3 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set ($#k4_parsp_1 :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ($#k4_domain_1 :::"]"::: ) )))) ; definitionlet "S" be ($#m1_hidden :::"set"::: ) ; mode :::"Relation4"::: "of" "S" -> ($#m1_hidden :::"set"::: ) means :: PARSP_1:def 5 (Bool it ($#r1_tarski :::"c="::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) "S" "," "S" "," "S" "," "S" ($#k4_zfmisc_1 :::":]"::: ) )); end; :: deftheorem defines :::"Relation4"::: PARSP_1:def 5 : (Bool "for" (Set (Var "S")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_parsp_1 :::"Relation4"::: ) "of" (Set (Var "S"))) "iff" (Bool (Set (Var "b2")) ($#r1_tarski :::"c="::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "S")) "," (Set (Var "S")) "," (Set (Var "S")) ($#k4_zfmisc_1 :::":]"::: ) )) ")" )); definitionattr "c1" is :::"strict"::: ; struct :::"ParStr"::: -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"ParStr":::(# :::"carrier":::, :::"4_arg_relation"::: #) -> ($#l1_parsp_1 :::"ParStr"::: ) ; sel :::"4_arg_relation"::: "c1" -> ($#m1_parsp_1 :::"Relation4"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_parsp_1 :::"ParStr"::: ) ; end; definitionlet "PS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_parsp_1 :::"ParStr"::: ) ; let "a", "b", "c", "d" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "PS")); pred "a" "," "b" :::"'||'"::: "c" "," "d" means :: PARSP_1:def 6 (Bool (Set ($#k5_domain_1 :::"["::: ) "a" "," "b" "," "c" "," "d" ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_parsp_1 :::"4_arg_relation"::: ) "of" "PS")); end; :: deftheorem defines :::"'||'"::: PARSP_1:def 6 : (Bool "for" (Set (Var "PS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_parsp_1 :::"ParStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_parsp_1 :::"4_arg_relation"::: ) "of" (Set (Var "PS")))) ")" ))); definitionlet "F" be ($#l6_algstr_0 :::"Field":::); func :::"C_3"::: "F" -> ($#m1_hidden :::"set"::: ) equals :: PARSP_1:def 7 (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ($#k3_zfmisc_1 :::":]"::: ) ); end; :: deftheorem defines :::"C_3"::: PARSP_1:def 7 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#k5_parsp_1 :::"C_3"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) ))); registrationlet "F" be ($#l6_algstr_0 :::"Field":::); cluster (Set ($#k5_parsp_1 :::"C_3"::: ) "F") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); func :::"4C_3"::: "F" -> ($#m1_hidden :::"set"::: ) equals :: PARSP_1:def 8 (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "(" ($#k5_parsp_1 :::"C_3"::: ) "F" ")" ) "," (Set "(" ($#k5_parsp_1 :::"C_3"::: ) "F" ")" ) "," (Set "(" ($#k5_parsp_1 :::"C_3"::: ) "F" ")" ) "," (Set "(" ($#k5_parsp_1 :::"C_3"::: ) "F" ")" ) ($#k4_zfmisc_1 :::":]"::: ) ); end; :: deftheorem defines :::"4C_3"::: PARSP_1:def 8 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#k6_parsp_1 :::"4C_3"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "(" ($#k5_parsp_1 :::"C_3"::: ) (Set (Var "F")) ")" ) "," (Set "(" ($#k5_parsp_1 :::"C_3"::: ) (Set (Var "F")) ")" ) "," (Set "(" ($#k5_parsp_1 :::"C_3"::: ) (Set (Var "F")) ")" ) "," (Set "(" ($#k5_parsp_1 :::"C_3"::: ) (Set (Var "F")) ")" ) ($#k4_zfmisc_1 :::":]"::: ) ))); registrationlet "F" be ($#l6_algstr_0 :::"Field":::); cluster (Set ($#k6_parsp_1 :::"4C_3"::: ) "F") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); func :::"PRs"::: "F" -> ($#m1_hidden :::"set"::: ) means :: PARSP_1:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_parsp_1 :::"4C_3"::: ) "F")) & (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k5_domain_1 :::"]"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "c")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "F")) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "c")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "F")) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "c")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "F")) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"PRs"::: PARSP_1:def 9 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_parsp_1 :::"PRs"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_parsp_1 :::"4C_3"::: ) (Set (Var "F")))) & (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k5_domain_1 :::"]"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "c")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "c")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "c")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) ")" )) ")" ) ")" )) ")" ))); theorem :: PARSP_1:4 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#k7_parsp_1 :::"PRs"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set "(" ($#k5_parsp_1 :::"C_3"::: ) (Set (Var "F")) ")" ) "," (Set "(" ($#k5_parsp_1 :::"C_3"::: ) (Set (Var "F")) ")" ) "," (Set "(" ($#k5_parsp_1 :::"C_3"::: ) (Set (Var "F")) ")" ) "," (Set "(" ($#k5_parsp_1 :::"C_3"::: ) (Set (Var "F")) ")" ) ($#k4_zfmisc_1 :::":]"::: ) ))) ; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); func :::"PR"::: "F" -> ($#m1_parsp_1 :::"Relation4"::: ) "of" (Set ($#k5_parsp_1 :::"C_3"::: ) "F") equals :: PARSP_1:def 10 (Set ($#k7_parsp_1 :::"PRs"::: ) "F"); end; :: deftheorem defines :::"PR"::: PARSP_1:def 10 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#k8_parsp_1 :::"PR"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k7_parsp_1 :::"PRs"::: ) (Set (Var "F"))))); definitionlet "F" be ($#l6_algstr_0 :::"Field":::); func :::"MPS"::: "F" -> ($#l1_parsp_1 :::"ParStr"::: ) equals :: PARSP_1:def 11 (Set ($#g1_parsp_1 :::"ParStr"::: ) "(#" (Set "(" ($#k5_parsp_1 :::"C_3"::: ) "F" ")" ) "," (Set "(" ($#k8_parsp_1 :::"PR"::: ) "F" ")" ) "#)" ); end; :: deftheorem defines :::"MPS"::: PARSP_1:def 11 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#k9_parsp_1 :::"MPS"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#g1_parsp_1 :::"ParStr"::: ) "(#" (Set "(" ($#k5_parsp_1 :::"C_3"::: ) (Set (Var "F")) ")" ) "," (Set "(" ($#k8_parsp_1 :::"PR"::: ) (Set (Var "F")) ")" ) "#)" ))); registrationlet "F" be ($#l6_algstr_0 :::"Field":::); cluster (Set ($#k9_parsp_1 :::"MPS"::: ) "F") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_parsp_1 :::"strict"::: ) ; end; theorem :: PARSP_1:5 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_parsp_1 :::"MPS"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_parsp_1 :::"C_3"::: ) (Set (Var "F"))))) ; theorem :: PARSP_1:6 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set "the" ($#u1_parsp_1 :::"4_arg_relation"::: ) "of" (Set "(" ($#k9_parsp_1 :::"MPS"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_parsp_1 :::"PR"::: ) (Set (Var "F"))))) ; theorem :: PARSP_1:7 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_parsp_1 :::"MPS"::: ) (Set (Var "F")) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_parsp_1 :::"PR"::: ) (Set (Var "F")))) ")" ))) ; theorem :: PARSP_1:8 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_parsp_1 :::"MPS"::: ) (Set (Var "F")) ")" ) "holds" (Bool "(" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_parsp_1 :::"PR"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_parsp_1 :::"4C_3"::: ) (Set (Var "F")))) & (Bool "ex" (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool "(" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k5_domain_1 :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_domain_1 :::"["::: ) (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ($#k5_domain_1 :::"]"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "e")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "g")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "e")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "e")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "g")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "e")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "e")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "g")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "e")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) ")" )) ")" ) ")" ))) ; theorem :: PARSP_1:9 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_parsp_1 :::"MPS"::: ) (Set (Var "F")) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool "(" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_parsp_1 :::"4C_3"::: ) (Set (Var "F")))) & (Bool "ex" (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool "(" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k5_domain_1 :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_domain_1 :::"["::: ) (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ($#k5_domain_1 :::"]"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "e")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "g")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "e")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "e")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "g")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "e")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "e")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "g")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "e")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) ")" )) ")" ) ")" ))) ; theorem :: PARSP_1:10 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k9_parsp_1 :::"MPS"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) ))) ; theorem :: PARSP_1:11 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_parsp_1 :::"MPS"::: ) (Set (Var "F")) ")" ) "holds" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k5_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_parsp_1 :::"4C_3"::: ) (Set (Var "F")))))) ; theorem :: PARSP_1:12 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_parsp_1 :::"MPS"::: ) (Set (Var "F")) ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool "ex" (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool "(" (Bool (Set ($#k5_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k5_domain_1 :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_domain_1 :::"["::: ) (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ($#k5_domain_1 :::"]"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "e")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "g")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "e")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "e")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "g")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "e")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "e")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "g")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "g")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "e")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) ")" )) ")" ))) ; theorem :: PARSP_1:13 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_parsp_1 :::"MPS"::: ) (Set (Var "F")) ")" ) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "a"))))) ; theorem :: PARSP_1:14 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_parsp_1 :::"MPS"::: ) (Set (Var "F")) ")" ) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "c"))))) ; theorem :: PARSP_1:15 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_parsp_1 :::"MPS"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "r")) "," (Set (Var "s"))) & (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "r")) "," (Set (Var "s"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: PARSP_1:16 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_parsp_1 :::"MPS"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "c"))))) ; theorem :: PARSP_1:17 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_parsp_1 :::"MPS"::: ) (Set (Var "F")) ")" ) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_parsp_1 :::"MPS"::: ) (Set (Var "F")) ")" ) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "d"))) ")" )))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_parsp_1 :::"ParStr"::: ) ; attr "IT" is :::"ParSp-like"::: means :: PARSP_1:def 12 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "c"))) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "r")) "," (Set (Var "s"))) & (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "r")) "," (Set (Var "s"))))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c")))) "implies" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "c"))) ")" & (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "x"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "x"))) ")" )) ")" )); end; :: deftheorem defines :::"ParSp-like"::: PARSP_1:def 12 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_parsp_1 :::"ParStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_parsp_1 :::"ParSp-like"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "c"))) & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "r")) "," (Set (Var "s"))) & (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "r")) "," (Set (Var "s"))))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c")))) "implies" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "c"))) ")" & (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "x"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "x"))) ")" )) ")" )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_parsp_1 :::"strict"::: ) ($#v2_parsp_1 :::"ParSp-like"::: ) for ($#l1_parsp_1 :::"ParStr"::: ) ; end; definitionmode ParSp is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_parsp_1 :::"ParSp-like"::: ) ($#l1_parsp_1 :::"ParStr"::: ) ; end; theorem :: PARSP_1:18 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "b"))))) ; theorem :: PARSP_1:19 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "b"))))) ; theorem :: PARSP_1:20 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "holds" (Bool (Set (Var "a")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "c"))))) ; theorem :: PARSP_1:21 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: PARSP_1:22 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "d")) "," (Set (Var "c"))))) ; theorem :: PARSP_1:23 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool "(" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "d")) "," (Set (Var "c"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "d")) "," (Set (Var "c"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "d")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "d")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "a"))) ")" ))) ; theorem :: PARSP_1:24 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c")))) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "a"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "a"))) & (Bool (Set (Var "c")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "b"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "c")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "a"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "a"))) & (Bool (Set (Var "c")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c"))) ")" ))) ; theorem :: PARSP_1:25 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) "or" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "d"))) "or" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "d"))) ")" ) "or" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "d"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) ")" )) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: PARSP_1:26 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "r")) "," (Set (Var "s")))) "holds" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "r")) "," (Set (Var "s"))))) ; theorem :: PARSP_1:27 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c"))))) "holds" (Bool "(" (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 :: PARSP_1:28 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) ")" ))) ; theorem :: PARSP_1:29 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c"))))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "c")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "c")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "c")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "c")))) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "c")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "c")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "c")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "b")))) & (Bool (Bool "not" (Set (Var "c")) "," (Set (Var "a")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "c")))) & (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "b")) "," (Set (Var "c")))) & (Bool (Bool "not" (Set (Var "c")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "a")))) & (Bool (Bool "not" (Set (Var "c")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool "not" (Set (Var "b")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c")))) ")" ))) ; theorem :: PARSP_1:30 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d")))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "r")) "," (Set (Var "s"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set (Var "s")))) "holds" (Bool "not" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "r")) "," (Set (Var "s")))))) ; theorem :: PARSP_1:31 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "p")) "," (Set (Var "r"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "q")) "," (Set (Var "r"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q")))) "holds" (Bool "not" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "p")) "," (Set (Var "r")))))) ; theorem :: PARSP_1:32 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "p")) "," (Set (Var "r"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "p")) "," (Set (Var "r")))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "r"))))) ; theorem :: PARSP_1:33 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "p")) "," (Set (Var "r")))) & (Bool (Set (Var "p")) "," (Set (Var "r")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "p")) "," (Set (Var "s"))) & (Bool (Set (Var "q")) "," (Set (Var "r")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "q")) "," (Set (Var "s")))) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Var "s"))))) ; theorem :: PARSP_1:34 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "p")) "," (Set (Var "r"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "p")) "," (Set (Var "s"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "q")) "," (Set (Var "r"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "q")) "," (Set (Var "s")))) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Var "s"))))) ; theorem :: PARSP_1:35 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: PARSP_1:36 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" )) "holds" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "holds" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "r")) "," (Set (Var "s"))))) ; theorem :: PARSP_1:37 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) "st" (Bool (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c"))) ")" ) ")" ))) "holds" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "holds" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "r")) "," (Set (Var "s"))))) ; theorem :: PARSP_1:38 (Bool "for" (Set (Var "PS")) "being" ($#l1_parsp_1 :::"ParSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PS")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) "," (Set (Var "b")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "p")) "," (Set (Var "a"))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "p")) "," (Set (Var "b")))) "holds" (Bool "not" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_parsp_1 :::"'||'"::: ) (Set (Var "p")) "," (Set (Var "c")))))) ;