:: AMISTD_1 semantic presentation

theorem Th1: :: AMISTD_1:1
for b1 being real number holds max {b1} = b1
proof end;

theorem Th2: :: AMISTD_1:2
for b1 being Nat holds max {b1} = b1 by Th1;

registration
cluster non trivial set ;
existence
not for b1 being FinSequence holds b1 is trivial
proof end;
end;

theorem Th3: :: AMISTD_1:3
for b1 being non empty set
for b2 being trivial FinSequence of b1 holds
( b2 is empty or ex b3 being Element of b1 st b2 = <*b3*> )
proof end;

registration
cluster -> with_non-empty_elements set ;
coherence
for b1 being Relation holds b1 is with_non-empty_elements
proof end;
end;

registration
let c1 be finite set ;
let c2 be set ;
cluster K339(a1,a2) -> finite ;
coherence
c1 --> c2 is finite
proof end;
end;

registration
let c1, c2 be set ;
cluster a1 .--> a2 -> trivial with_non-empty_elements ;
coherence
c1 .--> c2 is trivial
proof end;
end;

registration
let c1 be non empty FinSequence;
let c2 be FinSequence;
cluster a1 ^' a2 -> non empty with_non-empty_elements ;
coherence
not c1 ^' c2 is empty
proof end;
end;

theorem Th4: :: AMISTD_1:4
canceled;

theorem Th5: :: AMISTD_1:5
for b1 being non empty set
for b2 being non empty FinSequence of b1
for b3 being FinSequence of b1 holds (b2 ^' b3) /. 1 = b2 /. 1
proof end;

theorem Th6: :: AMISTD_1:6
for b1 being non empty set
for b2 being FinSequence of b1
for b3 being non trivial FinSequence of b1 holds (b2 ^' b3) /. (len (b2 ^' b3)) = b3 /. (len b3)
proof end;

theorem Th7: :: AMISTD_1:7
for b1 being FinSequence holds b1 ^' {} = b1
proof end;

theorem Th8: :: AMISTD_1:8
for b1 being set
for b2 being FinSequence holds b2 ^' <*b1*> = b2
proof end;

theorem Th9: :: AMISTD_1:9
for b1 being non empty set
for b2 being Nat
for b3, b4 being FinSequence of b1 st 1 <= b2 & b2 <= len b3 holds
(b3 ^' b4) /. b2 = b3 /. b2
proof end;

theorem Th10: :: AMISTD_1:10
for b1 being non empty set
for b2 being Nat
for b3, b4 being FinSequence of b1 st 1 <= b2 & b2 < len b4 holds
(b3 ^' b4) /. ((len b3) + b2) = b4 /. (b2 + 1)
proof end;

theorem Th11: :: AMISTD_1:11
for b1 being with_non-empty_elements set
for b2 being non empty non void definite AMI-Struct of b1
for b3 being Element of the Instructions of b2
for b4 being State of b2 holds b4 +* (the Instruction-Locations of b2 --> b3) is State of b2
proof end;

registration
let c1 be set ;
let c2 be AMI-Struct of c1;
cluster empty -> with_non-empty_elements programmed FinPartState of a2;
coherence
for b1 being FinPartState of c2 st b1 is empty holds
b1 is programmed
proof end;
end;

registration
let c1 be set ;
let c2 be AMI-Struct of c1;
cluster empty with_non-empty_elements programmed FinPartState of a2;
existence
ex b1 being FinPartState of c2 st b1 is empty
proof end;
end;

registration
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite AMI-Struct of c1;
cluster non empty trivial with_non-empty_elements programmed FinPartState of a2;
existence
ex b1 being FinPartState of c2 st
( not b1 is empty & b1 is trivial & b1 is programmed )
proof end;
end;

registration
let c1 be with_non-empty_elements set ;
let c2 be non void AMI-Struct of c1;
let c3 be Element of the Instructions of c2;
let c4 be State of c2;
cluster (the Execution of a2 . a3) . a4 -> Relation-like Function-like with_non-empty_elements ;
coherence
( (the Execution of c2 . c3) . c4 is Function-like & (the Execution of c2 . c3) . c4 is Relation-like )
proof end;
end;

Lemma10: for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of b1
for b3 being Instruction-Location of b2
for b4 being Element of the Instructions of b2
for b5 being FinPartState of b2 st b5 = b3 .--> b4 holds
b5 is autonomic
proof end;

registration
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of c1;
cluster non empty trivial with_non-empty_elements autonomic programmed FinPartState of a2;
existence
ex b1 being FinPartState of c2 st
( not b1 is empty & b1 is trivial & b1 is autonomic & b1 is programmed )
proof end;
end;

theorem Th12: :: AMISTD_1:12
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of b1
for b3 being Instruction-Location of b2
for b4 being Element of the Instructions of b2 holds b3 .--> b4 is autonomic by Lemma10;

theorem Th13: :: AMISTD_1:13
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of b1 holds b2 is programmable
proof end;

registration
let c1 be with_non-empty_elements set ;
cluster non empty non void IC-Ins-separated steady-programmed definite -> non empty non void IC-Ins-separated definite programmable AMI-Struct of a1;
coherence
for b1 being non empty non void IC-Ins-separated definite AMI-Struct of c1 st b1 is steady-programmed holds
b1 is programmable
by Th13;
end;

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void AMI-Struct of c1;
let c3 be InsType of c2;
canceled;
canceled;
attr a3 is jump-only means :: AMISTD_1:def 3
for b1 being State of a2
for b2 being Object of a2
for b3 being Instruction of a2 st InsCode b3 = a3 & b2 <> IC a2 holds
(Exec b3,b1) . b2 = b1 . b2;
end;

:: deftheorem Def1 AMISTD_1:def 1 :
canceled;

:: deftheorem Def2 AMISTD_1:def 2 :
canceled;

:: deftheorem Def3 defines jump-only AMISTD_1:def 3 :
for b1 being with_non-empty_elements set
for b2 being non empty non void AMI-Struct of b1
for b3 being InsType of b2 holds
( b3 is jump-only iff for b4 being State of b2
for b5 being Object of b2
for b6 being Instruction of b2 st InsCode b6 = b3 & b5 <> IC b2 holds
(Exec b6,b4) . b5 = b4 . b5 );

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void AMI-Struct of c1;
let c3 be Instruction of c2;
attr a3 is jump-only means :: AMISTD_1:def 4
InsCode a3 is jump-only;
end;

:: deftheorem Def4 defines jump-only AMISTD_1:def 4 :
for b1 being with_non-empty_elements set
for b2 being non empty non void AMI-Struct of b1
for b3 being Instruction of b2 holds
( b3 is jump-only iff InsCode b3 is jump-only );

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite AMI-Struct of c1;
let c3 be Instruction-Location of c2;
let c4 be Element of the Instructions of c2;
func NIC c4,c3 -> Subset of the Instruction-Locations of a2 equals :: AMISTD_1:def 5
{ (IC (Following b1)) where B is State of a2 : ( IC b1 = a3 & b1 . a3 = a4 ) } ;
coherence
{ (IC (Following b1)) where B is State of c2 : ( IC b1 = c3 & b1 . c3 = c4 ) } is Subset of the Instruction-Locations of c2
proof end;
end;

:: deftheorem Def5 defines NIC AMISTD_1:def 5 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being Instruction-Location of b2
for b4 being Element of the Instructions of b2 holds NIC b4,b3 = { (IC (Following b5)) where B is State of b2 : ( IC b5 = b3 & b5 . b3 = b4 ) } ;

E12: now
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite realistic AMI-Struct of c1;
let c3 be Element of the Instructions of c2;
let c4 be Instruction-Location of c2;
let c5 be State of c2;
let c6 be FinPartState of c2;
assume E13: c6 = (IC c2),c4 --> c4,c3 ;
set c7 = c5 +* c6;
E14: IC c2 <> c4 by AMI_1:48;
E15: dom c6 = {(IC c2),c4} by E13, FUNCT_4:65;
then E16: IC c2 in dom c6 by TARSKI:def 2;
E17: IC (c5 +* c6) = (c5 +* c6) . (IC c2)
.= c6 . (IC c2) by E16, FUNCT_4:14
.= c4 by E13, E14, FUNCT_4:66 ;
c4 in dom c6 by E15, TARSKI:def 2;
then (c5 +* c6) . c4 = c6 . c4 by FUNCT_4:14
.= c3 by E13, E14, FUNCT_4:66 ;
hence IC (Following (c5 +* c6)) in NIC c3,c4 by E17;
end;

registration
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite realistic AMI-Struct of c1;
let c3 be Element of the Instructions of c2;
let c4 be Instruction-Location of c2;
cluster NIC a3,a4 -> non empty ;
coherence
not NIC c3,c4 is empty
proof end;
end;

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite AMI-Struct of c1;
let c3 be Element of the Instructions of c2;
func JUMP c3 -> Subset of the Instruction-Locations of a2 equals :: AMISTD_1:def 6
meet { (NIC a3,b1) where B is Instruction-Location of a2 : verum } ;
coherence
meet { (NIC c3,b1) where B is Instruction-Location of c2 : verum } is Subset of the Instruction-Locations of c2
proof end;
end;

:: deftheorem Def6 defines JUMP AMISTD_1:def 6 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being Element of the Instructions of b2 holds JUMP b3 = meet { (NIC b3,b4) where B is Instruction-Location of b2 : verum } ;

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite AMI-Struct of c1;
let c3 be Instruction-Location of c2;
func SUCC c3 -> Subset of the Instruction-Locations of a2 equals :: AMISTD_1:def 7
union { ((NIC b1,a3) \ (JUMP b1)) where B is Element of the Instructions of a2 : verum } ;
coherence
union { ((NIC b1,c3) \ (JUMP b1)) where B is Element of the Instructions of c2 : verum } is Subset of the Instruction-Locations of c2
proof end;
end;

:: deftheorem Def7 defines SUCC AMISTD_1:def 7 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being Instruction-Location of b2 holds SUCC b3 = union { ((NIC b4,b3) \ (JUMP b4)) where B is Element of the Instructions of b2 : verum } ;

theorem Th14: :: AMISTD_1:14
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being Element of the Instructions of b2 st not the Instruction-Locations of b2 is trivial & ( for b4 being Instruction-Location of b2 holds NIC b3,b4 = {b4} ) holds
JUMP b3 is empty
proof end;

theorem Th15: :: AMISTD_1:15
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite realistic AMI-Struct of b1
for b3 being Instruction-Location of b2
for b4 being Instruction of b2 st b4 is halting holds
NIC b4,b3 = {b3}
proof end;

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite AMI-Struct of c1;
let c3, c4 be Instruction-Location of c2;
pred c3 <= c4 means :Def8: :: AMISTD_1:def 8
ex b1 being non empty FinSequence of the Instruction-Locations of a2 st
( b1 /. 1 = a3 & b1 /. (len b1) = a4 & ( for b2 being Nat st 1 <= b2 & b2 < len b1 holds
b1 /. (b2 + 1) in SUCC (b1 /. b2) ) );
reflexivity
for b1 being Instruction-Location of c2 ex b2 being non empty FinSequence of the Instruction-Locations of c2 st
( b2 /. 1 = b1 & b2 /. (len b2) = b1 & ( for b3 being Nat st 1 <= b3 & b3 < len b2 holds
b2 /. (b3 + 1) in SUCC (b2 /. b3) ) )
proof end;
end;

:: deftheorem Def8 defines <= AMISTD_1:def 8 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3, b4 being Instruction-Location of b2 holds
( b3 <= b4 iff ex b5 being non empty FinSequence of the Instruction-Locations of b2 st
( b5 /. 1 = b3 & b5 /. (len b5) = b4 & ( for b6 being Nat st 1 <= b6 & b6 < len b5 holds
b5 /. (b6 + 1) in SUCC (b5 /. b6) ) ) );

theorem Th16: :: AMISTD_1:16
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3, b4, b5 being Instruction-Location of b2 st b3 <= b4 & b4 <= b5 holds
b3 <= b5
proof end;

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite AMI-Struct of c1;
attr a2 is InsLoc-antisymmetric means :: AMISTD_1:def 9
for b1, b2 being Instruction-Location of a2 st b1 <= b2 & b2 <= b1 holds
b1 = b2;
end;

:: deftheorem Def9 defines InsLoc-antisymmetric AMISTD_1:def 9 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1 holds
( b2 is InsLoc-antisymmetric iff for b3, b4 being Instruction-Location of b2 st b3 <= b4 & b4 <= b3 holds
b3 = b4 );

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite AMI-Struct of c1;
attr a2 is standard means :Def10: :: AMISTD_1:def 10
ex b1 being Function of NAT ,the Instruction-Locations of a2 st
( b1 is bijective & ( for b2, b3 being Nat holds
( b2 <= b3 iff b1 . b2 <= b1 . b3 ) ) );
end;

:: deftheorem Def10 defines standard AMISTD_1:def 10 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1 holds
( b2 is standard iff ex b3 being Function of NAT ,the Instruction-Locations of b2 st
( b3 is bijective & ( for b4, b5 being Nat holds
( b4 <= b5 iff b3 . b4 <= b3 . b5 ) ) ) );

theorem Th17: :: AMISTD_1:17
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3, b4 being Function of NAT ,the Instruction-Locations of b2 st b3 is bijective & ( for b5, b6 being Nat holds
( b5 <= b6 iff b3 . b5 <= b3 . b6 ) ) & b4 is bijective & ( for b5, b6 being Nat holds
( b5 <= b6 iff b4 . b5 <= b4 . b6 ) ) holds
b3 = b4
proof end;

theorem Th18: :: AMISTD_1:18
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being Function of NAT ,the Instruction-Locations of b2 st b3 is bijective holds
( ( for b4, b5 being Nat holds
( b4 <= b5 iff b3 . b4 <= b3 . b5 ) ) iff for b4 being Nat holds
( b3 . (b4 + 1) in SUCC (b3 . b4) & ( for b5 being Nat st b3 . b5 in SUCC (b3 . b4) holds
b4 <= b5 ) ) )
proof end;

theorem Th19: :: AMISTD_1:19
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1 holds
( b2 is standard iff ex b3 being Function of NAT ,the Instruction-Locations of b2 st
( b3 is bijective & ( for b4 being Nat holds
( b3 . (b4 + 1) in SUCC (b3 . b4) & ( for b5 being Nat st b3 . b5 in SUCC (b3 . b4) holds
b4 <= b5 ) ) ) ) )
proof end;

Lemma20: for b1, b2 being set holds dom ((NAT --> b1) +* (NAT .--> b2)) = NAT \/ {NAT }
proof end;

set c1 = {[1,0],[0,0]};

definition
let c2 be with_non-empty_elements set ;
func STC c1 -> strict AMI-Struct of a1 means :Def11: :: AMISTD_1:def 11
( the carrier of a2 = NAT \/ {NAT } & the Instruction-Counter of a2 = NAT & the Instruction-Locations of a2 = NAT & the Instruction-Codes of a2 = {0,1} & the Instructions of a2 = {[0,0],[1,0]} & the Object-Kind of a2 = (NAT --> {[1,0],[0,0]}) +* (NAT .--> NAT ) & ex b1 being Function of product the Object-Kind of a2, product the Object-Kind of a2 st
( ( for b2 being Element of product the Object-Kind of a2 holds b1 . b2 = b2 +* (NAT .--> (succ (b2 . NAT ))) ) & the Execution of a2 = ([1,0] .--> b1) +* ([0,0] .--> (id (product the Object-Kind of a2))) ) );
existence
ex b1 being strict AMI-Struct of c2 st
( the carrier of b1 = NAT \/ {NAT } & the Instruction-Counter of b1 = NAT & the Instruction-Locations of b1 = NAT & the Instruction-Codes of b1 = {0,1} & the Instructions of b1 = {[0,0],[1,0]} & the Object-Kind of b1 = (NAT --> {[1,0],[0,0]}) +* (NAT .--> NAT ) & ex b2 being Function of product the Object-Kind of b1, product the Object-Kind of b1 st
( ( for b3 being Element of product the Object-Kind of b1 holds b2 . b3 = b3 +* (NAT .--> (succ (b3 . NAT ))) ) & the Execution of b1 = ([1,0] .--> b2) +* ([0,0] .--> (id (product the Object-Kind of b1))) ) )
proof end;
uniqueness
for b1, b2 being strict AMI-Struct of c2 st the carrier of b1 = NAT \/ {NAT } & the Instruction-Counter of b1 = NAT & the Instruction-Locations of b1 = NAT & the Instruction-Codes of b1 = {0,1} & the Instructions of b1 = {[0,0],[1,0]} & the Object-Kind of b1 = (NAT --> {[1,0],[0,0]}) +* (NAT .--> NAT ) & ex b3 being Function of product the Object-Kind of b1, product the Object-Kind of b1 st
( ( for b4 being Element of product the Object-Kind of b1 holds b3 . b4 = b4 +* (NAT .--> (succ (b4 . NAT ))) ) & the Execution of b1 = ([1,0] .--> b3) +* ([0,0] .--> (id (product the Object-Kind of b1))) ) & the carrier of b2 = NAT \/ {NAT } & the Instruction-Counter of b2 = NAT & the Instruction-Locations of b2 = NAT & the Instruction-Codes of b2 = {0,1} & the Instructions of b2 = {[0,0],[1,0]} & the Object-Kind of b2 = (NAT --> {[1,0],[0,0]}) +* (NAT .--> NAT ) & ex b3 being Function of product the Object-Kind of b2, product the Object-Kind of b2 st
( ( for b4 being Element of product the Object-Kind of b2 holds b3 . b4 = b4 +* (NAT .--> (succ (b4 . NAT ))) ) & the Execution of b2 = ([1,0] .--> b3) +* ([0,0] .--> (id (product the Object-Kind of b2))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines STC AMISTD_1:def 11 :
for b1 being with_non-empty_elements set
for b2 being strict AMI-Struct of b1 holds
( b2 = STC b1 iff ( the carrier of b2 = NAT \/ {NAT } & the Instruction-Counter of b2 = NAT & the Instruction-Locations of b2 = NAT & the Instruction-Codes of b2 = {0,1} & the Instructions of b2 = {[0,0],[1,0]} & the Object-Kind of b2 = (NAT --> {[1,0],[0,0]}) +* (NAT .--> NAT ) & ex b3 being Function of product the Object-Kind of b2, product the Object-Kind of b2 st
( ( for b4 being Element of product the Object-Kind of b2 holds b3 . b4 = b4 +* (NAT .--> (succ (b4 . NAT ))) ) & the Execution of b2 = ([1,0] .--> b3) +* ([0,0] .--> (id (product the Object-Kind of b2))) ) ) );

registration
let c2 be with_non-empty_elements set ;
cluster the Instruction-Locations of (STC a1) -> infinite ;
coherence
not the Instruction-Locations of (STC c2) is finite
by Def11, CARD_4:15;
end;

registration
let c2 be with_non-empty_elements set ;
cluster STC a1 -> non empty strict non void ;
coherence
( not STC c2 is empty & not STC c2 is void )
proof end;
end;

registration
let c2 be with_non-empty_elements set ;
cluster STC a1 -> non empty strict non void IC-Ins-separated data-oriented steady-programmed definite realistic programmable ;
coherence
( STC c2 is IC-Ins-separated & STC c2 is definite & STC c2 is realistic & STC c2 is steady-programmed & STC c2 is data-oriented )
proof end;
end;

Lemma22: for b1 being with_non-empty_elements set
for b2 being Instruction of (STC b1)
for b3 being State of (STC b1) st InsCode b2 = 1 holds
(Exec b2,b3) . (IC (STC b1)) = succ (IC b3)
proof end;

theorem Th20: :: AMISTD_1:20
for b1 being with_non-empty_elements set
for b2 being Instruction of (STC b1) st InsCode b2 = 0 holds
b2 is halting
proof end;

theorem Th21: :: AMISTD_1:21
for b1 being with_non-empty_elements set
for b2 being Instruction of (STC b1) st InsCode b2 = 1 holds
not b2 is halting
proof end;

theorem Th22: :: AMISTD_1:22
for b1 being with_non-empty_elements set
for b2 being Element of the Instructions of (STC b1) holds
( InsCode b2 = 1 or InsCode b2 = 0 )
proof end;

theorem Th23: :: AMISTD_1:23
for b1 being with_non-empty_elements set
for b2 being Instruction of (STC b1) holds b2 is jump-only
proof end;

Lemma26: for b1 being natural number
for b2 being with_non-empty_elements set
for b3 being Instruction-Location of (STC b2)
for b4 being Element of the Instructions of (STC b2) st b3 = b1 & InsCode b4 = 1 holds
NIC b4,b3 = {(b1 + 1)}
proof end;

Lemma27: for b1 being with_non-empty_elements set
for b2 being Element of the Instructions of (STC b1) holds JUMP b2 is empty
proof end;

theorem Th24: :: AMISTD_1:24
for b1 being natural number
for b2 being with_non-empty_elements set
for b3 being Instruction-Location of (STC b2) st b3 = b1 holds
SUCC b3 = {b1,(b1 + 1)}
proof end;

registration
let c2 be with_non-empty_elements set ;
cluster STC a1 -> non empty strict non void IC-Ins-separated data-oriented steady-programmed definite realistic programmable standard ;
coherence
STC c2 is standard
proof end;
end;

registration
let c2 be with_non-empty_elements set ;
cluster STC a1 -> non empty strict non void halting IC-Ins-separated data-oriented steady-programmed definite realistic programmable standard ;
coherence
STC c2 is halting
proof end;
end;

registration
let c2 be with_non-empty_elements set ;
cluster non empty non void halting IC-Ins-separated steady-programmed definite realistic programmable standard AMI-Struct of a1;
existence
ex b1 being non empty non void IC-Ins-separated definite AMI-Struct of c2 st
( b1 is standard & b1 is halting & b1 is realistic & b1 is steady-programmed & b1 is programmable )
proof end;
end;

definition
let c2 be with_non-empty_elements set ;
let c3 be non empty non void IC-Ins-separated definite standard AMI-Struct of c2;
let c4 be natural number ;
func il. c2,c3 -> Instruction-Location of a2 means :Def12: :: AMISTD_1:def 12
ex b1 being Function of NAT ,the Instruction-Locations of a2 st
( b1 is bijective & ( for b2, b3 being Nat holds
( b2 <= b3 iff b1 . b2 <= b1 . b3 ) ) & a4 = b1 . a3 );
existence
ex b1 being Instruction-Location of c3ex b2 being Function of NAT ,the Instruction-Locations of c3 st
( b2 is bijective & ( for b3, b4 being Nat holds
( b3 <= b4 iff b2 . b3 <= b2 . b4 ) ) & b1 = b2 . c4 )
proof end;
uniqueness
for b1, b2 being Instruction-Location of c3 st ex b3 being Function of NAT ,the Instruction-Locations of c3 st
( b3 is bijective & ( for b4, b5 being Nat holds
( b4 <= b5 iff b3 . b4 <= b3 . b5 ) ) & b1 = b3 . c4 ) & ex b3 being Function of NAT ,the Instruction-Locations of c3 st
( b3 is bijective & ( for b4, b5 being Nat holds
( b4 <= b5 iff b3 . b4 <= b3 . b5 ) ) & b2 = b3 . c4 ) holds
b1 = b2
by Th17;
end;

:: deftheorem Def12 defines il. AMISTD_1:def 12 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being natural number
for b4 being Instruction-Location of b2 holds
( b4 = il. b2,b3 iff ex b5 being Function of NAT ,the Instruction-Locations of b2 st
( b5 is bijective & ( for b6, b7 being Nat holds
( b6 <= b7 iff b5 . b6 <= b5 . b7 ) ) & b4 = b5 . b3 ) );

theorem Th25: :: AMISTD_1:25
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3, b4 being natural number st il. b2,b3 = il. b2,b4 holds
b3 = b4
proof end;

theorem Th26: :: AMISTD_1:26
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being Instruction-Location of b2 ex b4 being natural number st b3 = il. b2,b4
proof end;

definition
let c2 be with_non-empty_elements set ;
let c3 be non empty non void IC-Ins-separated definite standard AMI-Struct of c2;
let c4 be Instruction-Location of c3;
func locnum c3 -> natural number means :Def13: :: AMISTD_1:def 13
il. a2,a4 = a3;
existence
ex b1 being natural number st il. c3,b1 = c4
by Th26;
uniqueness
for b1, b2 being natural number st il. c3,b1 = c4 & il. c3,b2 = c4 holds
b1 = b2
by Th25;
end;

:: deftheorem Def13 defines locnum AMISTD_1:def 13 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being Instruction-Location of b2
for b4 being natural number holds
( b4 = locnum b3 iff il. b2,b4 = b3 );

definition
let c2 be with_non-empty_elements set ;
let c3 be non empty non void IC-Ins-separated definite standard AMI-Struct of c2;
let c4 be Instruction-Location of c3;
redefine func locnum as locnum c3 -> Nat;
coherence
locnum c4 is Nat
by ORDINAL2:def 21;
end;

theorem Th27: :: AMISTD_1:27
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3, b4 being Instruction-Location of b2 st locnum b3 = locnum b4 holds
b3 = b4
proof end;

theorem Th28: :: AMISTD_1:28
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3, b4 being natural number holds
( il. b2,b3 <= il. b2,b4 iff b3 <= b4 )
proof end;

theorem Th29: :: AMISTD_1:29
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3, b4 being Instruction-Location of b2 holds
( locnum b3 <= locnum b4 iff b3 <= b4 )
proof end;

theorem Th30: :: AMISTD_1:30
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1 st b2 is standard holds
b2 is InsLoc-antisymmetric
proof end;

registration
let c2 be with_non-empty_elements set ;
cluster non empty non void IC-Ins-separated definite standard -> non empty non void IC-Ins-separated definite InsLoc-antisymmetric AMI-Struct of a1;
coherence
for b1 being non empty non void IC-Ins-separated definite AMI-Struct of c2 st b1 is standard holds
b1 is InsLoc-antisymmetric
by Th30;
end;

definition
let c2 be with_non-empty_elements set ;
let c3 be non empty non void IC-Ins-separated definite standard AMI-Struct of c2;
let c4 be Instruction-Location of c3;
let c5 be natural number ;
func c3 + c4 -> Instruction-Location of a2 equals :: AMISTD_1:def 14
il. a2,((locnum a3) + a4);
coherence
il. c3,((locnum c4) + c5) is Instruction-Location of c3
;
end;

:: deftheorem Def14 defines + AMISTD_1:def 14 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being Instruction-Location of b2
for b4 being natural number holds b3 + b4 = il. b2,((locnum b3) + b4);

theorem Th31: :: AMISTD_1:31
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being Instruction-Location of b2 holds b3 + 0 = b3 by Def13;

theorem Th32: :: AMISTD_1:32
for b1 being natural number
for b2 being with_non-empty_elements set
for b3 being non empty non void IC-Ins-separated definite standard AMI-Struct of b2
for b4, b5 being Instruction-Location of b3 st b4 + b1 = b5 + b1 holds
b4 = b5
proof end;

theorem Th33: :: AMISTD_1:33
for b1 being natural number
for b2 being with_non-empty_elements set
for b3 being non empty non void IC-Ins-separated definite standard AMI-Struct of b2
for b4 being Instruction-Location of b3 holds (locnum b4) + b1 = locnum (b4 + b1) by Def13;

definition
let c2 be with_non-empty_elements set ;
let c3 be non empty non void IC-Ins-separated definite standard AMI-Struct of c2;
let c4 be Instruction-Location of c3;
func NextLoc c3 -> Instruction-Location of a2 equals :: AMISTD_1:def 15
a3 + 1;
coherence
c4 + 1 is Instruction-Location of c3
;
end;

:: deftheorem Def15 defines NextLoc AMISTD_1:def 15 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being Instruction-Location of b2 holds NextLoc b3 = b3 + 1;

theorem Th34: :: AMISTD_1:34
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being Instruction-Location of b2 holds NextLoc b3 = il. b2,((locnum b3) + 1) ;

theorem Th35: :: AMISTD_1:35
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being Instruction-Location of b2 holds b3 <> NextLoc b3
proof end;

theorem Th36: :: AMISTD_1:36
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3, b4 being Instruction-Location of b2 st NextLoc b3 = NextLoc b4 holds
b3 = b4
proof end;

theorem Th37: :: AMISTD_1:37
for b1 being natural number
for b2 being with_non-empty_elements set holds il. (STC b2),b1 = b1
proof end;

theorem Th38: :: AMISTD_1:38
for b1 being with_non-empty_elements set
for b2 being Instruction of (STC b1)
for b3 being State of (STC b1) st InsCode b2 = 1 holds
(Exec b2,b3) . (IC (STC b1)) = NextLoc (IC b3)
proof end;

theorem Th39: :: AMISTD_1:39
for b1 being with_non-empty_elements set
for b2 being Instruction-Location of (STC b1)
for b3 being Element of the Instructions of (STC b1) st InsCode b3 = 1 holds
NIC b3,b2 = {(NextLoc b2)}
proof end;

theorem Th40: :: AMISTD_1:40
for b1 being with_non-empty_elements set
for b2 being Instruction-Location of (STC b1) holds SUCC b2 = {b2,(NextLoc b2)}
proof end;

definition
let c2 be with_non-empty_elements set ;
let c3 be non empty non void IC-Ins-separated definite standard AMI-Struct of c2;
let c4 be Instruction of c3;
attr a3 is sequential means :: AMISTD_1:def 16
for b1 being State of a2 holds (Exec a3,b1) . (IC a2) = NextLoc (IC b1);
end;

:: deftheorem Def16 defines sequential AMISTD_1:def 16 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being Instruction of b2 holds
( b3 is sequential iff for b4 being State of b2 holds (Exec b3,b4) . (IC b2) = NextLoc (IC b4) );

theorem Th41: :: AMISTD_1:41
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite realistic standard AMI-Struct of b1
for b3 being Instruction-Location of b2
for b4 being Instruction of b2 st b4 is sequential holds
NIC b4,b3 = {(NextLoc b3)}
proof end;

theorem Th42: :: AMISTD_1:42
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite realistic standard AMI-Struct of b1
for b3 being Instruction of b2 st b3 is sequential holds
not b3 is halting
proof end;

registration
let c2 be with_non-empty_elements set ;
let c3 be non empty non void IC-Ins-separated definite realistic standard AMI-Struct of c2;
cluster sequential -> non halting Element of the Instructions of a2;
coherence
for b1 being Instruction of c3 st b1 is sequential holds
not b1 is halting
by Th42;
cluster halting -> non sequential Element of the Instructions of a2;
coherence
for b1 being Instruction of c3 st b1 is halting holds
not b1 is sequential
by Th42;
end;

theorem Th43: :: AMISTD_1:43
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being Instruction of b2 st not JUMP b3 is empty holds
not b3 is sequential
proof end;

definition
let c2 be with_non-empty_elements set ;
let c3 be non empty non void IC-Ins-separated definite AMI-Struct of c2;
let c4 be FinPartState of c3;
attr a3 is closed means :Def17: :: AMISTD_1:def 17
for b1 being Instruction-Location of a2 st b1 in dom a3 holds
NIC (pi a3,b1),b1 c= dom a3;
attr a3 is really-closed means :: AMISTD_1:def 18
for b1 being State of a2 st a3 c= b1 & IC b1 in dom a3 holds
for b2 being Nat holds IC ((Computation b1) . b2) in dom a3;
end;

:: deftheorem Def17 defines closed AMISTD_1:def 17 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being FinPartState of b2 holds
( b3 is closed iff for b4 being Instruction-Location of b2 st b4 in dom b3 holds
NIC (pi b3,b4),b4 c= dom b3 );

:: deftheorem Def18 defines really-closed AMISTD_1:def 18 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being FinPartState of b2 holds
( b3 is really-closed iff for b4 being State of b2 st b3 c= b4 & IC b4 in dom b3 holds
for b5 being Nat holds IC ((Computation b4) . b5) in dom b3 );

definition
let c2 be with_non-empty_elements set ;
let c3 be non empty non void IC-Ins-separated definite standard AMI-Struct of c2;
let c4 be FinPartState of c3;
attr a3 is para-closed means :: AMISTD_1:def 19
for b1 being State of a2 st a3 c= b1 & IC b1 = il. a2,0 holds
for b2 being Nat holds IC ((Computation b1) . b2) in dom a3;
end;

:: deftheorem Def19 defines para-closed AMISTD_1:def 19 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being FinPartState of b2 holds
( b3 is para-closed iff for b4 being State of b2 st b3 c= b4 & IC b4 = il. b2,0 holds
for b5 being Nat holds IC ((Computation b4) . b5) in dom b3 );

theorem Th44: :: AMISTD_1:44
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated steady-programmed definite standard AMI-Struct of b1
for b3 being FinPartState of b2 st b3 is really-closed & il. b2,0 in dom b3 holds
b3 is para-closed
proof end;

theorem Th45: :: AMISTD_1:45
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of b1
for b3 being FinPartState of b2 st b3 is closed holds
b3 is really-closed
proof end;

registration
let c2 be with_non-empty_elements set ;
let c3 be non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of c2;
cluster closed -> with_non-empty_elements really-closed FinPartState of a2;
coherence
for b1 being FinPartState of c3 st b1 is closed holds
b1 is really-closed
by Th45;
end;

theorem Th46: :: AMISTD_1:46
for b1 being with_non-empty_elements set
for b2 being non empty non void halting IC-Ins-separated definite realistic standard AMI-Struct of b1 holds (il. b2,0) .--> (halt b2) is closed
proof end;

definition
let c2 be with_non-empty_elements set ;
let c3 be non empty non void IC-Ins-separated definite AMI-Struct of c2;
let c4 be FinPartState of c3;
attr a3 is lower means :Def20: :: AMISTD_1:def 20
for b1 being Instruction-Location of a2 st b1 in dom a3 holds
for b2 being Instruction-Location of a2 st b2 <= b1 holds
b2 in dom a3;
end;

:: deftheorem Def20 defines lower AMISTD_1:def 20 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being FinPartState of b2 holds
( b3 is lower iff for b4 being Instruction-Location of b2 st b4 in dom b3 holds
for b5 being Instruction-Location of b2 st b5 <= b4 holds
b5 in dom b3 );

theorem Th47: :: AMISTD_1:47
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being empty FinPartState of b2 holds b3 is lower
proof end;

registration
let c2 be with_non-empty_elements set ;
let c3 be non empty non void IC-Ins-separated definite AMI-Struct of c2;
cluster empty -> with_non-empty_elements lower FinPartState of a2;
coherence
for b1 being FinPartState of c3 st b1 is empty holds
b1 is lower
by Th47;
end;

theorem Th48: :: AMISTD_1:48
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being Element of the Instructions of b2 holds (il. b2,0) .--> b3 is lower
proof end;

registration
let c2 be with_non-empty_elements set ;
let c3 be non empty non void IC-Ins-separated definite standard AMI-Struct of c2;
cluster non empty trivial with_non-empty_elements programmed lower FinPartState of a2;
existence
ex b1 being FinPartState of c3 st
( b1 is lower & not b1 is empty & b1 is trivial & b1 is programmed )
proof end;
end;

theorem Th49: :: AMISTD_1:49
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being non empty programmed lower FinPartState of b2 holds il. b2,0 in dom b3
proof end;

theorem Th50: :: AMISTD_1:50
for b1 being natural number
for b2 being with_non-empty_elements set
for b3 being non empty non void IC-Ins-separated definite standard AMI-Struct of b2
for b4 being programmed lower FinPartState of b3 holds
( b1 < card b4 iff il. b3,b1 in dom b4 )
proof end;

definition
let c2 be with_non-empty_elements set ;
let c3 be non empty non void IC-Ins-separated definite standard AMI-Struct of c2;
let c4 be non empty programmed FinPartState of c3;
func LastLoc c3 -> Instruction-Location of a2 means :Def21: :: AMISTD_1:def 21
ex b1 being non empty finite natural-membered set st
( b1 = { (locnum b2) where B is Element of the Instruction-Locations of a2 : b2 in dom a3 } & a4 = il. a2,(max b1) );
existence
ex b1 being Instruction-Location of c3ex b2 being non empty finite natural-membered set st
( b2 = { (locnum b3) where B is Element of the Instruction-Locations of c3 : b3 in dom c4 } & b1 = il. c3,(max b2) )
proof end;
uniqueness
for b1, b2 being Instruction-Location of c3 st ex b3 being non empty finite natural-membered set st
( b3 = { (locnum b4) where B is Element of the Instruction-Locations of c3 : b4 in dom c4 } & b1 = il. c3,(max b3) ) & ex b3 being non empty finite natural-membered set st
( b3 = { (locnum b4) where B is Element of the Instruction-Locations of c3 : b4 in dom c4 } & b2 = il. c3,(max b3) ) holds
b1 = b2
;
end;

:: deftheorem Def21 defines LastLoc AMISTD_1:def 21 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being non empty programmed FinPartState of b2
for b4 being Instruction-Location of b2 holds
( b4 = LastLoc b3 iff ex b5 being non empty finite natural-membered set st
( b5 = { (locnum b6) where B is Element of the Instruction-Locations of b2 : b6 in dom b3 } & b4 = il. b2,(max b5) ) );

theorem Th51: :: AMISTD_1:51
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being non empty programmed FinPartState of b2 holds LastLoc b3 in dom b3
proof end;

theorem Th52: :: AMISTD_1:52
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3, b4 being non empty programmed FinPartState of b2 st b3 c= b4 holds
LastLoc b3 <= LastLoc b4
proof end;

theorem Th53: :: AMISTD_1:53
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being non empty programmed FinPartState of b2
for b4 being Instruction-Location of b2 st b4 in dom b3 holds
b4 <= LastLoc b3
proof end;

theorem Th54: :: AMISTD_1:54
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being non empty programmed lower FinPartState of b2
for b4 being non empty programmed FinPartState of b2 st b3 c= b4 & LastLoc b3 = LastLoc b4 holds
b3 = b4
proof end;

theorem Th55: :: AMISTD_1:55
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being non empty programmed lower FinPartState of b2 holds LastLoc b3 = il. b2,((card b3) -' 1)
proof end;

registration
let c2 be with_non-empty_elements set ;
let c3 be non empty non void IC-Ins-separated steady-programmed definite standard AMI-Struct of c2;
cluster non empty programmed really-closed lower -> with_non-empty_elements para-closed FinPartState of a2;
coherence
for b1 being FinPartState of c3 st b1 is really-closed & b1 is lower & not b1 is empty & b1 is programmed holds
b1 is para-closed
proof end;
end;

E54: now
let c2 be with_non-empty_elements set ;
let c3 be non empty non void halting IC-Ins-separated definite standard AMI-Struct of c2;
set c4 = (il. c3,0) .--> (halt c3);
E55: dom ((il. c3,0) .--> (halt c3)) = {(il. c3,0)} by CQC_LANG:5;
then E56: card (dom ((il. c3,0) .--> (halt c3))) = 1 by CARD_1:79;
(il. c3,0) .--> (halt c3) is lower FinPartState of c3 by Th48;
then E57: LastLoc ((il. c3,0) .--> (halt c3)) = il. c3,((card ((il. c3,0) .--> (halt c3))) -' 1) by Th55
.= il. c3,((card (dom ((il. c3,0) .--> (halt c3)))) -' 1) by PRE_CIRC:21
.= il. c3,0 by E56, BINARITH:51 ;
hence ((il. c3,0) .--> (halt c3)) . (LastLoc ((il. c3,0) .--> (halt c3))) = halt c3 by CQC_LANG:6;
let c5 be Instruction-Location of c3;
assume ((il. c3,0) .--> (halt c3)) . c5 = halt c3 ;
assume c5 in dom ((il. c3,0) .--> (halt c3)) ;
hence c5 = LastLoc ((il. c3,0) .--> (halt c3)) by E55, E57, TARSKI:def 1;
end;

definition
let c2 be with_non-empty_elements set ;
let c3 be non empty non void halting IC-Ins-separated definite standard AMI-Struct of c2;
let c4 be non empty programmed FinPartState of c3;
attr a3 is halt-ending means :: AMISTD_1:def 22
a3 . (LastLoc a3) = halt a2;
attr a3 is unique-halt means :: AMISTD_1:def 23
for b1 being Instruction-Location of a2 st a3 . b1 = halt a2 & b1 in dom a3 holds
b1 = LastLoc a3;
end;

:: deftheorem Def22 defines halt-ending AMISTD_1:def 22 :
for b1 being with_non-empty_elements set
for b2 being non empty non void halting IC-Ins-separated definite standard AMI-Struct of b1
for b3 being non empty programmed FinPartState of b2 holds
( b3 is halt-ending iff b3 . (LastLoc b3) = halt b2 );

:: deftheorem Def23 defines unique-halt AMISTD_1:def 23 :
for b1 being with_non-empty_elements set
for b2 being non empty non void halting IC-Ins-separated definite standard AMI-Struct of b1
for b3 being non empty programmed FinPartState of b2 holds
( b3 is unique-halt iff for b4 being Instruction-Location of b2 st b3 . b4 = halt b2 & b4 in dom b3 holds
b4 = LastLoc b3 );

registration
let c2 be with_non-empty_elements set ;
let c3 be non empty non void halting IC-Ins-separated definite standard AMI-Struct of c2;
cluster non empty trivial with_non-empty_elements programmed lower halt-ending unique-halt FinPartState of a2;
existence
ex b1 being non empty programmed lower FinPartState of c3 st
( b1 is halt-ending & b1 is unique-halt & b1 is trivial )
proof end;
end;

registration
let c2 be with_non-empty_elements set ;
let c3 be non empty non void halting IC-Ins-separated definite realistic standard AMI-Struct of c2;
cluster non empty trivial with_non-empty_elements programmed closed lower FinPartState of a2;
existence
ex b1 being FinPartState of c3 st
( b1 is trivial & b1 is closed & b1 is lower & not b1 is empty & b1 is programmed )
proof end;
end;

registration
let c2 be with_non-empty_elements set ;
let c3 be non empty non void halting IC-Ins-separated definite realistic standard AMI-Struct of c2;
cluster non empty trivial with_non-empty_elements programmed closed lower halt-ending unique-halt FinPartState of a2;
existence
ex b1 being non empty programmed lower FinPartState of c3 st
( b1 is halt-ending & b1 is unique-halt & b1 is trivial & b1 is closed )
proof end;
end;

registration
let c2 be with_non-empty_elements set ;
let c3 be non empty non void halting IC-Ins-separated steady-programmed definite realistic standard AMI-Struct of c2;
cluster non empty trivial with_non-empty_elements autonomic programmed closed really-closed para-closed lower halt-ending unique-halt FinPartState of a2;
existence
ex b1 being non empty programmed lower FinPartState of c3 st
( b1 is halt-ending & b1 is unique-halt & b1 is autonomic & b1 is trivial & b1 is closed )
proof end;
end;

definition
let c2 be with_non-empty_elements set ;
let c3 be non empty non void halting IC-Ins-separated definite standard AMI-Struct of c2;
mode pre-Macro of a2 is non empty programmed lower halt-ending unique-halt FinPartState of a2;
end;

registration
let c2 be with_non-empty_elements set ;
let c3 be non empty non void halting IC-Ins-separated definite realistic standard AMI-Struct of c2;
cluster closed FinPartState of a2;
existence
ex b1 being pre-Macro of c3 st b1 is closed
proof end;
end;