begin
definition
func SCM -> ( (
strict ) (
strict )
AMI-Struct over 2 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V86()
integer with_zero complex ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V24()
V84()
V85()
with_zero )
Element of
K32(
REAL : ( ( ) ( non
empty with_zero )
set ) ) : ( ( ) ( )
set ) ) ) )
equals
AMI-Struct(#
SCM-Memory : ( ( ) ( non
empty )
set ) ,
(In (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ,SCM-Memory : ( ( ) ( non empty ) set ) )) : ( ( ) ( )
Element of
SCM-Memory : ( ( ) ( non
empty )
set ) ) ,
SCM-Instr : ( ( non
empty ) ( non
empty Relation-like standard-ins V98()
V99()
V101() )
set ) ,
SCM-OK : ( (
Function-like V36(
SCM-Memory : ( ( ) ( non
empty )
set ) ,2 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V86()
integer with_zero complex ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V24()
V84()
V85()
with_zero )
Element of
K32(
REAL : ( ( ) ( non
empty with_zero )
set ) ) : ( ( ) ( )
set ) ) ) ) ) (
Relation-like Function-like V36(
SCM-Memory : ( ( ) ( non
empty )
set ) ,2 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V86()
integer with_zero complex ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V24()
V84()
V85()
with_zero )
Element of
K32(
REAL : ( ( ) ( non
empty with_zero )
set ) ) : ( ( ) ( )
set ) ) ) ) )
Element of
K32(
K33(
SCM-Memory : ( ( ) ( non
empty )
set ) ,2 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V86()
integer with_zero complex ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V24()
V84()
V85()
with_zero )
Element of
K32(
REAL : ( ( ) ( non
empty with_zero )
set ) ) : ( ( ) ( )
set ) ) ) ) : ( ( ) (
Relation-like )
set ) ) : ( ( ) ( )
set ) ) ,
SCM-VAL : ( (
Relation-like 2 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V86()
integer with_zero complex ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V24()
V84()
V85()
with_zero )
Element of
K32(
REAL : ( ( ) ( non
empty with_zero )
set ) ) : ( ( ) ( )
set ) ) )
-defined Function-like V35(2 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V86()
integer with_zero complex ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V24()
V84()
V85()
with_zero )
Element of
K32(
REAL : ( ( ) ( non
empty with_zero )
set ) ) : ( ( ) ( )
set ) ) ) ) ) (
Relation-like 2 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V86()
integer with_zero complex ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V24()
V84()
V85()
with_zero )
Element of
K32(
REAL : ( ( ) ( non
empty with_zero )
set ) ) : ( ( ) ( )
set ) ) )
-defined Function-like V35(2 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V86()
integer with_zero complex ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V24()
V84()
V85()
with_zero )
Element of
K32(
REAL : ( ( ) ( non
empty with_zero )
set ) ) : ( ( ) ( )
set ) ) ) ) )
set ) ,
SCM-Exec : ( (
Function-like V36(
SCM-Instr : ( ( non
empty ) ( non
empty Relation-like standard-ins V98()
V99()
V101() )
set ) ,
K145(
K233(
(SCM-OK : ( ( Function-like V36( SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( Relation-like Function-like V36( SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32(K33(SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * SCM-VAL : ( ( Relation-like 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) -defined Function-like V35(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( Relation-like 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) -defined Function-like V35(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) set ) ) : ( (
Relation-like ) (
Relation-like non-empty Function-like )
set ) ) : ( ( ) ( non
empty functional V82()
V83() )
set ) ,
K233(
(SCM-OK : ( ( Function-like V36( SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( Relation-like Function-like V36( SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32(K33(SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * SCM-VAL : ( ( Relation-like 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) -defined Function-like V35(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( Relation-like 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) -defined Function-like V35(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) set ) ) : ( (
Relation-like ) (
Relation-like non-empty Function-like )
set ) ) : ( ( ) ( non
empty functional V82()
V83() )
set ) ) : ( ( ) ( )
set ) ) ) (
Relation-like Function-like V36(
SCM-Instr : ( ( non
empty ) ( non
empty Relation-like standard-ins V98()
V99()
V101() )
set ) ,
K145(
K233(
(SCM-OK : ( ( Function-like V36( SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( Relation-like Function-like V36( SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32(K33(SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * SCM-VAL : ( ( Relation-like 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) -defined Function-like V35(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( Relation-like 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) -defined Function-like V35(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) set ) ) : ( (
Relation-like ) (
Relation-like non-empty Function-like )
set ) ) : ( ( ) ( non
empty functional V82()
V83() )
set ) ,
K233(
(SCM-OK : ( ( Function-like V36( SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( Relation-like Function-like V36( SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32(K33(SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * SCM-VAL : ( ( Relation-like 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) -defined Function-like V35(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( Relation-like 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) -defined Function-like V35(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) set ) ) : ( (
Relation-like ) (
Relation-like non-empty Function-like )
set ) ) : ( ( ) ( non
empty functional V82()
V83() )
set ) ) : ( ( ) ( )
set ) ) )
Element of
K32(
K33(
SCM-Instr : ( ( non
empty ) ( non
empty Relation-like standard-ins V98()
V99()
V101() )
set ) ,
K145(
K233(
(SCM-OK : ( ( Function-like V36( SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( Relation-like Function-like V36( SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32(K33(SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * SCM-VAL : ( ( Relation-like 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) -defined Function-like V35(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( Relation-like 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) -defined Function-like V35(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) set ) ) : ( (
Relation-like ) (
Relation-like non-empty Function-like )
set ) ) : ( ( ) ( non
empty functional V82()
V83() )
set ) ,
K233(
(SCM-OK : ( ( Function-like V36( SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( Relation-like Function-like V36( SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32(K33(SCM-Memory : ( ( ) ( non empty ) set ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) * SCM-VAL : ( ( Relation-like 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) -defined Function-like V35(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ( Relation-like 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) -defined Function-like V35(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ) ) set ) ) : ( (
Relation-like ) (
Relation-like non-empty Function-like )
set ) ) : ( ( ) ( non
empty functional V82()
V83() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
Relation-like )
set ) ) : ( ( ) ( )
set ) ) #) : ( (
strict ) (
strict )
AMI-Struct over 2 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V86()
integer with_zero complex ext-real positive non
negative )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V24()
V84()
V85()
with_zero )
Element of
K32(
REAL : ( ( ) ( non
empty with_zero )
set ) ) : ( ( ) ( )
set ) ) ) ) ;
end;
begin
begin
begin
theorem
for
I being ( ( ) ( )
set ) holds
(
I : ( ( ) ( )
set ) is ( ( ) ( )
Instruction of ( (
standard-ins V98()
V99()
V101() ) ( non
empty Relation-like standard-ins V98()
V99()
V101() )
set ) ) iff (
I : ( ( ) ( )
set )
= [0 : ( ( ) ( empty Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() FinSequence-like FinSubsequence-like FinSequence-membered V81() V84() V86() integer Function-yielding V120() complex ext-real non positive non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) ) ,{} : ( ( ) ( empty Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() FinSequence-like FinSubsequence-like FinSequence-membered V81() V84() V86() integer Function-yielding V120() complex ext-real non positive non negative ) set ) ,{} : ( ( ) ( empty Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero ) Element of K32(REAL : ( ( ) ( non empty with_zero ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() FinSequence-like FinSubsequence-like FinSequence-membered V81() V84() V86() integer Function-yielding V120() complex ext-real non positive non negative ) set ) ] : ( ( ) (
V1()
V2() )
set ) or ex
a,
b being ( (
Int-like ) (
Int-like )
Data-Location) st
I : ( ( ) ( )
set )
= a : ( (
Int-like ) (
Int-like )
Data-Location)
:= b : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V86()
integer complex ext-real )
Nat) : ( ( ) ( )
Instruction of ( (
standard-ins V98()
V99()
V101() ) ( non
empty Relation-like standard-ins V98()
V99()
V101() )
set ) ) or ex
a,
b being ( (
Int-like ) (
Int-like )
Data-Location) st
I : ( ( ) ( )
set )
= AddTo (
a : ( (
Int-like ) (
Int-like )
Data-Location) ,
b : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V86()
integer complex ext-real )
Nat) ) : ( ( ) ( )
Instruction of ( (
standard-ins V98()
V99()
V101() ) ( non
empty Relation-like standard-ins V98()
V99()
V101() )
set ) ) or ex
a,
b being ( (
Int-like ) (
Int-like )
Data-Location) st
I : ( ( ) ( )
set )
= SubFrom (
a : ( (
Int-like ) (
Int-like )
Data-Location) ,
b : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V86()
integer complex ext-real )
Nat) ) : ( ( ) ( )
Instruction of ( (
standard-ins V98()
V99()
V101() ) ( non
empty Relation-like standard-ins V98()
V99()
V101() )
set ) ) or ex
a,
b being ( (
Int-like ) (
Int-like )
Data-Location) st
I : ( ( ) ( )
set )
= MultBy (
a : ( (
Int-like ) (
Int-like )
Data-Location) ,
b : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V86()
integer complex ext-real )
Nat) ) : ( ( ) ( )
Instruction of ( (
standard-ins V98()
V99()
V101() ) ( non
empty Relation-like standard-ins V98()
V99()
V101() )
set ) ) or ex
a,
b being ( (
Int-like ) (
Int-like )
Data-Location) st
I : ( ( ) ( )
set )
= Divide (
a : ( (
Int-like ) (
Int-like )
Data-Location) ,
b : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V86()
integer complex ext-real )
Nat) ) : ( ( ) ( )
Instruction of ( (
standard-ins V98()
V99()
V101() ) ( non
empty Relation-like standard-ins V98()
V99()
V101() )
set ) ) or ex
loc being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V86()
integer complex ext-real )
Nat) st
I : ( ( ) ( )
set )
= SCM-goto loc : ( (
Int-like ) (
Int-like )
Data-Location) : ( ( ) ( )
Instruction of ( (
standard-ins V98()
V99()
V101() ) ( non
empty Relation-like standard-ins V98()
V99()
V101() )
set ) ) or ex
a being ( (
Int-like ) (
Int-like )
Data-Location) ex
loc being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V86()
integer complex ext-real )
Nat) st
I : ( ( ) ( )
set )
= a : ( (
Int-like ) (
Int-like )
Data-Location)
=0_goto loc : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V86()
integer complex ext-real )
Nat) : ( ( ) ( )
Instruction of ( (
standard-ins V98()
V99()
V101() ) ( non
empty Relation-like standard-ins V98()
V99()
V101() )
set ) ) or ex
a being ( (
Int-like ) (
Int-like )
Data-Location) ex
loc being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V86()
integer complex ext-real )
Nat) st
I : ( ( ) ( )
set )
= a : ( (
Int-like ) (
Int-like )
Data-Location)
>0_goto loc : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V86()
integer complex ext-real )
Nat) : ( ( ) ( )
Instruction of ( (
standard-ins V98()
V99()
V101() ) ( non
empty Relation-like standard-ins V98()
V99()
V101() )
set ) ) ) ) ;