:: MEMSTR_0 semantic presentation begin definitionlet "N" be ($#m1_hidden :::"set"::: ) ; attr "c2" is :::"strict"::: ; struct :::"Mem-Struct"::: "over" "N" -> ($#l2_struct_0 :::"ZeroStr"::: ) ; aggr :::"Mem-Struct":::(# :::"carrier":::, :::"ZeroF":::, :::"Object-Kind":::, :::"ValuesF"::: #) -> ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" "N"; sel :::"Object-Kind"::: "c2" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c2") "," "N"; sel :::"ValuesF"::: "c2" -> ($#m1_hidden :::"ManySortedSet":::) "of" "N"; end; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; func :::"Trivial-Mem"::: "N" -> ($#v1_memstr_0 :::"strict"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" "N" means :: MEMSTR_0:def 1 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "the" ($#u1_memstr_0 :::"Object-Kind"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set "the" ($#u2_memstr_0 :::"ValuesF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "N" ($#k8_funcop_1 :::"-->"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) ")" ); end; :: deftheorem defines :::"Trivial-Mem"::: MEMSTR_0:def 1 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v1_memstr_0 :::"strict"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_memstr_0 :::"Trivial-Mem"::: ) (Set (Var "N")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "the" ($#u1_memstr_0 :::"Object-Kind"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set "the" ($#u2_memstr_0 :::"ValuesF"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) ")" ) ")" ))); registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_memstr_0 :::"Trivial-Mem"::: ) "N") -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_memstr_0 :::"strict"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) for ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" "N"; end; notationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); synonym :::"IC"::: "S" for :::"0."::: "N"; synonym :::"Data-Locations"::: "S" for :::"NonZero"::: "N"; end; registration cluster ($#v1_setfam_1 :::"with_zero"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); func :::"the_Values_of"::: "S" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") equals :: MEMSTR_0:def 2 (Set (Set "the" ($#u2_memstr_0 :::"ValuesF"::: ) "of" "S") ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_memstr_0 :::"Object-Kind"::: ) "of" "S")); end; :: deftheorem defines :::"the_Values_of"::: MEMSTR_0:def 2 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) "holds" (Bool (Set ($#k2_memstr_0 :::"the_Values_of"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_memstr_0 :::"ValuesF"::: ) "of" (Set (Var "S"))) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_memstr_0 :::"Object-Kind"::: ) "of" (Set (Var "S"))))))); definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); mode PartState of "S" is (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#v4_relat_1 :::"-defined"::: ) (Set ($#k2_memstr_0 :::"the_Values_of"::: ) "S") ($#v5_funct_1 :::"-compatible"::: ) ($#m1_hidden :::"Function":::); end; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); attr "S" is :::"with_non-empty_values"::: means :: MEMSTR_0:def 3 (Bool (Set ($#k2_memstr_0 :::"the_Values_of"::: ) "S") "is" ($#v2_relat_1 :::"non-empty"::: ) ); end; :: deftheorem defines :::"with_non-empty_values"::: MEMSTR_0:def 3 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_memstr_0 :::"with_non-empty_values"::: ) ) "iff" (Bool (Set ($#k2_memstr_0 :::"the_Values_of"::: ) (Set (Var "S"))) "is" ($#v2_relat_1 :::"non-empty"::: ) ) ")" ))); registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_memstr_0 :::"Trivial-Mem"::: ) "N") -> ($#v1_memstr_0 :::"strict"::: ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v2_memstr_0 :::"with_non-empty_values"::: ) for ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" "N"; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); cluster (Set ($#k2_memstr_0 :::"the_Values_of"::: ) "S") -> ($#v2_relat_1 :::"non-empty"::: ) ; end; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); mode State of "S" is ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"PartState":::) "of" "S"; end; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); mode Object of "S" is ($#m1_subset_1 :::"Element":::) "of" "S"; end; begin definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "o" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "S")); func :::"ObjectKind"::: "o" -> ($#m1_subset_1 :::"Element"::: ) "of" "N" equals :: MEMSTR_0:def 4 (Set (Set "the" ($#u1_memstr_0 :::"Object-Kind"::: ) "of" "S") ($#k3_funct_2 :::"."::: ) "o"); end; :: deftheorem defines :::"ObjectKind"::: MEMSTR_0:def 4 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k3_memstr_0 :::"ObjectKind"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_memstr_0 :::"Object-Kind"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set (Var "o"))))))); definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "o" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "S")); func :::"Values"::: "o" -> ($#m1_hidden :::"set"::: ) equals :: MEMSTR_0:def 5 (Set (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) "S" ")" ) ($#k1_funct_1 :::"."::: ) "o"); end; :: deftheorem defines :::"Values"::: MEMSTR_0:def 5 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set (Var "S")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))))))); definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); attr "IT" is :::"IC-Ins-separated"::: means :: MEMSTR_0:def 6 (Bool (Set ($#k4_memstr_0 :::"Values"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )); end; :: deftheorem defines :::"IC-Ins-separated"::: MEMSTR_0:def 6 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ) "iff" (Bool (Set ($#k4_memstr_0 :::"Values"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ")" ))); registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_memstr_0 :::"Trivial-Mem"::: ) "N") -> ($#v1_memstr_0 :::"strict"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) ($#v8_struct_0 :::"finite"::: ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_memstr_0 :::"strict"::: ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) for ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" "N"; end; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "p" be ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")); func :::"IC"::: "p" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: MEMSTR_0:def 7 (Set "p" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )); end; :: deftheorem defines :::"IC"::: MEMSTR_0:def 7 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )))))); theorem :: MEMSTR_0:1 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s2"))))) "holds" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Var "s2")))))) ; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "o" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "S")); cluster (Set ($#k4_memstr_0 :::"Values"::: ) "o") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "la" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "S")); let "a" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Const "la"))); cluster (Set "la" ($#k16_funcop_1 :::".-->"::: ) "a") -> (Set ($#k2_memstr_0 :::"the_Values_of"::: ) "S") ($#v5_funct_1 :::"-compatible"::: ) ; let "lb" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "S")); let "b" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Const "lb"))); cluster (Set "(" "la" "," "lb" ")" ($#k4_funct_4 :::"-->"::: ) "(" "a" "," "b" ")" ) -> (Set ($#k2_memstr_0 :::"the_Values_of"::: ) "S") ($#v5_funct_1 :::"-compatible"::: ) ; end; theorem :: MEMSTR_0:2 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "s"))))))) ; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "p" be ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")); func :::"DataPart"::: "p" -> ($#m1_hidden :::"PartState":::) "of" "S" equals :: MEMSTR_0:def 8 (Set "p" ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k8_struct_0 :::"Data-Locations"::: ) ")" )); projectivity (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k8_struct_0 :::"Data-Locations"::: ) ")" )))) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k8_struct_0 :::"Data-Locations"::: ) ")" )))) ; end; :: deftheorem defines :::"DataPart"::: MEMSTR_0:def 8 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k8_struct_0 :::"Data-Locations"::: ) ")" )))))); definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "p" be ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")); attr "p" is :::"data-only"::: means :: MEMSTR_0:def 9 (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "p") ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"data-only"::: MEMSTR_0:def 9 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v4_memstr_0 :::"data-only"::: ) ) "iff" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k1_tarski :::"}"::: ) )) ")" )))); registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) (Set ($#k2_memstr_0 :::"the_Values_of"::: ) "S") ($#v5_funct_1 :::"-compatible"::: ) -> ($#v4_memstr_0 :::"data-only"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) (Set ($#k2_memstr_0 :::"the_Values_of"::: ) "S") ($#v5_funct_1 :::"-compatible"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: MEMSTR_0:3 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Bool "not" (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")) ")" ))))))) ; theorem :: MEMSTR_0:4 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k1_tarski :::"}"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")) ")" )))))) ; theorem :: MEMSTR_0:5 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#v4_memstr_0 :::"data-only"::: ) ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "q"))) "iff" (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "q")))) ")" ))))) ; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "p" be ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")); cluster (Set ($#k6_memstr_0 :::"DataPart"::: ) "p") -> ($#v4_memstr_0 :::"data-only"::: ) ; end; theorem :: MEMSTR_0:6 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v4_memstr_0 :::"data-only"::: ) ) "iff" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k8_struct_0 :::"Data-Locations"::: ) )) ")" )))) ; theorem :: MEMSTR_0:7 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#v4_memstr_0 :::"data-only"::: ) ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p")))))) ; theorem :: MEMSTR_0:8 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k8_struct_0 :::"Data-Locations"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "s"))))))) ; theorem :: MEMSTR_0:9 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_struct_0 :::"Data-Locations"::: ) ))))) ; theorem :: MEMSTR_0:10 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "d")) "being" ($#v4_memstr_0 :::"data-only"::: ) ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Bool "not" (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "d")))))))) ; theorem :: MEMSTR_0:11 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "d")) "being" ($#v4_memstr_0 :::"data-only"::: ) ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "d")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p")))))))) ; theorem :: MEMSTR_0:12 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set (Var "p")))))) ; theorem :: MEMSTR_0:13 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k6_domain_1 :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k8_struct_0 :::"Data-Locations"::: ) ")" )))))) ; theorem :: MEMSTR_0:14 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k8_struct_0 :::"Data-Locations"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")) ")" )))))) ; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "l" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "s" be ($#m1_hidden :::"State":::) "of" (Set (Const "S")); cluster (Set "s" ($#k2_funct_7 :::"+*"::: ) "(" (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) "," "l" ")" ) -> (Set ($#k2_memstr_0 :::"the_Values_of"::: ) "S") ($#v5_funct_1 :::"-compatible"::: ) ; end; begin definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "l" be ($#m1_hidden :::"Nat":::); func :::"Start-At"::: "(" "l" "," "S" ")" -> ($#m1_hidden :::"PartState":::) "of" "S" equals :: MEMSTR_0:def 10 (Set (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k16_funcop_1 :::".-->"::: ) "l"); end; :: deftheorem defines :::"Start-At"::: MEMSTR_0:def 10 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "l")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "l"))))))); definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "l" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")); attr "p" is "l" :::"-started"::: means :: MEMSTR_0:def 11 (Bool "(" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p")) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) "p") ($#r1_hidden :::"="::: ) "l") ")" ); end; :: deftheorem defines :::"-started"::: MEMSTR_0:def 11 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" (Set (Var "l")) ($#v5_memstr_0 :::"-started"::: ) ) "iff" (Bool "(" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "l"))) ")" ) ")" ))))); registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "l" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" "l" "," "S" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) "l" ($#v5_memstr_0 :::"-started"::: ) ; end; theorem :: MEMSTR_0:15 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "l")) "," (Set (Var "S")) ")" ")" )))))) ; theorem :: MEMSTR_0:16 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "n")) "," (Set (Var "S")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))))))) ; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "l" be ($#m1_hidden :::"Nat":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) (Set ($#k2_memstr_0 :::"the_Values_of"::: ) "S") ($#v5_funct_1 :::"-compatible"::: ) ($#v1_partfun1 :::"total"::: ) "l" ($#v5_memstr_0 :::"-started"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "l" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")); let "q" be (Set (Const "l")) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")); cluster (Set "p" ($#k1_funct_4 :::"+*"::: ) "q") -> "l" ($#v5_memstr_0 :::"-started"::: ) ; end; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "l" be ($#m1_hidden :::"Nat":::); let "s" be ($#m1_hidden :::"State":::) "of" (Set (Const "S")); redefine attr "s" is "l" :::"-started"::: means :: MEMSTR_0:def 12 (Bool (Set ($#k5_memstr_0 :::"IC"::: ) "s") ($#r1_hidden :::"="::: ) "l"); end; :: deftheorem defines :::"-started"::: MEMSTR_0:def 12 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" (Set (Var "l")) ($#v5_memstr_0 :::"-started"::: ) ) "iff" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "l"))) ")" ))))); theorem :: MEMSTR_0:17 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" (Set (Var "b3")) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool (Set (Var "s")) "is" (Set (Var "l")) ($#v5_memstr_0 :::"-started"::: ) )))))) ; theorem :: MEMSTR_0:18 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: MEMSTR_0:19 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p")) ")" ) "," (Set (Var "S")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")) ")" )))))) ; theorem :: MEMSTR_0:20 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "l")) "," (Set (Var "S")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: MEMSTR_0:21 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "l1")) "," (Set (Var "l2")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set (Var "l1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k")) ")" ) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set (Var "l2")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k")) ")" ) "," (Set (Var "S")) ")" )) "iff" (Bool (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "l1")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "l2")) "," (Set (Var "S")) ")" )) ")" )))) ; theorem :: MEMSTR_0:22 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "l1")) "," (Set (Var "l2")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "l1")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "l2")) "," (Set (Var "S")) ")" ))) "holds" (Bool (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set (Var "l1")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set (Var "l2")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) "," (Set (Var "S")) ")" ))))) ; theorem :: MEMSTR_0:23 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "d")) "being" ($#v4_memstr_0 :::"data-only"::: ) ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Var "d")) ($#r1_partfun1 :::"tolerates"::: ) (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "k")) "," (Set (Var "S")) ")" )))))) ; theorem :: MEMSTR_0:24 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k6_domain_1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")) ")" ) ")" )))))) ; theorem :: MEMSTR_0:25 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k6_domain_1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s")) ")" ) ")" )))))) ; theorem :: MEMSTR_0:26 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p")) ")" ) "," (Set (Var "S")) ")" ")" )))))) ; theorem :: MEMSTR_0:27 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "k")) "," (Set (Var "S")) ")" ")" ) ")" ))))))) ; theorem :: MEMSTR_0:28 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "k")) "," (Set (Var "S")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "k")))))))) ; theorem :: MEMSTR_0:29 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" (Set (Var "l")) ($#v5_memstr_0 :::"-started"::: ) ) "iff" (Bool (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "l")) "," (Set (Var "S")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "p"))) ")" ))))) ; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "k" be ($#m1_hidden :::"Nat":::); let "p" be (Set (Const "k")) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")); let "d" be ($#v4_memstr_0 :::"data-only"::: ) ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")); cluster (Set "p" ($#k1_funct_4 :::"+*"::: ) "d") -> "k" ($#v5_memstr_0 :::"-started"::: ) ; end; theorem :: MEMSTR_0:30 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ) "," (Set (Var "S")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "s")))))) ; theorem :: MEMSTR_0:31 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ) "," (Set (Var "S")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "s")))))) ; theorem :: MEMSTR_0:32 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k6_domain_1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")) ")" ) ")" )))))) ; theorem :: MEMSTR_0:33 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k8_struct_0 :::"Data-Locations"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" )))))) ; theorem :: MEMSTR_0:34 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "s1")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k8_struct_0 :::"Data-Locations"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k8_struct_0 :::"Data-Locations"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" )))) "holds" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Var "s2")))))) ; theorem :: MEMSTR_0:35 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p")) ")" ) "," (Set (Var "S")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")) ")" )))))) ; theorem :: MEMSTR_0:36 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "k")) "," (Set (Var "S")) ")" ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "l")) "," (Set (Var "S")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "l")) "," (Set (Var "S")) ")" ")" ))))))) ; theorem :: MEMSTR_0:37 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p")) ")" ) "," (Set (Var "S")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p")))))) ; theorem :: MEMSTR_0:38 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "k")) "," (Set (Var "S")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "k")))))))) ; theorem :: MEMSTR_0:39 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "S")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "p")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: MEMSTR_0:40 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "k")) "," (Set (Var "S")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "p")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))))))) ; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) (Set ($#k2_memstr_0 :::"the_Values_of"::: ) "S") ($#v5_funct_1 :::"-compatible"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: MEMSTR_0:41 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) ($#r2_subset_1 :::"meets"::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k6_domain_1 :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k8_struct_0 :::"Data-Locations"::: ) ")" )))))) ; begin definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "p" be ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")); func :::"Initialize"::: "p" -> ($#m1_hidden :::"PartState":::) "of" "S" equals :: MEMSTR_0:def 13 (Set "p" ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," "S" ")" ")" )); projectivity (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Const "S")) ")" ")" )))) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Const "S")) ")" ")" )))) ; end; :: deftheorem defines :::"Initialize"::: MEMSTR_0:def 13 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "S")) ")" ")" )))))); registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "p" be ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")); cluster (Set ($#k8_memstr_0 :::"Initialize"::: ) "p") -> (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ; end; theorem :: MEMSTR_0:42 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: MEMSTR_0:43 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "p")) ")" ))) "or" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"IC"::: ) )) ")" ))))) ; theorem :: MEMSTR_0:44 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p")))))) ; theorem :: MEMSTR_0:45 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p"))))))) ; theorem :: MEMSTR_0:46 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "s")))))) ; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "s" be ($#m1_hidden :::"State":::) "of" (Set (Const "S")); cluster (Set ($#k8_memstr_0 :::"Initialize"::: ) "s") -> ($#v1_partfun1 :::"total"::: ) ; end; theorem :: MEMSTR_0:47 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: MEMSTR_0:48 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "p")) ")" )))))) ; theorem :: MEMSTR_0:49 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "q")) ")" ) ")" )))))) ; theorem :: MEMSTR_0:50 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "S")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "q")))))) ; begin definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "p" be ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")); let "k" be ($#m1_hidden :::"Nat":::); func :::"IncIC"::: "(" "p" "," "k" ")" -> ($#m1_hidden :::"PartState":::) "of" "S" equals :: MEMSTR_0:def 14 (Set "p" ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) "p" ")" ) ($#k2_nat_1 :::"+"::: ) "k" ")" ) "," "S" ")" ")" )); end; :: deftheorem defines :::"IncIC"::: MEMSTR_0:def 14 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) "," (Set (Var "S")) ")" ")" ))))))); theorem :: MEMSTR_0:51 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")))))))) ; theorem :: MEMSTR_0:52 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" ))))))) ; theorem :: MEMSTR_0:53 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")))))))) ; theorem :: MEMSTR_0:54 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "d")) "being" ($#v4_memstr_0 :::"data-only"::: ) ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "d")) ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "d"))))))))) ; theorem :: MEMSTR_0:55 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) "," (Set (Var "S")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" )))))) ; theorem :: MEMSTR_0:56 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) "," (Set (Var "S")) ")" ")" ))))))) ; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "s" be ($#m1_hidden :::"State":::) "of" (Set (Const "S")); let "k" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" "s" "," "k" ")" ) -> ($#v1_partfun1 :::"total"::: ) ; end; theorem :: MEMSTR_0:57 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set "(" ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")) ")" ) ")" )))))) ; theorem :: MEMSTR_0:58 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "j")) "," (Set (Var "S")) ")" ")" ) ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k")) ")" ) "," (Set (Var "S")) ")" ")" ))))))) ; theorem :: MEMSTR_0:59 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")))))))) ; theorem :: MEMSTR_0:60 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q"))))) "holds" (Bool (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "q")) ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "q")) "," (Set (Var "k")) ")" ")" ))))))) ; theorem :: MEMSTR_0:61 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "s2")))) "holds" (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "s1")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2")) ")" )))))))) ; theorem :: MEMSTR_0:62 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" )))))) ; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "p" be ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")); let "k" be ($#m1_hidden :::"Nat":::); func :::"DecIC"::: "(" "p" "," "k" ")" -> ($#m1_hidden :::"PartState":::) "of" "S" equals :: MEMSTR_0:def 15 (Set "p" ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) "p" ")" ) ($#k7_nat_d :::"-'"::: ) "k" ")" ) "," "S" ")" ")" )); end; :: deftheorem defines :::"DecIC"::: MEMSTR_0:def 15 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) "," (Set (Var "S")) ")" ")" ))))))); theorem :: MEMSTR_0:63 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")))))))) ; theorem :: MEMSTR_0:64 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" ))))))) ; theorem :: MEMSTR_0:65 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")))))))) ; theorem :: MEMSTR_0:66 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "d")) "being" ($#v4_memstr_0 :::"data-only"::: ) ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "d")) ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "d"))))))))) ; theorem :: MEMSTR_0:67 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) "," (Set (Var "S")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" )))))) ; theorem :: MEMSTR_0:68 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) "," (Set (Var "S")) ")" ")" ))))))) ; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "s" be ($#m1_hidden :::"State":::) "of" (Set (Const "S")); let "k" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k10_memstr_0 :::"DecIC"::: ) "(" "s" "," "k" ")" ) -> ($#v1_partfun1 :::"total"::: ) ; end; theorem :: MEMSTR_0:69 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set "(" ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")) ")" ) ")" )))))) ; theorem :: MEMSTR_0:70 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "j")) "," (Set (Var "S")) ")" ")" ) ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) "," (Set (Var "S")) ")" ")" ))))))) ; theorem :: MEMSTR_0:71 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s"))))) "holds" (Bool (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")))))))) ; theorem :: MEMSTR_0:72 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q"))))) "holds" (Bool (Set ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "q")) ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set (Var "q")) "," (Set (Var "k")) ")" ")" ))))))) ; theorem :: MEMSTR_0:73 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set "(" ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "p"))))))) ; theorem :: MEMSTR_0:74 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q"))))) "holds" (Bool (Set ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "q")) "," (Set (Var "k")) ")" ")" ) ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "q")))))))) ; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "k" be ($#m1_hidden :::"Nat":::); let "p" be (Set (Const "k")) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")); cluster (Set ($#k10_memstr_0 :::"DecIC"::: ) "(" "p" "," "k" ")" ) -> (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ; end; begin registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "l" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" "l" "," "S" ")" ) -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); mode FinPartState of "S" is ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"PartState":::) "of" "S"; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "l" be ($#m1_hidden :::"Nat":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) (Set ($#k2_memstr_0 :::"the_Values_of"::: ) "S") ($#v5_funct_1 :::"-compatible"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v4_card_3 :::"countable"::: ) bbbadV2_PRE_POLY() "l" ($#v5_memstr_0 :::"-started"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "p" be ($#m1_hidden :::"FinPartState":::) "of" (Set (Const "S")); cluster (Set ($#k6_memstr_0 :::"DataPart"::: ) "p") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "p" be ($#m1_hidden :::"FinPartState":::) "of" (Set (Const "S")); cluster (Set ($#k8_memstr_0 :::"Initialize"::: ) "p") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "p" be ($#m1_hidden :::"FinPartState":::) "of" (Set (Const "S")); let "k" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" "p" "," "k" ")" ) -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "p" be ($#m1_hidden :::"FinPartState":::) "of" (Set (Const "S")); let "k" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k10_memstr_0 :::"DecIC"::: ) "(" "p" "," "k" ")" ) -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); func :::"FinPartSt"::: "S" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k8_card_3 :::"sproduct"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) "S" ")" ) ")" ) equals :: MEMSTR_0:def 16 "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k8_card_3 :::"sproduct"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) "S" ")" )) : (Bool (Set (Var "p")) "is" ($#v1_finset_1 :::"finite"::: ) ) "}" ; end; :: deftheorem defines :::"FinPartSt"::: MEMSTR_0:def 16 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) "holds" (Bool (Set ($#k11_memstr_0 :::"FinPartSt"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k8_card_3 :::"sproduct"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set (Var "S")) ")" )) : (Bool (Set (Var "p")) "is" ($#v1_finset_1 :::"finite"::: ) ) "}" ))); theorem :: MEMSTR_0:75 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k11_memstr_0 :::"FinPartSt"::: ) (Set (Var "S"))))))) ; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); cluster (Set ($#k11_memstr_0 :::"FinPartSt"::: ) "S") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: MEMSTR_0:76 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k11_memstr_0 :::"FinPartSt"::: ) (Set (Var "S"))) "holds" (Bool (Set (Var "p")) "is" ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")))))) ; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "IT" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k11_memstr_0 :::"FinPartSt"::: ) (Set (Const "S")) ")" ) "," (Set "(" ($#k11_memstr_0 :::"FinPartSt"::: ) (Set (Const "S")) ")" ); attr "IT" is :::"data-only"::: means :: MEMSTR_0:def 17 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" "S" "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "IT"))) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v4_memstr_0 :::"data-only"::: ) ) & (Bool "(" "for" (Set (Var "q")) "being" ($#m1_hidden :::"PartState":::) "of" "S" "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "q")) "is" ($#v4_memstr_0 :::"data-only"::: ) ) ")" ) ")" )); end; :: deftheorem defines :::"data-only"::: MEMSTR_0:def 17 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k11_memstr_0 :::"FinPartSt"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k11_memstr_0 :::"FinPartSt"::: ) (Set (Var "S")) ")" ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_memstr_0 :::"data-only"::: ) ) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "IT"))))) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v4_memstr_0 :::"data-only"::: ) ) & (Bool "(" "for" (Set (Var "q")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "q")) "is" ($#v4_memstr_0 :::"data-only"::: ) ) ")" ) ")" )) ")" )))); registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k11_memstr_0 :::"FinPartSt"::: ) "S") ($#v4_relat_1 :::"-defined"::: ) (Set ($#k11_memstr_0 :::"FinPartSt"::: ) "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) bbbadV2_FUNCOP_1() ($#v6_memstr_0 :::"data-only"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k11_memstr_0 :::"FinPartSt"::: ) "S" ")" ) "," (Set "(" ($#k11_memstr_0 :::"FinPartSt"::: ) "S" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; begin theorem :: MEMSTR_0:77 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Var "o")))))))) ; theorem :: MEMSTR_0:78 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s2")))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2"))))) "holds" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Var "s2")))))) ; theorem :: MEMSTR_0:79 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "l")) "," (Set (Var "S")) ")" ")" ) ")" ))))))) ; theorem :: MEMSTR_0:80 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2"))))) "holds" (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s2"))))))) ; theorem :: MEMSTR_0:81 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_memstr_0 :::"the_Values_of"::: ) (Set "(" ($#k1_memstr_0 :::"Trivial-Mem"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set ($#k5_numbers :::"NAT"::: ) )))) ; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Const "N")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set (Const "S")) ")" ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ); attr "f" is :::"on_data_only"::: means :: MEMSTR_0:def 18 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" "S" "st" (Bool (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2"))))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "s2"))))); end; :: deftheorem defines :::"on_data_only"::: MEMSTR_0:def 18 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set (Var "S")) ")" ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_memstr_0 :::"on_data_only"::: ) ) "iff" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s2"))))) ")" ))));