:: AMI_3 semantic presentation

definition
func SCM -> strict AMI-Struct of {INT } equals :: AMI_3:def 1
AMI-Struct(# NAT ,0,SCM-Instr-Loc ,(Segm 9),SCM-Instr ,SCM-OK ,SCM-Exec #);
coherence
AMI-Struct(# NAT ,0,SCM-Instr-Loc ,(Segm 9),SCM-Instr ,SCM-OK ,SCM-Exec #) is strict AMI-Struct of {INT }
;
end;

:: deftheorem Def1 defines SCM AMI_3:def 1 :
SCM = AMI-Struct(# NAT ,0,SCM-Instr-Loc ,(Segm 9),SCM-Instr ,SCM-OK ,SCM-Exec #);

registration
cluster SCM -> non empty strict non void ;
coherence
( not SCM is empty & not SCM is void )
by AMI_1:def 3, STRUCT_0:def 1;
end;

theorem Th1: :: AMI_3:1
SCM is data-oriented
proof end;

theorem Th2: :: AMI_3:2
SCM is definite
proof end;

registration
cluster SCM -> non empty strict non void IC-Ins-separated data-oriented definite ;
coherence
( SCM is IC-Ins-separated & SCM is data-oriented & SCM is definite )
proof end;
end;

definition
mode Data-Location -> Object of SCM means :Def2: :: AMI_3:def 2
a1 in SCM-Data-Loc ;
existence
ex b1 being Object of SCM st b1 in SCM-Data-Loc
proof end;
end;

:: deftheorem Def2 defines Data-Location AMI_3:def 2 :
for b1 being Object of SCM holds
( b1 is Data-Location iff b1 in SCM-Data-Loc );

definition
let c1 be State of SCM ;
let c2 be Data-Location ;
redefine func . as c1 . c2 -> Integer;
coherence
c1 . c2 is Integer
proof end;
end;

definition
let c1, c2 be Data-Location ;
func c1 := c2 -> Instruction of SCM equals :: AMI_3:def 3
[1,<*a1,a2*>];
correctness
coherence
[1,<*c1,c2*>] is Instruction of SCM
;
proof end;
func AddTo c1,c2 -> Instruction of SCM equals :: AMI_3:def 4
[2,<*a1,a2*>];
correctness
coherence
[2,<*c1,c2*>] is Instruction of SCM
;
proof end;
func SubFrom c1,c2 -> Instruction of SCM equals :: AMI_3:def 5
[3,<*a1,a2*>];
correctness
coherence
[3,<*c1,c2*>] is Instruction of SCM
;
proof end;
func MultBy c1,c2 -> Instruction of SCM equals :: AMI_3:def 6
[4,<*a1,a2*>];
correctness
coherence
[4,<*c1,c2*>] is Instruction of SCM
;
proof end;
func Divide c1,c2 -> Instruction of SCM equals :: AMI_3:def 7
[5,<*a1,a2*>];
correctness
coherence
[5,<*c1,c2*>] is Instruction of SCM
;
proof end;
end;

:: deftheorem Def3 defines := AMI_3:def 3 :
for b1, b2 being Data-Location holds b1 := b2 = [1,<*b1,b2*>];

:: deftheorem Def4 defines AddTo AMI_3:def 4 :
for b1, b2 being Data-Location holds AddTo b1,b2 = [2,<*b1,b2*>];

:: deftheorem Def5 defines SubFrom AMI_3:def 5 :
for b1, b2 being Data-Location holds SubFrom b1,b2 = [3,<*b1,b2*>];

:: deftheorem Def6 defines MultBy AMI_3:def 6 :
for b1, b2 being Data-Location holds MultBy b1,b2 = [4,<*b1,b2*>];

:: deftheorem Def7 defines Divide AMI_3:def 7 :
for b1, b2 being Data-Location holds Divide b1,b2 = [5,<*b1,b2*>];

definition
let c1 be Instruction-Location of SCM ;
func goto c1 -> Instruction of SCM equals :: AMI_3:def 8
[6,<*a1*>];
correctness
coherence
[6,<*c1*>] is Instruction of SCM
;
by AMI_2:3;
let c2 be Data-Location ;
func c2 =0_goto c1 -> Instruction of SCM equals :: AMI_3:def 9
[7,<*a1,a2*>];
correctness
coherence
[7,<*c1,c2*>] is Instruction of SCM
;
proof end;
func c2 >0_goto c1 -> Instruction of SCM equals :: AMI_3:def 10
[8,<*a1,a2*>];
correctness
coherence
[8,<*c1,c2*>] is Instruction of SCM
;
proof end;
end;

:: deftheorem Def8 defines goto AMI_3:def 8 :
for b1 being Instruction-Location of SCM holds goto b1 = [6,<*b1*>];

:: deftheorem Def9 defines =0_goto AMI_3:def 9 :
for b1 being Instruction-Location of SCM
for b2 being Data-Location holds b2 =0_goto b1 = [7,<*b1,b2*>];

:: deftheorem Def10 defines >0_goto AMI_3:def 10 :
for b1 being Instruction-Location of SCM
for b2 being Data-Location holds b2 >0_goto b1 = [8,<*b1,b2*>];

theorem Th3: :: AMI_3:3
canceled;

theorem Th4: :: AMI_3:4
IC SCM = 0 ;

theorem Th5: :: AMI_3:5
for b1 being State of SCM
for b2 being SCM-State st b2 = b1 holds
IC b1 = IC b2 by AMI_2:def 6;

definition
let c1 be Instruction-Location of SCM ;
func Next c1 -> Instruction-Location of SCM means :Def11: :: AMI_3:def 11
ex b1 being Element of SCM-Instr-Loc st
( b1 = a1 & a2 = Next b1 );
existence
ex b1 being Instruction-Location of SCM ex b2 being Element of SCM-Instr-Loc st
( b2 = c1 & b1 = Next b2 )
proof end;
correctness
uniqueness
for b1, b2 being Instruction-Location of SCM st ex b3 being Element of SCM-Instr-Loc st
( b3 = c1 & b1 = Next b3 ) & ex b3 being Element of SCM-Instr-Loc st
( b3 = c1 & b2 = Next b3 ) holds
b1 = b2
;
;
end;

:: deftheorem Def11 defines Next AMI_3:def 11 :
for b1, b2 being Instruction-Location of SCM holds
( b2 = Next b1 iff ex b3 being Element of SCM-Instr-Loc st
( b3 = b1 & b2 = Next b3 ) );

theorem Th6: :: AMI_3:6
for b1 being Instruction-Location of SCM
for b2 being Element of SCM-Instr-Loc st b2 = b1 holds
Next b2 = Next b1 by Def11;

theorem Th7: :: AMI_3:7
for b1 being Instruction of SCM
for b2 being State of SCM
for b3 being Element of SCM-Instr st b3 = b1 holds
for b4 being SCM-State st b4 = b2 holds
Exec b1,b2 = SCM-Exec-Res b3,b4 by AMI_2:def 17;

theorem Th8: :: AMI_3:8
for b1, b2 being Data-Location
for b3 being State of SCM holds
( (Exec (b1 := b2),b3) . (IC SCM ) = Next (IC b3) & (Exec (b1 := b2),b3) . b1 = b3 . b2 & ( for b4 being Data-Location st b4 <> b1 holds
(Exec (b1 := b2),b3) . b4 = b3 . b4 ) )
proof end;

theorem Th9: :: AMI_3:9
for b1, b2 being Data-Location
for b3 being State of SCM holds
( (Exec (AddTo b1,b2),b3) . (IC SCM ) = Next (IC b3) & (Exec (AddTo b1,b2),b3) . b1 = (b3 . b1) + (b3 . b2) & ( for b4 being Data-Location st b4 <> b1 holds
(Exec (AddTo b1,b2),b3) . b4 = b3 . b4 ) )
proof end;

theorem Th10: :: AMI_3:10
for b1, b2 being Data-Location
for b3 being State of SCM holds
( (Exec (SubFrom b1,b2),b3) . (IC SCM ) = Next (IC b3) & (Exec (SubFrom b1,b2),b3) . b1 = (b3 . b1) - (b3 . b2) & ( for b4 being Data-Location st b4 <> b1 holds
(Exec (SubFrom b1,b2),b3) . b4 = b3 . b4 ) )
proof end;

theorem Th11: :: AMI_3:11
for b1, b2 being Data-Location
for b3 being State of SCM holds
( (Exec (MultBy b1,b2),b3) . (IC SCM ) = Next (IC b3) & (Exec (MultBy b1,b2),b3) . b1 = (b3 . b1) * (b3 . b2) & ( for b4 being Data-Location st b4 <> b1 holds
(Exec (MultBy b1,b2),b3) . b4 = b3 . b4 ) )
proof end;

theorem Th12: :: AMI_3:12
for b1, b2 being Data-Location
for b3 being State of SCM holds
( (Exec (Divide b1,b2),b3) . (IC SCM ) = Next (IC b3) & ( b1 <> b2 implies (Exec (Divide b1,b2),b3) . b1 = (b3 . b1) div (b3 . b2) ) & (Exec (Divide b1,b2),b3) . b2 = (b3 . b1) mod (b3 . b2) & ( for b4 being Data-Location st b4 <> b1 & b4 <> b2 holds
(Exec (Divide b1,b2),b3) . b4 = b3 . b4 ) )
proof end;

theorem Th13: :: AMI_3:13
for b1 being Data-Location
for b2 being Instruction-Location of SCM
for b3 being State of SCM holds
( (Exec (goto b2),b3) . (IC SCM ) = b2 & (Exec (goto b2),b3) . b1 = b3 . b1 )
proof end;

theorem Th14: :: AMI_3:14
for b1, b2 being Data-Location
for b3 being Instruction-Location of SCM
for b4 being State of SCM holds
( ( b4 . b1 = 0 implies (Exec (b1 =0_goto b3),b4) . (IC SCM ) = b3 ) & ( b4 . b1 <> 0 implies (Exec (b1 =0_goto b3),b4) . (IC SCM ) = Next (IC b4) ) & (Exec (b1 =0_goto b3),b4) . b2 = b4 . b2 )
proof end;

theorem Th15: :: AMI_3:15
for b1, b2 being Data-Location
for b3 being Instruction-Location of SCM
for b4 being State of SCM holds
( ( b4 . b1 > 0 implies (Exec (b1 >0_goto b3),b4) . (IC SCM ) = b3 ) & ( b4 . b1 <= 0 implies (Exec (b1 >0_goto b3),b4) . (IC SCM ) = Next (IC b4) ) & (Exec (b1 >0_goto b3),b4) . b2 = b4 . b2 )
proof end;

Lemma15: for b1 being Instruction of SCM st ex b2 being State of SCM st (Exec b1,b2) . (IC SCM ) = Next (IC b2) holds
not b1 is halting
proof end;

Lemma16: for b1 being Instruction of SCM st b1 = [0,{} ] holds
b1 is halting
proof end;

Lemma17: for b1, b2 being Data-Location holds not b1 := b2 is halting
proof end;

Lemma18: for b1, b2 being Data-Location holds not AddTo b1,b2 is halting
proof end;

Lemma19: for b1, b2 being Data-Location holds not SubFrom b1,b2 is halting
proof end;

Lemma20: for b1, b2 being Data-Location holds not MultBy b1,b2 is halting
proof end;

Lemma21: for b1, b2 being Data-Location holds not Divide b1,b2 is halting
proof end;

Lemma22: for b1 being Instruction-Location of SCM holds not goto b1 is halting
proof end;

Lemma23: for b1 being Data-Location
for b2 being Instruction-Location of SCM holds not b1 =0_goto b2 is halting
proof end;

Lemma24: for b1 being Data-Location
for b2 being Instruction-Location of SCM holds not b1 >0_goto b2 is halting
proof end;

Lemma25: for b1 being set holds
( b1 is Instruction of SCM iff ( b1 = [0,{} ] or ex b2, b3 being Data-Location st b1 = b2 := b3 or ex b2, b3 being Data-Location st b1 = AddTo b2,b3 or ex b2, b3 being Data-Location st b1 = SubFrom b2,b3 or ex b2, b3 being Data-Location st b1 = MultBy b2,b3 or ex b2, b3 being Data-Location st b1 = Divide b2,b3 or ex b2 being Instruction-Location of SCM st b1 = goto b2 or ex b2 being Data-Location ex b3 being Instruction-Location of SCM st b1 = b2 =0_goto b3 or ex b2 being Data-Location ex b3 being Instruction-Location of SCM st b1 = b2 >0_goto b3 ) )
proof end;

registration
cluster SCM -> non empty strict non void halting IC-Ins-separated data-oriented definite ;
coherence
SCM is halting
proof end;
end;

Lemma26: for b1 being Instruction of SCM st b1 is halting holds
b1 = halt SCM
proof end;

Lemma27: halt SCM = [0,{} ]
proof end;

theorem Th16: :: AMI_3:16
canceled;

theorem Th17: :: AMI_3:17
canceled;

theorem Th18: :: AMI_3:18
for b1, b2 being Integer holds b1 * b2,0 are_congruent_mod b1
proof end;

scheme :: AMI_3:sch 1
s1{ F1() -> Nat, F2() -> Nat, P1[ set ] } :
P1[F2()]
provided
E29: P1[0] and
E30: F1() > 0 and
E31: for b1, b2 being Nat st P1[F1() * b1] & b2 <> 0 & b2 <= F1() holds
P1[(F1() * b1) + b2]
proof end;

theorem Th19: :: AMI_3:19
for b1, b2 being non empty set
for b3, b4 being PartFunc of b1,b2 st ( for b5 being Element of b1
for b6 being Element of b2 holds
( [b5,b6] in b3 iff [b5,b6] in b4 ) ) holds
b3 = b4
proof end;

Lemma30: for b1, b2 being Function
for b3, b4 being set st b1 | b3 = b2 | b3 & b1 | b4 = b2 | b4 holds
b1 | (b3 \/ b4) = b2 | (b3 \/ b4)
by RELAT_1:185;

Lemma31: for b1 being Function
for b2 being set st b2 in dom b1 holds
b1 | {b2} = {[b2,(b1 . b2)]}
by GRFUNC_1:89;

Lemma32: for b1 being Function
for b2 being set st b2 misses dom b1 holds
b1 | b2 = {}
by RELAT_1:95;

theorem Th20: :: AMI_3:20
canceled;

theorem Th21: :: AMI_3:21
canceled;

theorem Th22: :: AMI_3:22
canceled;

theorem Th23: :: AMI_3:23
canceled;

theorem Th24: :: AMI_3:24
for b1, b2 being Function
for b3 being set st dom b1 = dom b2 & b1 . b3 = b2 . b3 holds
b1 | {b3} = b2 | {b3}
proof end;

theorem Th25: :: AMI_3:25
for b1, b2 being Function
for b3, b4 being set st dom b1 = dom b2 & b1 . b3 = b2 . b3 & b1 . b4 = b2 . b4 holds
b1 | {b3,b4} = b2 | {b3,b4}
proof end;

theorem Th26: :: AMI_3:26
for b1, b2 being Function
for b3, b4, b5 being set st dom b1 = dom b2 & b1 . b3 = b2 . b3 & b1 . b4 = b2 . b4 & b1 . b5 = b2 . b5 holds
b1 | {b3,b4,b5} = b2 | {b3,b4,b5}
proof end;

theorem Th27: :: AMI_3:27
for b1, b2 being set
for b3 being Function st b1 in dom b3 & b3 . b1 = b2 holds
b1 .--> b2 c= b3
proof end;

theorem Th28: :: AMI_3:28
canceled;

theorem Th29: :: AMI_3:29
for b1, b2, b3, b4 being set
for b5 being Function st b1 in dom b5 & b3 in dom b5 & b5 . b1 = b2 & b5 . b3 = b4 holds
b1,b3 --> b2,b4 c= b5
proof end;

theorem Th30: :: AMI_3:30
canceled;

theorem Th31: :: AMI_3:31
for b1 being set
for b2 being AMI-Struct of b1
for b3 being FinPartState of b2 holds b3 in FinPartSt b2
proof end;

registration
let c1 be set ;
let c2 be AMI-Struct of c1;
cluster FinPartSt a2 -> non empty ;
coherence
not FinPartSt c2 is empty
by Th31;
end;

theorem Th32: :: AMI_3:32
for b1 being set
for b2 being AMI-Struct of b1
for b3 being Element of FinPartSt b2 holds b3 is FinPartState of b2
proof end;

theorem Th33: :: AMI_3:33
for b1 being set
for b2 being AMI-Struct of b1
for b3, b4 being PartFunc of FinPartSt b2, FinPartSt b2 st ( for b5, b6 being FinPartState of b2 holds
( [b5,b6] in b3 iff [b5,b6] in b4 ) ) holds
b3 = b4
proof end;

scheme :: AMI_3:sch 2
s2{ F1() -> non empty with_non-empty_elements set , F2() -> AMI-Struct of F1(), P1[ set , set ], F3() -> PartFunc of FinPartSt F2(), FinPartSt F2(), F4() -> PartFunc of FinPartSt F2(), FinPartSt F2() } :
F3() = F4()
provided
E39: for b1, b2 being FinPartState of F2() holds
( [b1,b2] in F3() iff P1[b1,b2] ) and
E40: for b1, b2 being FinPartState of F2() holds
( [b1,b2] in F4() iff P1[b1,b2] )
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 be Instruction-Location of c2;
func Start-At c3 -> FinPartState of a2 equals :: AMI_3:def 12
(IC a2) .--> a3;
correctness
coherence
(IC c2) .--> c3 is FinPartState of c2
;
proof end;
end;

:: deftheorem Def12 defines Start-At AMI_3:def 12 :
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 Start-At b3 = (IC b2) .--> b3;

theorem Th34: :: AMI_3:34
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 dom (Start-At b3) = {(IC b2)}
proof end;

definition
let c1 be set ;
let c2 be AMI-Struct of c1;
let c3 be FinPartState of c2;
attr a3 is programmed means :Def13: :: AMI_3:def 13
dom a3 c= the Instruction-Locations of a2;
end;

:: deftheorem Def13 defines programmed AMI_3:def 13 :
for b1 being set
for b2 being AMI-Struct of b1
for b3 being FinPartState of b2 holds
( b3 is programmed iff dom b3 c= the Instruction-Locations of b2 );

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

theorem Th35: :: AMI_3:35
for b1 being set
for b2 being AMI-Struct of b1
for b3, b4 being programmed FinPartState of b2 holds b3 +* b4 is programmed
proof end;

theorem Th36: :: AMI_3:36
for b1 being with_non-empty_elements set
for b2 being non void AMI-Struct of b1
for b3 being State of b2 holds dom b3 = the carrier of b2
proof end;

theorem Th37: :: AMI_3:37
for b1 being with_non-empty_elements set
for b2 being AMI-Struct of b1
for b3 being FinPartState of b2 holds dom b3 c= the carrier of b2
proof end;

theorem Th38: :: AMI_3:38
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 programmed FinPartState of b2
for b4 being State of b2 st b3 c= b4 holds
for b5 being Nat holds b3 c= (Computation b4) . b5
proof end;

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated AMI-Struct of c1;
let c3 be State of c2;
let c4 be Instruction-Location of c2;
pred c3 starts_at c4 means :: AMI_3:def 14
IC a3 = a4;
end;

:: deftheorem Def14 defines starts_at AMI_3:def 14 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated AMI-Struct of b1
for b3 being State of b2
for b4 being Instruction-Location of b2 holds
( b3 starts_at b4 iff IC b3 = b4 );

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void halting IC-Ins-separated AMI-Struct of c1;
let c3 be State of c2;
let c4 be Instruction-Location of c2;
pred c3 halts_at c4 means :Def15: :: AMI_3:def 15
a3 . a4 = halt a2;
end;

:: deftheorem Def15 defines halts_at AMI_3:def 15 :
for b1 being with_non-empty_elements set
for b2 being non empty non void halting IC-Ins-separated AMI-Struct of b1
for b3 being State of b2
for b4 being Instruction-Location of b2 holds
( b3 halts_at b4 iff b3 . b4 = halt b2 );

theorem Th39: :: AMI_3:39
for b1 being with_non-empty_elements set
for b2 being non void AMI-Struct of b1
for b3 being FinPartState of b2 ex b4 being State of b2 st b3 c= b4
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 be FinPartState of c2;
assume E44: IC c2 in dom c3 ;
func IC c3 -> Instruction-Location of a2 equals :Def16: :: AMI_3:def 16
a3 . (IC a2);
coherence
c3 . (IC c2) is Instruction-Location of c2
proof end;
end;

:: deftheorem Def16 defines IC AMI_3:def 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 being FinPartState of b2 st IC b2 in dom b3 holds
IC b3 = b3 . (IC b2);

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 FinPartState of c2;
let c4 be Instruction-Location of c2;
pred c3 starts_at c4 means :: AMI_3:def 17
( IC a2 in dom a3 & IC a3 = a4 );
end;

:: deftheorem Def17 defines starts_at AMI_3: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
for b4 being Instruction-Location of b2 holds
( b3 starts_at b4 iff ( IC b2 in dom b3 & IC b3 = b4 ) );

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void halting IC-Ins-separated definite AMI-Struct of c1;
let c3 be FinPartState of c2;
let c4 be Instruction-Location of c2;
pred c3 halts_at c4 means :: AMI_3:def 18
( a4 in dom a3 & a3 . a4 = halt a2 );
end;

:: deftheorem Def18 defines halts_at AMI_3:def 18 :
for b1 being with_non-empty_elements set
for b2 being non empty non void halting IC-Ins-separated definite AMI-Struct of b1
for b3 being FinPartState of b2
for b4 being Instruction-Location of b2 holds
( b3 halts_at b4 iff ( b4 in dom b3 & b3 . b4 = halt b2 ) );

theorem Th40: :: AMI_3:40
for b1 being with_non-empty_elements set
for b2 being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of b1
for b3 being State of b2 holds
( b3 is halting iff ex b4 being Nat st b3 halts_at IC ((Computation b3) . b4) )
proof end;

theorem Th41: :: AMI_3:41
for b1 being with_non-empty_elements set
for b2 being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of b1
for b3 being State of b2
for b4 being FinPartState of b2
for b5 being Instruction-Location of b2 st b4 c= b3 & b4 halts_at b5 holds
b3 halts_at b5
proof end;

theorem Th42: :: AMI_3:42
for b1 being with_non-empty_elements set
for b2 being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of b1
for b3 being State of b2
for b4 being Nat st b3 is halting holds
( Result b3 = (Computation b3) . b4 iff b3 halts_at IC ((Computation b3) . b4) )
proof end;

theorem Th43: :: AMI_3:43
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 State of b2
for b4 being programmed FinPartState of b2
for b5 being Nat holds
( b4 c= b3 iff b4 c= (Computation b3) . b5 )
proof end;

theorem Th44: :: AMI_3:44
for b1 being with_non-empty_elements set
for b2 being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of b1
for b3 being State of b2
for b4 being Nat st b3 halts_at IC ((Computation b3) . b4) holds
Result b3 = (Computation b3) . b4
proof end;

theorem Th45: :: AMI_3:45
for b1, b2 being Nat
for b3 being with_non-empty_elements set st b1 <= b2 holds
for b4 being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of b3
for b5 being State of b4 st b5 halts_at IC ((Computation b5) . b1) holds
b5 halts_at IC ((Computation b5) . b2)
proof end;

theorem Th46: :: AMI_3:46
for b1, b2 being Nat
for b3 being with_non-empty_elements set st b1 <= b2 holds
for b4 being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of b3
for b5 being State of b4 st b5 halts_at IC ((Computation b5) . b1) holds
(Computation b5) . b2 = (Computation b5) . b1
proof end;

theorem Th47: :: AMI_3:47
for b1 being with_non-empty_elements set
for b2 being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of b1
for b3 being State of b2 st ex b4 being Nat st b3 halts_at IC ((Computation b3) . b4) holds
for b4 being Nat holds Result b3 = Result ((Computation b3) . b4)
proof end;

theorem Th48: :: AMI_3:48
for b1 being with_non-empty_elements set
for b2 being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of b1
for b3 being State of b2
for b4 being Instruction-Location of b2
for b5 being Nat holds
( b3 halts_at b4 iff (Computation b3) . b5 halts_at b4 )
proof end;

theorem Th49: :: AMI_3:49
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
for b4 being Instruction-Location of b2 st b3 starts_at b4 holds
for b5 being State of b2 st b3 c= b5 holds
b5 starts_at b4
proof end;

theorem Th50: :: AMI_3:50
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 (Start-At b3) . (IC b2) = b3 by CQC_LANG:6;

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;
redefine func .--> as c3 .--> c4 -> programmed FinPartState of a2;
coherence
c3 .--> c4 is programmed FinPartState of c2
proof end;
end;

Lemma49: for b1 being State of SCM
for b2 being Instruction of SCM
for b3 being Instruction-Location of SCM holds (Exec b2,b1) . b3 = b1 . b3
proof end;

theorem Th51: :: AMI_3:51
SCM is realistic by AMI_1:def 21, AMI_2:6;

registration
cluster SCM -> non empty strict non void halting IC-Ins-separated data-oriented steady-programmed definite realistic ;
coherence
( SCM is steady-programmed & SCM is realistic )
proof end;
end;

definition
let c1 be natural number ;
func dl. c1 -> Data-Location equals :: AMI_3:def 19
(2 * a1) + 1;
coherence
(2 * c1) + 1 is Data-Location
proof end;
func il. c1 -> Instruction-Location of SCM equals :: AMI_3:def 20
(2 * a1) + 2;
coherence
(2 * c1) + 2 is Instruction-Location of SCM
proof end;
end;

:: deftheorem Def19 defines dl. AMI_3:def 19 :
for b1 being natural number holds dl. b1 = (2 * b1) + 1;

:: deftheorem Def20 defines il. AMI_3:def 20 :
for b1 being natural number holds il. b1 = (2 * b1) + 2;

theorem Th52: :: AMI_3:52
for b1, b2 being natural number st b1 <> b2 holds
dl. b1 <> dl. b2
proof end;

theorem Th53: :: AMI_3:53
for b1, b2 being natural number st b1 <> b2 holds
il. b1 <> il. b2
proof end;

theorem Th54: :: AMI_3:54
for b1 being natural number holds Next (il. b1) = il. (b1 + 1)
proof end;

theorem Th55: :: AMI_3:55
for b1 being Data-Location holds ObjectKind b1 = INT
proof end;

definition
let c1 be Data-Location ;
let c2 be Integer;
redefine func .--> as c1 .--> c2 -> FinPartState of SCM ;
coherence
c1 .--> c2 is FinPartState of SCM
proof end;
end;

definition
let c1, c2 be Data-Location ;
let c3, c4 be Integer;
redefine func --> as c1,c2 --> c3,c4 -> FinPartState of SCM ;
coherence
c1,c2 --> c3,c4 is FinPartState of SCM
proof end;
end;

theorem Th56: :: AMI_3:56
for b1, b2 being natural number holds dl. b1 <> il. b2
proof end;

theorem Th57: :: AMI_3:57
for b1 being natural number holds
( IC SCM <> dl. b1 & IC SCM <> il. b1 ) ;

theorem Th58: :: AMI_3:58
for b1 being Instruction of SCM st ex b2 being State of SCM st (Exec b1,b2) . (IC SCM ) = Next (IC b2) holds
not b1 is halting by Lemma15;

theorem Th59: :: AMI_3:59
for b1 being Instruction of SCM st b1 = [0,{} ] holds
b1 is halting by Lemma16;

theorem Th60: :: AMI_3:60
for b1, b2 being Data-Location holds not b1 := b2 is halting by Lemma17;

theorem Th61: :: AMI_3:61
for b1, b2 being Data-Location holds not AddTo b1,b2 is halting by Lemma18;

theorem Th62: :: AMI_3:62
for b1, b2 being Data-Location holds not SubFrom b1,b2 is halting by Lemma19;

theorem Th63: :: AMI_3:63
for b1, b2 being Data-Location holds not MultBy b1,b2 is halting by Lemma20;

theorem Th64: :: AMI_3:64
for b1, b2 being Data-Location holds not Divide b1,b2 is halting by Lemma21;

theorem Th65: :: AMI_3:65
for b1 being Instruction-Location of SCM holds not goto b1 is halting by Lemma22;

theorem Th66: :: AMI_3:66
for b1 being Data-Location
for b2 being Instruction-Location of SCM holds not b1 =0_goto b2 is halting by Lemma23;

theorem Th67: :: AMI_3:67
for b1 being Data-Location
for b2 being Instruction-Location of SCM holds not b1 >0_goto b2 is halting by Lemma24;

theorem Th68: :: AMI_3:68
[0,{} ] is Instruction of SCM by AMI_2:2;

theorem Th69: :: AMI_3:69
for b1 being set holds
( b1 is Instruction of SCM iff ( b1 = [0,{} ] or ex b2, b3 being Data-Location st b1 = b2 := b3 or ex b2, b3 being Data-Location st b1 = AddTo b2,b3 or ex b2, b3 being Data-Location st b1 = SubFrom b2,b3 or ex b2, b3 being Data-Location st b1 = MultBy b2,b3 or ex b2, b3 being Data-Location st b1 = Divide b2,b3 or ex b2 being Instruction-Location of SCM st b1 = goto b2 or ex b2 being Data-Location ex b3 being Instruction-Location of SCM st b1 = b2 =0_goto b3 or ex b2 being Data-Location ex b3 being Instruction-Location of SCM st b1 = b2 >0_goto b3 ) ) by Lemma25;

theorem Th70: :: AMI_3:70
for b1 being Instruction of SCM st b1 is halting holds
b1 = halt SCM by Lemma26;

theorem Th71: :: AMI_3:71
halt SCM = [0,{} ] by Lemma27;