:: AMISTD_3  semantic presentation 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"::: )     ($#v3_amistd_1 :::"standard"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Const "N")); let "M" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ); func  :::"LocSeq":::  "(" "M" "," "S" ")"  ->   ($#m1_hidden :::"T-Sequence":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: AMISTD_3:def 1 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  "M")) & (Bool  "("   "for" (Set (Var "m")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  "M"))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_wellord1 :::"canonical_isomorphism_of"::: )   "(" (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set  "("  ($#k2_wellord2 :::"order_type_of"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  "M" ")" ) ")" ) ")" ) "," (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  "M" ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "m"))))  ")" )  ")" ); end; 







:: deftheorem    defines :::"LocSeq"::: AMISTD_3:def 1 :  (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"::: )     ($#v3_amistd_1 :::"standard"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Var "N"))  (Bool  "for" (Set (Var "M")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) )  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_hidden :::"T-Sequence":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_amistd_3 :::"LocSeq"::: )   "(" (Set (Var "M")) "," (Set (Var "S")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "M")))) & (Bool  "("   "for" (Set (Var "m")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "M"))))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_wellord1 :::"canonical_isomorphism_of"::: )   "(" (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set  "("  ($#k2_wellord2 :::"order_type_of"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "M")) ")" ) ")" ) ")" ) "," (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "M")) ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "m"))))  ")" )  ")" )  ")" ))))); 
 
theorem :: AMISTD_3:1 (Bool  "for" (Set (Var "n")) "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"::: )     ($#v3_amistd_1 :::"standard"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Var "N"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) )  "st" (Bool (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "n")) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool (Set   ($#k1_amistd_3 :::"LocSeq"::: )   "(" (Set (Var "F")) "," (Set (Var "S")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k16_funcop_1 :::".-->"::: )  (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"::: )     ($#v3_amistd_1 :::"standard"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Const "N")); let "M" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ); 
cluster (Set   ($#k1_amistd_3 :::"LocSeq"::: )   "(" "M" "," "S" ")" ) ->   ($#v2_funct_1 :::"one-to-one"::: )   ; 
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"::: )     ($#v3_amistd_1 :::"standard"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Const "N")); let "M" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"preProgram":::) "of" (Set (Const "S")); func  :::"ExecTree"::: "M" ->   ($#m1_hidden :::"DecoratedTree":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: AMISTD_3:def 2 (Bool  "("  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k64_valued_1 :::"FirstLoc"::: )  "M")) & (Bool  "("   "for" (Set (Var "t")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  it) "holds"   (Bool  "("  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set (Var "t"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "k")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) where k "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "(" "M"  ($#k7_partfun1 :::"/."::: )  (Set  "(" it  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) ")" ) "," (Set  "(" it  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) ")"  ")" )))  "}"  ) & (Bool  "("   "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "(" "M"  ($#k7_partfun1 :::"/."::: )  (Set  "(" it  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) ")" ) "," (Set  "(" it  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) ")"  ")" )))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "t"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "m")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_amistd_3 :::"LocSeq"::: )   "(" (Set  "("  ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "(" "M"  ($#k7_partfun1 :::"/."::: )  (Set  "(" it  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) ")" ) "," (Set  "(" it  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) ")"  ")" ) "," "S" ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "m"))))  ")" )  ")" )  ")" )  ")" ); end; 







:: deftheorem    defines :::"ExecTree"::: AMISTD_3:def 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"::: )     ($#v3_memstr_0 :::"IC-Ins-separated"::: )     ($#v3_amistd_1 :::"standard"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Var "N"))  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_amistd_3 :::"ExecTree"::: )  (Set (Var "M")))) "iff" (Bool  "("  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k64_valued_1 :::"FirstLoc"::: )  (Set (Var "M")))) & (Bool  "("   "for" (Set (Var "t")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b4"))) "holds"   (Bool  "("  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set (Var "t"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "k")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) where k "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "(" (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "b4"))  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) ")" ) "," (Set  "(" (Set (Var "b4"))  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) ")"  ")" )))  "}"  ) & (Bool  "("   "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "(" (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "b4"))  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) ")" ) "," (Set  "(" (Set (Var "b4"))  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) ")"  ")" )))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "t"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "m")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_amistd_3 :::"LocSeq"::: )   "(" (Set  "("  ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "(" (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "b4"))  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) ")" ) "," (Set  "(" (Set (Var "b4"))  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) ")"  ")" ) "," (Set (Var "S")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "m"))))  ")" )  ")" )  ")" )  ")" )  ")" ))))); 
 
theorem :: AMISTD_3: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"::: )     ($#v3_memstr_0 :::"IC-Ins-separated"::: )     ($#v3_extpro_1 :::"halting"::: )     ($#v3_amistd_1 :::"standard"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Var "N")) "holds"  (Bool (Set   ($#k2_amistd_3 :::"ExecTree"::: )  (Set  "("  ($#k4_compos_1 :::"Stop"::: )  (Set (Var "S")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k8_trees_1 :::"TrivialInfiniteTree"::: ) )  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k6_numbers :::"0"::: ) ))))) ;