:: SCM_1 semantic presentation

definition
let c1 be Integer;
redefine func <* as <*c1*> -> FinSequence of INT ;
coherence
<*c1*> is FinSequence of INT
proof end;
end;

theorem Th1: :: SCM_1:1
for b1 being State of SCM holds
( IC b1 = b1 . 0 & CurInstr b1 = b1 . (b1 . 0) ) by AMI_3:4;

theorem Th2: :: SCM_1:2
for b1 being State of SCM
for b2 being Nat holds
( CurInstr ((Computation b1) . b2) = b1 . (IC ((Computation b1) . b2)) & CurInstr ((Computation b1) . b2) = b1 . (((Computation b1) . b2) . 0) ) by AMI_3:4, AMI_1:54;

theorem Th3: :: SCM_1:3
for b1 being State of SCM st ex b2 being Nat st b1 . (IC ((Computation b1) . b2)) = halt SCM holds
b1 is halting
proof end;

theorem Th4: :: SCM_1:4
for b1 being State of SCM
for b2 being Nat st b1 . (IC ((Computation b1) . b2)) = halt SCM holds
Result b1 = (Computation b1) . b2
proof end;

theorem Th5: :: SCM_1:5
canceled;

theorem Th6: :: SCM_1:6
canceled;

theorem Th7: :: SCM_1:7
for b1, b2 being Nat holds
( IC SCM <> il. b1 & IC SCM <> dl. b1 & il. b1 <> dl. b2 ) by AMI_3:56, AMI_3:57;

E6: now
let c1 be FinSequence;
let c2 be Nat;
assume c2 < len c1 ;
then ( c2 + 1 >= 0 + 1 & c2 + 1 <= len c1 ) by NAT_1:38;
then ( c2 + 1 in dom c1 & dom c1 = Seg (len c1) ) by FINSEQ_1:def 3, FINSEQ_3:27;
hence ( c2 + 1 in dom c1 & c1 . (c2 + 1) in rng c1 ) by FUNCT_1:def 5;
end;

E7: now
let c1 be Nat;
let c2 be set ;
let c3 be FinSequence of c2;
assume c1 < len c3 ;
then ( c3 . (c1 + 1) in rng c3 & rng c3 c= c2 ) by Lemma6, FINSEQ_1:def 4;
hence c3 . (c1 + 1) in c2 ;
end;

definition
let c1 be FinSequence of the Instructions of SCM ;
let c2 be FinSequence of INT ;
let c3, c4, c5 be Nat;
mode State-consisting of c3,c4,c5,c1,c2 -> State of SCM means :Def1: :: SCM_1:def 1
( IC a6 = il. a3 & ( for b1 being Nat st b1 < len a1 holds
a6 . (il. (a4 + b1)) = a1 . (b1 + 1) ) & ( for b1 being Nat st b1 < len a2 holds
a6 . (dl. (a5 + b1)) = a2 . (b1 + 1) ) );
existence
ex b1 being State of SCM st
( IC b1 = il. c3 & ( for b2 being Nat st b2 < len c1 holds
b1 . (il. (c4 + b2)) = c1 . (b2 + 1) ) & ( for b2 being Nat st b2 < len c2 holds
b1 . (dl. (c5 + b2)) = c2 . (b2 + 1) ) )
proof end;
end;

:: deftheorem Def1 defines State-consisting SCM_1:def 1 :
for b1 being FinSequence of the Instructions of SCM
for b2 being FinSequence of INT
for b3, b4, b5 being Nat
for b6 being State of SCM holds
( b6 is State-consisting of b3,b4,b5,b1,b2 iff ( IC b6 = il. b3 & ( for b7 being Nat st b7 < len b1 holds
b6 . (il. (b4 + b7)) = b1 . (b7 + 1) ) & ( for b7 being Nat st b7 < len b2 holds
b6 . (dl. (b5 + b7)) = b2 . (b7 + 1) ) ) );

Lemma9: ( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 )
by FINSEQ_1:3;

Lemma10: ( 1 in Seg 4 & 2 in Seg 4 & 3 in Seg 4 & 4 in Seg 4 )
by FINSEQ_1:3;

Lemma11: ( 1 in Seg 5 & 2 in Seg 5 & 3 in Seg 5 & 4 in Seg 5 & 5 in Seg 5 )
by FINSEQ_1:3;

Lemma12: ( 1 in Seg 6 & 2 in Seg 6 & 3 in Seg 6 & 4 in Seg 6 & 5 in Seg 6 & 6 in Seg 6 )
by FINSEQ_1:3;

Lemma13: ( 1 in Seg 7 & 2 in Seg 7 & 3 in Seg 7 & 4 in Seg 7 & 5 in Seg 7 & 6 in Seg 7 & 7 in Seg 7 )
by FINSEQ_1:3;

Lemma14: ( 1 in Seg 8 & 2 in Seg 8 & 3 in Seg 8 & 4 in Seg 8 & 5 in Seg 8 & 6 in Seg 8 & 7 in Seg 8 & 8 in Seg 8 )
by FINSEQ_1:3;

theorem Th8: :: SCM_1:8
for b1, b2, b3, b4 being set
for b5 being FinSequence st b5 = ((<*b1*> ^ <*b2*>) ^ <*b3*>) ^ <*b4*> holds
( len b5 = 4 & b5 . 1 = b1 & b5 . 2 = b2 & b5 . 3 = b3 & b5 . 4 = b4 )
proof end;

theorem Th9: :: SCM_1:9
for b1, b2, b3, b4, b5 being set
for b6 being FinSequence st b6 = (((<*b1*> ^ <*b2*>) ^ <*b3*>) ^ <*b4*>) ^ <*b5*> holds
( len b6 = 5 & b6 . 1 = b1 & b6 . 2 = b2 & b6 . 3 = b3 & b6 . 4 = b4 & b6 . 5 = b5 )
proof end;

theorem Th10: :: SCM_1:10
for b1, b2, b3, b4, b5, b6 being set
for b7 being FinSequence st b7 = ((((<*b1*> ^ <*b2*>) ^ <*b3*>) ^ <*b4*>) ^ <*b5*>) ^ <*b6*> holds
( len b7 = 6 & b7 . 1 = b1 & b7 . 2 = b2 & b7 . 3 = b3 & b7 . 4 = b4 & b7 . 5 = b5 & b7 . 6 = b6 )
proof end;

theorem Th11: :: SCM_1:11
for b1, b2, b3, b4, b5, b6, b7 being set
for b8 being FinSequence st b8 = (((((<*b1*> ^ <*b2*>) ^ <*b3*>) ^ <*b4*>) ^ <*b5*>) ^ <*b6*>) ^ <*b7*> holds
( len b8 = 7 & b8 . 1 = b1 & b8 . 2 = b2 & b8 . 3 = b3 & b8 . 4 = b4 & b8 . 5 = b5 & b8 . 6 = b6 & b8 . 7 = b7 )
proof end;

theorem Th12: :: SCM_1:12
for b1, b2, b3, b4, b5, b6, b7, b8 being set
for b9 being FinSequence st b9 = ((((((<*b1*> ^ <*b2*>) ^ <*b3*>) ^ <*b4*>) ^ <*b5*>) ^ <*b6*>) ^ <*b7*>) ^ <*b8*> holds
( len b9 = 8 & b9 . 1 = b1 & b9 . 2 = b2 & b9 . 3 = b3 & b9 . 4 = b4 & b9 . 5 = b5 & b9 . 6 = b6 & b9 . 7 = b7 & b9 . 8 = b8 )
proof end;

theorem Th13: :: SCM_1:13
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being set
for b10 being FinSequence st b10 = (((((((<*b1*> ^ <*b2*>) ^ <*b3*>) ^ <*b4*>) ^ <*b5*>) ^ <*b6*>) ^ <*b7*>) ^ <*b8*>) ^ <*b9*> holds
( len b10 = 9 & b10 . 1 = b1 & b10 . 2 = b2 & b10 . 3 = b3 & b10 . 4 = b4 & b10 . 5 = b5 & b10 . 6 = b6 & b10 . 7 = b7 & b10 . 8 = b8 & b10 . 9 = b9 )
proof end;

theorem Th14: :: SCM_1:14
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being Instruction of SCM
for b10, b11, b12, b13 being Integer
for b14 being Nat
for b15 being State-consisting of b14,0,0,(((((((<*b1*> ^ <*b2*>) ^ <*b3*>) ^ <*b4*>) ^ <*b5*>) ^ <*b6*>) ^ <*b7*>) ^ <*b8*>) ^ <*b9*>,((<*b10*> ^ <*b11*>) ^ <*b12*>) ^ <*b13*> holds
( IC b15 = il. b14 & b15 . (il. 0) = b1 & b15 . (il. 1) = b2 & b15 . (il. 2) = b3 & b15 . (il. 3) = b4 & b15 . (il. 4) = b5 & b15 . (il. 5) = b6 & b15 . (il. 6) = b7 & b15 . (il. 7) = b8 & b15 . (il. 8) = b9 & b15 . (dl. 0) = b10 & b15 . (dl. 1) = b11 & b15 . (dl. 2) = b12 & b15 . (dl. 3) = b13 )
proof end;

theorem Th15: :: SCM_1:15
for b1, b2 being Instruction of SCM
for b3, b4 being Integer
for b5 being Nat
for b6 being State-consisting of b5,0,0,<*b1*> ^ <*b2*>,<*b3*> ^ <*b4*> holds
( IC b6 = il. b5 & b6 . (il. 0) = b1 & b6 . (il. 1) = b2 & b6 . (dl. 0) = b3 & b6 . (dl. 1) = b4 )
proof end;

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 State of c2;
assume E22: c3 is halting ;
func Complexity c3 -> Nat means :Def2: :: SCM_1:def 2
( CurInstr ((Computation a3) . a4) = halt a2 & ( for b1 being Nat st CurInstr ((Computation a3) . b1) = halt a2 holds
a4 <= b1 ) );
existence
ex b1 being Nat st
( CurInstr ((Computation c3) . b1) = halt c2 & ( for b2 being Nat st CurInstr ((Computation c3) . b2) = halt c2 holds
b1 <= b2 ) )
proof end;
uniqueness
for b1, b2 being Nat st CurInstr ((Computation c3) . b1) = halt c2 & ( for b3 being Nat st CurInstr ((Computation c3) . b3) = halt c2 holds
b1 <= b3 ) & CurInstr ((Computation c3) . b2) = halt c2 & ( for b3 being Nat st CurInstr ((Computation c3) . b3) = halt c2 holds
b2 <= b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Complexity SCM_1:def 2 :
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 State of b2 st b3 is halting holds
for b4 being Nat holds
( b4 = Complexity b3 iff ( CurInstr ((Computation b3) . b4) = halt b2 & ( for b5 being Nat st CurInstr ((Computation b3) . b5) = halt b2 holds
b4 <= b5 ) ) );

notation
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 State of c2;
synonym LifeSpan c3 for Complexity c3;
end;

theorem Th16: :: SCM_1:16
for b1 being State of SCM
for b2 being Nat holds
( b1 . (IC ((Computation b1) . b2)) <> halt SCM & b1 . (IC ((Computation b1) . (b2 + 1))) = halt SCM iff ( Complexity b1 = b2 + 1 & b1 is halting ) )
proof end;

theorem Th17: :: SCM_1:17
for b1 being State of SCM
for b2 being Nat st IC ((Computation b1) . b2) <> IC ((Computation b1) . (b2 + 1)) & b1 . (IC ((Computation b1) . (b2 + 1))) = halt SCM holds
Complexity b1 = b2 + 1
proof end;

Lemma25: for b1 being Nat holds Next (il. b1) = il. (b1 + 1)
proof end;

Lemma26: for b1 being Nat
for b2 being State of SCM holds (Computation b2) . (b1 + 1) = Exec (CurInstr ((Computation b2) . b1)),((Computation b2) . b1)
proof end;

E27: now
let c1, c2 be Nat;
let c3 be State of SCM ;
let c4, c5 be Data-Location ;
assume E28: IC ((Computation c3) . c1) = il. c2 ;
E29: ((Computation c3) . c1) . (il. c2) = c3 . (il. c2) by AMI_1:54;
set c6 = (Computation c3) . c1;
set c7 = (Computation c3) . (c1 + 1);
E30: ((Computation c3) . c1) . 0 = il. c2 by E28, Th1;
assume E31: ( c3 . (il. c2) = c4 := c5 or c3 . (il. c2) = AddTo c4,c5 or c3 . (il. c2) = SubFrom c4,c5 or c3 . (il. c2) = MultBy c4,c5 or ( c4 <> c5 & c3 . (il. c2) = Divide c4,c5 ) ) ;
thus E32: (Computation c3) . (c1 + 1) = Exec (CurInstr ((Computation c3) . c1)),((Computation c3) . c1) by Lemma26
.= Exec (c3 . (il. c2)),((Computation c3) . c1) by E29, E30, Th1 ;
thus IC ((Computation c3) . (c1 + 1)) = ((Computation c3) . (c1 + 1)) . 0 by Th1
.= Next (IC ((Computation c3) . c1)) by E31, E32, AMI_3:4, AMI_3:8, AMI_3:9, AMI_3:10, AMI_3:11, AMI_3:12
.= il. (c2 + 1) by E28, Lemma25 ;
end;

theorem Th18: :: SCM_1:18
for b1, b2 being Nat
for b3 being State of SCM
for b4, b5 being Data-Location st IC ((Computation b3) . b1) = il. b2 & b3 . (il. b2) = b4 := b5 holds
( IC ((Computation b3) . (b1 + 1)) = il. (b2 + 1) & ((Computation b3) . (b1 + 1)) . b4 = ((Computation b3) . b1) . b5 & ( for b6 being Data-Location st b6 <> b4 holds
((Computation b3) . (b1 + 1)) . b6 = ((Computation b3) . b1) . b6 ) )
proof end;

theorem Th19: :: SCM_1:19
for b1, b2 being Nat
for b3 being State of SCM
for b4, b5 being Data-Location st IC ((Computation b3) . b1) = il. b2 & b3 . (il. b2) = AddTo b4,b5 holds
( IC ((Computation b3) . (b1 + 1)) = il. (b2 + 1) & ((Computation b3) . (b1 + 1)) . b4 = (((Computation b3) . b1) . b4) + (((Computation b3) . b1) . b5) & ( for b6 being Data-Location st b6 <> b4 holds
((Computation b3) . (b1 + 1)) . b6 = ((Computation b3) . b1) . b6 ) )
proof end;

theorem Th20: :: SCM_1:20
for b1, b2 being Nat
for b3 being State of SCM
for b4, b5 being Data-Location st IC ((Computation b3) . b1) = il. b2 & b3 . (il. b2) = SubFrom b4,b5 holds
( IC ((Computation b3) . (b1 + 1)) = il. (b2 + 1) & ((Computation b3) . (b1 + 1)) . b4 = (((Computation b3) . b1) . b4) - (((Computation b3) . b1) . b5) & ( for b6 being Data-Location st b6 <> b4 holds
((Computation b3) . (b1 + 1)) . b6 = ((Computation b3) . b1) . b6 ) )
proof end;

theorem Th21: :: SCM_1:21
for b1, b2 being Nat
for b3 being State of SCM
for b4, b5 being Data-Location st IC ((Computation b3) . b1) = il. b2 & b3 . (il. b2) = MultBy b4,b5 holds
( IC ((Computation b3) . (b1 + 1)) = il. (b2 + 1) & ((Computation b3) . (b1 + 1)) . b4 = (((Computation b3) . b1) . b4) * (((Computation b3) . b1) . b5) & ( for b6 being Data-Location st b6 <> b4 holds
((Computation b3) . (b1 + 1)) . b6 = ((Computation b3) . b1) . b6 ) )
proof end;

theorem Th22: :: SCM_1:22
for b1, b2 being Nat
for b3 being State of SCM
for b4, b5 being Data-Location st IC ((Computation b3) . b1) = il. b2 & b3 . (il. b2) = Divide b4,b5 & b4 <> b5 holds
( IC ((Computation b3) . (b1 + 1)) = il. (b2 + 1) & ((Computation b3) . (b1 + 1)) . b4 = (((Computation b3) . b1) . b4) div (((Computation b3) . b1) . b5) & ((Computation b3) . (b1 + 1)) . b5 = (((Computation b3) . b1) . b4) mod (((Computation b3) . b1) . b5) & ( for b6 being Data-Location st b6 <> b4 & b6 <> b5 holds
((Computation b3) . (b1 + 1)) . b6 = ((Computation b3) . b1) . b6 ) )
proof end;

theorem Th23: :: SCM_1:23
for b1, b2 being Nat
for b3 being State of SCM
for b4 being Instruction-Location of SCM st IC ((Computation b3) . b1) = il. b2 & b3 . (il. b2) = goto b4 holds
( IC ((Computation b3) . (b1 + 1)) = b4 & ( for b5 being Data-Location holds ((Computation b3) . (b1 + 1)) . b5 = ((Computation b3) . b1) . b5 ) )
proof end;

theorem Th24: :: SCM_1:24
for b1, b2 being Nat
for b3 being State of SCM
for b4 being Data-Location
for b5 being Instruction-Location of SCM st IC ((Computation b3) . b1) = il. b2 & b3 . (il. b2) = b4 =0_goto b5 holds
( ( ((Computation b3) . b1) . b4 = 0 implies IC ((Computation b3) . (b1 + 1)) = b5 ) & ( ((Computation b3) . b1) . b4 <> 0 implies IC ((Computation b3) . (b1 + 1)) = il. (b2 + 1) ) & ( for b6 being Data-Location holds ((Computation b3) . (b1 + 1)) . b6 = ((Computation b3) . b1) . b6 ) )
proof end;

theorem Th25: :: SCM_1:25
for b1, b2 being Nat
for b3 being State of SCM
for b4 being Data-Location
for b5 being Instruction-Location of SCM st IC ((Computation b3) . b1) = il. b2 & b3 . (il. b2) = b4 >0_goto b5 holds
( ( ((Computation b3) . b1) . b4 > 0 implies IC ((Computation b3) . (b1 + 1)) = b5 ) & ( ((Computation b3) . b1) . b4 <= 0 implies IC ((Computation b3) . (b1 + 1)) = il. (b2 + 1) ) & ( for b6 being Data-Location holds ((Computation b3) . (b1 + 1)) . b6 = ((Computation b3) . b1) . b6 ) )
proof end;

theorem Th26: :: SCM_1:26
( (halt SCM ) `1 = 0 & ( for b1, b2 being Data-Location holds (b1 := b2) `1 = 1 ) & ( for b1, b2 being Data-Location holds (AddTo b1,b2) `1 = 2 ) & ( for b1, b2 being Data-Location holds (SubFrom b1,b2) `1 = 3 ) & ( for b1, b2 being Data-Location holds (MultBy b1,b2) `1 = 4 ) & ( for b1, b2 being Data-Location holds (Divide b1,b2) `1 = 5 ) & ( for b1 being Instruction-Location of SCM holds (goto b1) `1 = 6 ) & ( for b1 being Data-Location
for b2 being Instruction-Location of SCM holds (b1 =0_goto b2) `1 = 7 ) & ( for b1 being Data-Location
for b2 being Instruction-Location of SCM holds (b1 >0_goto b2) `1 = 8 ) )
proof end;

theorem Th27: :: SCM_1:27
for b1 being non empty with_non-empty_elements set
for b2 being non empty non void halting IC-Ins-separated definite AMI-Struct of b1
for b3 being State of b2
for b4 being Nat holds
( b3 is halting iff (Computation b3) . b4 is halting )
proof end;

theorem Th28: :: SCM_1:28
for b1, b2 being State of SCM
for b3, b4 being Nat st b2 = (Computation b1) . b3 & Complexity b2 = b4 & b2 is halting & 0 < b4 holds
Complexity b1 = b3 + b4
proof end;

theorem Th29: :: SCM_1:29
for b1, b2 being State of SCM
for b3 being Nat st b2 = (Computation b1) . b3 & b2 is halting holds
Result b2 = Result b1
proof end;

theorem Th30: :: SCM_1:30
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being Instruction of SCM
for b10, b11, b12, b13 being Integer
for b14 being Nat
for b15 being State of SCM st IC b15 = il. b14 & b15 . (il. 0) = b1 & b15 . (il. 1) = b2 & b15 . (il. 2) = b3 & b15 . (il. 3) = b4 & b15 . (il. 4) = b5 & b15 . (il. 5) = b6 & b15 . (il. 6) = b7 & b15 . (il. 7) = b8 & b15 . (il. 8) = b9 & b15 . (dl. 0) = b10 & b15 . (dl. 1) = b11 & b15 . (dl. 2) = b12 & b15 . (dl. 3) = b13 holds
b15 is State-consisting of b14,0,0,(((((((<*b1*> ^ <*b2*>) ^ <*b3*>) ^ <*b4*>) ^ <*b5*>) ^ <*b6*>) ^ <*b7*>) ^ <*b8*>) ^ <*b9*>,((<*b10*> ^ <*b11*>) ^ <*b12*>) ^ <*b13*>
proof end;

theorem Th31: :: SCM_1:31
for b1 being State-consisting of 0,0,0,<*(halt SCM )*>, <*> INT holds
( b1 is halting & Complexity b1 = 0 & Result b1 = b1 )
proof end;

theorem Th32: :: SCM_1:32
for b1, b2 being Integer
for b3 being State-consisting of 0,0,0,<*((dl. 0) := (dl. 1))*> ^ <*(halt SCM )*>,<*b1*> ^ <*b2*> holds
( b3 is halting & Complexity b3 = 1 & (Result b3) . (dl. 0) = b2 & ( for b4 being Data-Location st b4 <> dl. 0 holds
(Result b3) . b4 = b3 . b4 ) )
proof end;

theorem Th33: :: SCM_1:33
for b1, b2 being Integer
for b3 being State-consisting of 0,0,0,<*(AddTo (dl. 0),(dl. 1))*> ^ <*(halt SCM )*>,<*b1*> ^ <*b2*> holds
( b3 is halting & Complexity b3 = 1 & (Result b3) . (dl. 0) = b1 + b2 & ( for b4 being Data-Location st b4 <> dl. 0 holds
(Result b3) . b4 = b3 . b4 ) )
proof end;

theorem Th34: :: SCM_1:34
for b1, b2 being Integer
for b3 being State-consisting of 0,0,0,<*(SubFrom (dl. 0),(dl. 1))*> ^ <*(halt SCM )*>,<*b1*> ^ <*b2*> holds
( b3 is halting & Complexity b3 = 1 & (Result b3) . (dl. 0) = b1 - b2 & ( for b4 being Data-Location st b4 <> dl. 0 holds
(Result b3) . b4 = b3 . b4 ) )
proof end;

theorem Th35: :: SCM_1:35
for b1, b2 being Integer
for b3 being State-consisting of 0,0,0,<*(MultBy (dl. 0),(dl. 1))*> ^ <*(halt SCM )*>,<*b1*> ^ <*b2*> holds
( b3 is halting & Complexity b3 = 1 & (Result b3) . (dl. 0) = b1 * b2 & ( for b4 being Data-Location st b4 <> dl. 0 holds
(Result b3) . b4 = b3 . b4 ) )
proof end;

theorem Th36: :: SCM_1:36
for b1, b2 being Integer
for b3 being State-consisting of 0,0,0,<*(Divide (dl. 0),(dl. 1))*> ^ <*(halt SCM )*>,<*b1*> ^ <*b2*> holds
( b3 is halting & Complexity b3 = 1 & (Result b3) . (dl. 0) = b1 div b2 & (Result b3) . (dl. 1) = b1 mod b2 & ( for b4 being Data-Location st b4 <> dl. 0 & b4 <> dl. 1 holds
(Result b3) . b4 = b3 . b4 ) )
proof end;

theorem Th37: :: SCM_1:37
for b1, b2 being Integer
for b3 being State-consisting of 0,0,0,<*(goto (il. 1))*> ^ <*(halt SCM )*>,<*b1*> ^ <*b2*> holds
( b3 is halting & Complexity b3 = 1 & ( for b4 being Data-Location holds (Result b3) . b4 = b3 . b4 ) )
proof end;

theorem Th38: :: SCM_1:38
for b1, b2 being Integer
for b3 being State-consisting of 0,0,0,<*((dl. 0) =0_goto (il. 1))*> ^ <*(halt SCM )*>,<*b1*> ^ <*b2*> holds
( b3 is halting & Complexity b3 = 1 & ( for b4 being Data-Location holds (Result b3) . b4 = b3 . b4 ) )
proof end;

theorem Th39: :: SCM_1:39
for b1, b2 being Integer
for b3 being State-consisting of 0,0,0,<*((dl. 0) >0_goto (il. 1))*> ^ <*(halt SCM )*>,<*b1*> ^ <*b2*> holds
( b3 is halting & Complexity b3 = 1 & ( for b4 being Data-Location holds (Result b3) . b4 = b3 . b4 ) )
proof end;