:: SCMPDS_9 semantic presentation

begin

definition
let la, lb be ( ( Int-like ) ( Int-like ) Int_position) ;
let a, b be ( ( integer ) ( V11() real integer ext-real ) Integer) ;
:: original: -->
redefine func (la,lb) --> (a,b) -> ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like the_Values_of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) ( Relation-like non-empty the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) set ) -compatible ) ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like the_Values_of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) ( Relation-like non-empty the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) set ) -compatible ) PartState of 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;
end;

registration
let k be ( ( integer ) ( V11() real integer ext-real ) Integer) ;
cluster JUMP (goto k : ( ( integer ) ( V11() real integer ext-real ) set ) ) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) -> empty ;
end;

theorem :: SCMPDS_9:1
for i being ( ( ) ( ) Instruction of ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) )
for l being ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) st ( for s being ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like the_Values_of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) ( Relation-like non-empty the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) set ) -compatible V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like the_Values_of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) ( Relation-like non-empty the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) set ) -compatible V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) State of ( ( ) ( ) set ) ) st IC s : ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like the_Values_of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) ( Relation-like non-empty the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) set ) -compatible V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like the_Values_of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) ( Relation-like non-empty the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) set ) -compatible V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) State of ( ( ) ( ) set ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) = l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(Exec (i : ( ( ) ( ) Instruction of ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) ,s : ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like the_Values_of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) ( Relation-like non-empty the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) set ) -compatible V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like the_Values_of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) ( Relation-like non-empty the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) set ) -compatible V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) State of ( ( ) ( ) set ) ) )) : ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like the_Values_of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) ( Relation-like non-empty the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) set ) -compatible V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like the_Values_of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) ( Relation-like non-empty the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) set ) -compatible V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) set ) . (IC ) : ( ( ) ( ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = succ (IC s : ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like the_Values_of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) ( Relation-like non-empty the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) set ) -compatible V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like the_Values_of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Relation-like the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) ( Relation-like non-empty the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) -defined Function-like V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) set ) -compatible V25( the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) State of ( ( ) ( ) set ) ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
NIC (i : ( ( ) ( ) Instruction of ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) ,l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = {(succ l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: SCMPDS_9:2
for i being ( ( ) ( ) Instruction of ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) st ( for l being ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) holds NIC (i : ( ( ) ( ) Instruction of ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) ,l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = {(succ l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ) holds
JUMP i : ( ( ) ( ) Instruction of ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) is empty ;

theorem :: SCMPDS_9:3
for l being ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) )
for k being ( ( integer ) ( V11() real integer ext-real ) Integer) holds NIC ((goto k : ( ( integer ) ( V11() real integer ext-real ) Integer) ) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) ,l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = {(abs (k : ( ( integer ) ( V11() real integer ext-real ) Integer) + l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real integer ext-real ) set ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( non empty V121() V122() V123() V124() V125() V126() ) set ) ;

theorem :: SCMPDS_9:4
for a being ( ( Int-like ) ( Int-like ) Int_position)
for l being ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) holds NIC ((return a : ( ( Int-like ) ( Int-like ) Int_position) ) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) ,l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = { k : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) where k is ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : k : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) > 1 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) } ;

theorem :: SCMPDS_9:5
for a being ( ( Int-like ) ( Int-like ) Int_position)
for l being ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) )
for k1 being ( ( integer ) ( V11() real integer ext-real ) Integer) holds NIC ((saveIC (a : ( ( Int-like ) ( Int-like ) Int_position) ,k1 : ( ( integer ) ( V11() real integer ext-real ) Integer) )) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) ,l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = {(succ l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: SCMPDS_9:6
for a being ( ( Int-like ) ( Int-like ) Int_position)
for l being ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) )
for k1 being ( ( integer ) ( V11() real integer ext-real ) Integer) holds NIC ((a : ( ( Int-like ) ( Int-like ) Int_position) := k1 : ( ( integer ) ( V11() real integer ext-real ) Integer) ) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) ,l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = {(succ l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: SCMPDS_9:7
for a being ( ( Int-like ) ( Int-like ) Int_position)
for l being ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) )
for k1, k2 being ( ( integer ) ( V11() real integer ext-real ) Integer) holds NIC (((a : ( ( Int-like ) ( Int-like ) Int_position) ,k1 : ( ( integer ) ( V11() real integer ext-real ) Integer) ) := k2 : ( ( integer ) ( V11() real integer ext-real ) Integer) ) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) ,l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = {(succ l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: SCMPDS_9:8
for a, b being ( ( Int-like ) ( Int-like ) Int_position)
for l being ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) )
for k1, k2 being ( ( integer ) ( V11() real integer ext-real ) Integer) holds NIC (((a : ( ( Int-like ) ( Int-like ) Int_position) ,k1 : ( ( integer ) ( V11() real integer ext-real ) Integer) ) := (b : ( ( Int-like ) ( Int-like ) Int_position) ,k2 : ( ( integer ) ( V11() real integer ext-real ) Integer) )) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) ,l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = {(succ l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: SCMPDS_9:9
for a being ( ( Int-like ) ( Int-like ) Int_position)
for l being ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) )
for k1, k2 being ( ( integer ) ( V11() real integer ext-real ) Integer) holds NIC ((AddTo (a : ( ( Int-like ) ( Int-like ) Int_position) ,k1 : ( ( integer ) ( V11() real integer ext-real ) Integer) ,k2 : ( ( integer ) ( V11() real integer ext-real ) Integer) )) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) ,l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = {(succ l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: SCMPDS_9:10
for a, b being ( ( Int-like ) ( Int-like ) Int_position)
for l being ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) )
for k1, k2 being ( ( integer ) ( V11() real integer ext-real ) Integer) holds NIC ((AddTo (a : ( ( Int-like ) ( Int-like ) Int_position) ,k1 : ( ( integer ) ( V11() real integer ext-real ) Integer) ,b : ( ( Int-like ) ( Int-like ) Int_position) ,k2 : ( ( integer ) ( V11() real integer ext-real ) Integer) )) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) ,l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = {(succ l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: SCMPDS_9:11
for a, b being ( ( Int-like ) ( Int-like ) Int_position)
for l being ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) )
for k1, k2 being ( ( integer ) ( V11() real integer ext-real ) Integer) holds NIC ((SubFrom (a : ( ( Int-like ) ( Int-like ) Int_position) ,k1 : ( ( integer ) ( V11() real integer ext-real ) Integer) ,b : ( ( Int-like ) ( Int-like ) Int_position) ,k2 : ( ( integer ) ( V11() real integer ext-real ) Integer) )) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) ,l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = {(succ l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: SCMPDS_9:12
for a, b being ( ( Int-like ) ( Int-like ) Int_position)
for l being ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) )
for k1, k2 being ( ( integer ) ( V11() real integer ext-real ) Integer) holds NIC ((MultBy (a : ( ( Int-like ) ( Int-like ) Int_position) ,k1 : ( ( integer ) ( V11() real integer ext-real ) Integer) ,b : ( ( Int-like ) ( Int-like ) Int_position) ,k2 : ( ( integer ) ( V11() real integer ext-real ) Integer) )) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) ,l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = {(succ l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: SCMPDS_9:13
for a, b being ( ( Int-like ) ( Int-like ) Int_position)
for l being ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) )
for k1, k2 being ( ( integer ) ( V11() real integer ext-real ) Integer) holds NIC ((Divide (a : ( ( Int-like ) ( Int-like ) Int_position) ,k1 : ( ( integer ) ( V11() real integer ext-real ) Integer) ,b : ( ( Int-like ) ( Int-like ) Int_position) ,k2 : ( ( integer ) ( V11() real integer ext-real ) Integer) )) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) ,l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = {(succ l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: SCMPDS_9:14
for a being ( ( Int-like ) ( Int-like ) Int_position)
for l being ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) )
for k1, k2 being ( ( integer ) ( V11() real integer ext-real ) Integer) holds NIC (((a : ( ( Int-like ) ( Int-like ) Int_position) ,k1 : ( ( integer ) ( V11() real integer ext-real ) Integer) ) <>0_goto k2 : ( ( integer ) ( V11() real integer ext-real ) Integer) ) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) ,l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = {(succ l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ,(abs (k2 : ( ( integer ) ( V11() real integer ext-real ) Integer) + l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real integer ext-real ) set ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( non empty ) set ) ;

theorem :: SCMPDS_9:15
for a being ( ( Int-like ) ( Int-like ) Int_position)
for l being ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) )
for k1, k2 being ( ( integer ) ( V11() real integer ext-real ) Integer) holds NIC (((a : ( ( Int-like ) ( Int-like ) Int_position) ,k1 : ( ( integer ) ( V11() real integer ext-real ) Integer) ) <=0_goto k2 : ( ( integer ) ( V11() real integer ext-real ) Integer) ) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) ,l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = {(succ l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ,(abs (k2 : ( ( integer ) ( V11() real integer ext-real ) Integer) + l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real integer ext-real ) set ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( non empty ) set ) ;

theorem :: SCMPDS_9:16
for a being ( ( Int-like ) ( Int-like ) Int_position)
for l being ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) )
for k1, k2 being ( ( integer ) ( V11() real integer ext-real ) Integer) holds NIC (((a : ( ( Int-like ) ( Int-like ) Int_position) ,k1 : ( ( integer ) ( V11() real integer ext-real ) Integer) ) >=0_goto k2 : ( ( integer ) ( V11() real integer ext-real ) Integer) ) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) ,l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = {(succ l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ,(abs (k2 : ( ( integer ) ( V11() real integer ext-real ) Integer) + l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real integer ext-real ) set ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( non empty ) set ) ;

theorem :: SCMPDS_9:17
for a being ( ( Int-like ) ( Int-like ) Int_position) holds JUMP (return a : ( ( Int-like ) ( Int-like ) Int_position) ) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = { k : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) where k is ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : k : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) > 1 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) } ;

registration
let a be ( ( Int-like ) ( Int-like ) Int_position) ;
cluster JUMP (return a : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) -> infinite ;
end;

registration
let a be ( ( Int-like ) ( Int-like ) Int_position) ;
let k1 be ( ( integer ) ( V11() real integer ext-real ) Integer) ;
cluster JUMP (saveIC (a : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ,k1 : ( ( integer ) ( V11() real integer ext-real ) set ) )) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) -> empty ;
end;

registration
let a be ( ( Int-like ) ( Int-like ) Int_position) ;
let k1 be ( ( integer ) ( V11() real integer ext-real ) Integer) ;
cluster JUMP (a : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) := k1 : ( ( integer ) ( V11() real integer ext-real ) set ) ) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) -> empty ;
end;

registration
let a be ( ( Int-like ) ( Int-like ) Int_position) ;
let k1, k2 be ( ( integer ) ( V11() real integer ext-real ) Integer) ;
cluster JUMP ((a : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ,k1 : ( ( integer ) ( V11() real integer ext-real ) set ) ) := k2 : ( ( integer ) ( V11() real integer ext-real ) set ) ) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) -> empty ;
end;

registration
let a, b be ( ( Int-like ) ( Int-like ) Int_position) ;
let k1, k2 be ( ( integer ) ( V11() real integer ext-real ) Integer) ;
cluster JUMP ((a : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ,k1 : ( ( integer ) ( V11() real integer ext-real ) set ) ) := (b : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ,k2 : ( ( integer ) ( V11() real integer ext-real ) set ) )) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) -> empty ;
end;

registration
let a be ( ( Int-like ) ( Int-like ) Int_position) ;
let k1, k2 be ( ( integer ) ( V11() real integer ext-real ) Integer) ;
cluster JUMP (AddTo (a : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ,k1 : ( ( integer ) ( V11() real integer ext-real ) set ) ,k2 : ( ( integer ) ( V11() real integer ext-real ) set ) )) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) -> empty ;
end;

registration
let a, b be ( ( Int-like ) ( Int-like ) Int_position) ;
let k1, k2 be ( ( integer ) ( V11() real integer ext-real ) Integer) ;
cluster JUMP (AddTo (a : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ,k1 : ( ( integer ) ( V11() real integer ext-real ) set ) ,b : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ,k2 : ( ( integer ) ( V11() real integer ext-real ) set ) )) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) -> empty ;
cluster JUMP (SubFrom (a : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ,k1 : ( ( integer ) ( V11() real integer ext-real ) set ) ,b : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ,k2 : ( ( integer ) ( V11() real integer ext-real ) set ) )) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) -> empty ;
cluster JUMP (MultBy (a : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ,k1 : ( ( integer ) ( V11() real integer ext-real ) set ) ,b : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ,k2 : ( ( integer ) ( V11() real integer ext-real ) set ) )) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) -> empty ;
cluster JUMP (Divide (a : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ,k1 : ( ( integer ) ( V11() real integer ext-real ) set ) ,b : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ,k2 : ( ( integer ) ( V11() real integer ext-real ) set ) )) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) -> empty ;
end;

registration
let a be ( ( Int-like ) ( Int-like ) Int_position) ;
let k1, k2 be ( ( integer ) ( V11() real integer ext-real ) Integer) ;
cluster JUMP ((a : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ,k1 : ( ( integer ) ( V11() real integer ext-real ) set ) ) <>0_goto k2 : ( ( integer ) ( V11() real integer ext-real ) set ) ) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) -> empty ;
cluster JUMP ((a : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ,k1 : ( ( integer ) ( V11() real integer ext-real ) set ) ) <=0_goto k2 : ( ( integer ) ( V11() real integer ext-real ) set ) ) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) -> empty ;
cluster JUMP ((a : ( ( Int-like ) ( Int-like ) Element of the U1 of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) ) ,k1 : ( ( integer ) ( V11() real integer ext-real ) set ) ) >=0_goto k2 : ( ( integer ) ( V11() real integer ext-real ) set ) ) : ( ( ) ( ) Element of the InstructionsF of SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V72() V73() V74() V76() ) ( V72() V73() V74() V76() ) set ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) -> empty ;
end;

theorem :: SCMPDS_9:18
for l being ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) holds SUCC (l : ( ( ) ( ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ,SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) : ( ( ) ( countable V121() V122() V123() V124() V125() V126() ) Element of K6(NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) = NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ;

registration
cluster SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) -> strict non InsLoc-antisymmetric ;
end;

registration
cluster SCMPDS : ( ( strict ) ( V50() with_non-empty_values IC-Ins-separated strict V91(2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) non InsLoc-antisymmetric ) AMI-Struct over 2 : ( ( ) ( non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() ) Element of NAT : ( ( ) ( non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() ) Element of K6(REAL : ( ( ) ( V121() V122() V123() V127() ) set ) ) : ( ( ) ( ) set ) ) ) ) -> strict non weakly_standard ;
end;