:: AMI_3 semantic presentation

begin


registration
cluster non zero natural  ->  non zero with_zero for set ;
coherence
 for b1 being non zero Nat holds b1 is with_zero
proof
let n be non zero Nat; ::_thesis: n is with_zero
 {} in n by ORDINAL3:8;
hence  n is with_zero ; ::_thesis: verum
end;
end;


definition
func SCM  ->  strict AMI-Struct over 2 equals :: AMI_3:def 1
 AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCM-Instr,SCM-OK,SCM-VAL,SCM-Exec #);
coherence
 AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCM-Instr,SCM-OK,SCM-VAL,SCM-Exec #) is strict AMI-Struct over 2 ;
end;

:: deftheorem  defines SCM AMI_3:def_1_:_
 SCM = AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCM-Instr,SCM-OK,SCM-VAL,SCM-Exec #);

registration
cluster SCM  ->  non empty strict ;
coherence
 not SCM is empty by STRUCT_0:def_1;
end;

Lm1: the_Values_of SCM = the ValuesF of SCM * the Object-Kind of SCM
.= SCM-VAL * SCM-OK ;

registration
cluster SCM  ->  with_non-empty_values strict ;
coherence
 SCM is with_non-empty_values
proof
thus  the_Values_of SCM is non-empty ; :: according to MEMSTR_0:def_3 ::_thesis: verum
end;
end;

registration
cluster SCM  ->  IC-Ins-separated strict ;
coherence
 SCM is IC-Ins-separated
proof
 IC = NAT by AMI_2:22, FUNCT_7:def_1;
then  Values (IC ) = NAT by AMI_2:6;
hence  SCM is IC-Ins-separated by MEMSTR_0:def_6; ::_thesis: verum
end;
end;

registration
cluster Int-like for Element of the carrier of SCM;
existence
 ex b1 being Object of SCM st b1 is Int-like
proof
reconsider x = the Element of SCM-Data-Loc as Object of SCM ;
take  x ; ::_thesis: x is Int-like
thus  x is Int-like by AMI_2:def_16; ::_thesis: verum
end;
end;

definition
mode Data-Location is Int-like Object of SCM;
end;

registration
let s be State of SCM;
let d be Data-Location;
clusters . d ->  integer ;
coherence
 s . d is integer
proof
reconsider D = d as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider S = s as SCM-State by CARD_3:107;
 S . D = s . d ;
hence  s . d is integer ; ::_thesis: verum
end;
end;


definition
canceled;
let a, b be Data-Location;
funca := b ->  Instruction of SCM equals :: AMI_3:def 3
[1,{},<*a,b*>];
correctness
coherence
[1,{},<*a,b*>] is Instruction of SCM;
proof
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def_16;
 1 in {1,2,3,4,5} by ENUMSET1:def_3;
then  [1,{},<*mk,ml*>] in SCM-Instr by SCM_INST:4;
hence  [1,{},<*a,b*>] is Instruction of SCM ; ::_thesis: verum
end;
func AddTo (a,b) ->  Instruction of SCM equals :: AMI_3:def 4
[2,{},<*a,b*>];
correctness
coherence
[2,{},<*a,b*>] is Instruction of SCM;
proof
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def_16;
 2 in {1,2,3,4,5} by ENUMSET1:def_3;
then  [2,{},<*mk,ml*>] in SCM-Instr by SCM_INST:4;
hence  [2,{},<*a,b*>] is Instruction of SCM ; ::_thesis: verum
end;
func SubFrom (a,b) ->  Instruction of SCM equals :: AMI_3:def 5
[3,{},<*a,b*>];
correctness
coherence
[3,{},<*a,b*>] is Instruction of SCM;
proof
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def_16;
 3 in {1,2,3,4,5} by ENUMSET1:def_3;
then  [3,{},<*mk,ml*>] in SCM-Instr by SCM_INST:4;
hence  [3,{},<*a,b*>] is Instruction of SCM ; ::_thesis: verum
end;
func MultBy (a,b) ->  Instruction of SCM equals :: AMI_3:def 6
[4,{},<*a,b*>];
correctness
coherence
[4,{},<*a,b*>] is Instruction of SCM;
proof
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def_16;
 4 in {1,2,3,4,5} by ENUMSET1:def_3;
then  [4,{},<*mk,ml*>] in SCM-Instr by SCM_INST:4;
hence  [4,{},<*a,b*>] is Instruction of SCM ; ::_thesis: verum
end;
func Divide (a,b) ->  Instruction of SCM equals :: AMI_3:def 7
[5,{},<*a,b*>];
correctness
coherence
[5,{},<*a,b*>] is Instruction of SCM;
proof
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def_16;
 5 in {1,2,3,4,5} by ENUMSET1:def_3;
then  [5,{},<*mk,ml*>] in SCM-Instr by SCM_INST:4;
hence  [5,{},<*a,b*>] is Instruction of SCM ; ::_thesis: verum
end;
end;

:: deftheorem  AMI_3:def_2_:_
canceled;

:: deftheorem  defines := AMI_3:def_3_:_
 for a, b being Data-Location holds a := b = [1,{},<*a,b*>];

:: deftheorem  defines AddTo AMI_3:def_4_:_
 for a, b being Data-Location holds AddTo (a,b) = [2,{},<*a,b*>];

:: deftheorem  defines SubFrom AMI_3:def_5_:_
 for a, b being Data-Location holds SubFrom (a,b) = [3,{},<*a,b*>];

:: deftheorem  defines MultBy AMI_3:def_6_:_
 for a, b being Data-Location holds MultBy (a,b) = [4,{},<*a,b*>];

:: deftheorem  defines Divide AMI_3:def_7_:_
 for a, b being Data-Location holds Divide (a,b) = [5,{},<*a,b*>];

definition
let loc be Nat;
func SCM-goto loc ->  Instruction of SCM equals :: AMI_3:def 8
[6,<*loc*>,{}];
correctness
coherence
[6,<*loc*>,{}] is Instruction of SCM;
proof
 loc in NAT by ORDINAL1:def_12;
hence  [6,<*loc*>,{}] is Instruction of SCM by SCM_INST:2; ::_thesis: verum
end;
let a be Data-Location;
funca =0_goto loc ->  Instruction of SCM equals :: AMI_3:def 9
[7,<*loc*>,<*a*>];
correctness
coherence
[7,<*loc*>,<*a*>] is Instruction of SCM;
proof
reconsider a = a as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider loc = loc as Element of NAT by ORDINAL1:def_12;
 7 in {7,8} by TARSKI:def_2;
then  [7,<*loc*>,<*a*>] in SCM-Instr by SCM_INST:3;
hence  [7,<*loc*>,<*a*>] is Instruction of SCM ; ::_thesis: verum
end;
funca >0_goto loc ->  Instruction of SCM equals :: AMI_3:def 10
[8,<*loc*>,<*a*>];
correctness
coherence
[8,<*loc*>,<*a*>] is Instruction of SCM;
proof
reconsider a = a as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider loc = loc as Element of NAT by ORDINAL1:def_12;
 8 in {7,8} by TARSKI:def_2;
then  [8,<*loc*>,<*a*>] in SCM-Instr by SCM_INST:3;
hence  [8,<*loc*>,<*a*>] is Instruction of SCM ; ::_thesis: verum
end;
end;

:: deftheorem  defines SCM-goto AMI_3:def_8_:_
 for loc being Nat holds SCM-goto loc = [6,<*loc*>,{}];

:: deftheorem  defines =0_goto AMI_3:def_9_:_
 for loc being Nat
for a being Data-Location holds a =0_goto loc = [7,<*loc*>,<*a*>];

:: deftheorem  defines >0_goto AMI_3:def_10_:_
 for loc being Nat
for a being Data-Location holds a >0_goto loc = [8,<*loc*>,<*a*>];

theorem Th1: :: AMI_3:1
IC = NAT by AMI_2:22, FUNCT_7:def_1;

begin

theorem Th2: :: AMI_3:2
for a, b being Data-Location
for s being State of SCM holds
( (Exec ((a := b),s)) . (IC ) = succ (IC s) & (Exec ((a := b),s)) . a = s . b & ( for c being Data-Location st c <> a holds
(Exec ((a := b),s)) . c = s . c ) )
proof
let a, b be Data-Location; ::_thesis: for s being State of SCM holds
( (Exec ((a := b),s)) . (IC ) = succ (IC s) & (Exec ((a := b),s)) . a = s . b & ( for c being Data-Location st c <> a holds
(Exec ((a := b),s)) . c = s . c ) )
let s be State of SCM; ::_thesis: ( (Exec ((a := b),s)) . (IC ) = succ (IC s) & (Exec ((a := b),s)) . a = s . b & ( for c being Data-Location st c <> a holds
(Exec ((a := b),s)) . c = s . c ) )
reconsider S = s as SCM-State by CARD_3:107;
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = a := b as Element of SCM-Instr ;
set S1 = SCM-Chg (S,(I address_1),(S . (I address_2)));
reconsider i = 1 as Element of Segm 9 by NAT_1:44;
A1: I = [i,{},<*mk,ml*>] ;
then A2: I address_1 = mk by SCM_INST:5;
A3: I address_2 = ml by A1, SCM_INST:5;
A4: Exec ((a := b),s) = SCM-Exec-Res (I,S) by AMI_2:def_15
.= SCM-Chg ((SCM-Chg (S,(I address_1),(S . (I address_2)))),(succ (IC S))) by A1, AMI_2:def_14 ;
hence  (Exec ((a := b),s)) . (IC ) = succ (IC s) by Th1, AMI_2:11; ::_thesis: ( (Exec ((a := b),s)) . a = s . b & ( for c being Data-Location st c <> a holds
(Exec ((a := b),s)) . c = s . c ) )
thus (Exec ((a := b),s)) . a = (SCM-Chg (S,(I address_1),(S . (I address_2)))) . mk by A4, AMI_2:12
.= s . b by A2, A3, AMI_2:15 ; ::_thesis: for c being Data-Location st c <> a holds
(Exec ((a := b),s)) . c = s . c
let c be Data-Location; ::_thesis: ( c <> a implies (Exec ((a := b),s)) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def_16;
assume A5: c <> a ; ::_thesis: (Exec ((a := b),s)) . c = s . c
thus (Exec ((a := b),s)) . c = (SCM-Chg (S,(I address_1),(S . (I address_2)))) . mn by A4, AMI_2:12
.= s . c by A2, A5, AMI_2:16 ; ::_thesis: verum
end;

theorem Th3: :: AMI_3:3
for a, b being Data-Location
for s being State of SCM holds
( (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Data-Location st c <> a holds
(Exec ((AddTo (a,b)),s)) . c = s . c ) )
proof
let a, b be Data-Location; ::_thesis: for s being State of SCM holds
( (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Data-Location st c <> a holds
(Exec ((AddTo (a,b)),s)) . c = s . c ) )
let s be State of SCM; ::_thesis: ( (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Data-Location st c <> a holds
(Exec ((AddTo (a,b)),s)) . c = s . c ) )
reconsider S = s as SCM-State by CARD_3:107;
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = AddTo (a,b) as Element of SCM-Instr ;
set S1 = SCM-Chg (S,(I address_1),((S . (I address_1)) + (S . (I address_2))));
reconsider i = 2 as Element of Segm 9 by NAT_1:44;
A1: I = [i,{},<*mk,ml*>] ;
then A2: I address_1 = mk by SCM_INST:5;
A3: I address_2 = ml by A1, SCM_INST:5;
A4: Exec ((AddTo (a,b)),s) = SCM-Exec-Res (I,S) by AMI_2:def_15
.= SCM-Chg ((SCM-Chg (S,(I address_1),((S . (I address_1)) + (S . (I address_2))))),(succ (IC S))) by A1, AMI_2:def_14 ;
hence  (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) by Th1, AMI_2:11; ::_thesis: ( (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Data-Location st c <> a holds
(Exec ((AddTo (a,b)),s)) . c = s . c ) )
thus (Exec ((AddTo (a,b)),s)) . a = (SCM-Chg (S,(I address_1),((S . (I address_1)) + (S . (I address_2))))) . mk by A4, AMI_2:12
.= (s . a) + (s . b) by A2, A3, AMI_2:15 ; ::_thesis: for c being Data-Location st c <> a holds
(Exec ((AddTo (a,b)),s)) . c = s . c
let c be Data-Location; ::_thesis: ( c <> a implies (Exec ((AddTo (a,b)),s)) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def_16;
assume A5: c <> a ; ::_thesis: (Exec ((AddTo (a,b)),s)) . c = s . c
thus (Exec ((AddTo (a,b)),s)) . c = (SCM-Chg (S,(I address_1),((S . (I address_1)) + (S . (I address_2))))) . mn by A4, AMI_2:12
.= s . c by A2, A5, AMI_2:16 ; ::_thesis: verum
end;

theorem Th4: :: AMI_3:4
for a, b being Data-Location
for s being State of SCM holds
( (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Data-Location st c <> a holds
(Exec ((SubFrom (a,b)),s)) . c = s . c ) )
proof
let a, b be Data-Location; ::_thesis: for s being State of SCM holds
( (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Data-Location st c <> a holds
(Exec ((SubFrom (a,b)),s)) . c = s . c ) )
let s be State of SCM; ::_thesis: ( (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Data-Location st c <> a holds
(Exec ((SubFrom (a,b)),s)) . c = s . c ) )
reconsider S = s as SCM-State by CARD_3:107;
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = SubFrom (a,b) as Element of SCM-Instr ;
set S1 = SCM-Chg (S,(I address_1),((S . (I address_1)) - (S . (I address_2))));
reconsider i = 3 as Element of Segm 9 by NAT_1:44;
A1: I = [i,{},<*mk,ml*>] ;
then A2: I address_1 = mk by SCM_INST:5;
A3: I address_2 = ml by A1, SCM_INST:5;
A4: Exec ((SubFrom (a,b)),s) = SCM-Exec-Res (I,S) by AMI_2:def_15
.= SCM-Chg ((SCM-Chg (S,(I address_1),((S . (I address_1)) - (S . (I address_2))))),(succ (IC S))) by A1, AMI_2:def_14 ;
hence  (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) by Th1, AMI_2:11; ::_thesis: ( (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Data-Location st c <> a holds
(Exec ((SubFrom (a,b)),s)) . c = s . c ) )
thus (Exec ((SubFrom (a,b)),s)) . a = (SCM-Chg (S,(I address_1),((S . (I address_1)) - (S . (I address_2))))) . mk by A4, AMI_2:12
.= (s . a) - (s . b) by A2, A3, AMI_2:15 ; ::_thesis: for c being Data-Location st c <> a holds
(Exec ((SubFrom (a,b)),s)) . c = s . c
let c be Data-Location; ::_thesis: ( c <> a implies (Exec ((SubFrom (a,b)),s)) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def_16;
assume A5: c <> a ; ::_thesis: (Exec ((SubFrom (a,b)),s)) . c = s . c
thus (Exec ((SubFrom (a,b)),s)) . c = (SCM-Chg (S,(I address_1),((S . (I address_1)) - (S . (I address_2))))) . mn by A4, AMI_2:12
.= s . c by A2, A5, AMI_2:16 ; ::_thesis: verum
end;

theorem Th5: :: AMI_3:5
for a, b being Data-Location
for s being State of SCM holds
( (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) & ( for c being Data-Location st c <> a holds
(Exec ((MultBy (a,b)),s)) . c = s . c ) )
proof
let a, b be Data-Location; ::_thesis: for s being State of SCM holds
( (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) & ( for c being Data-Location st c <> a holds
(Exec ((MultBy (a,b)),s)) . c = s . c ) )
let s be State of SCM; ::_thesis: ( (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) & ( for c being Data-Location st c <> a holds
(Exec ((MultBy (a,b)),s)) . c = s . c ) )
reconsider S = s as SCM-State by CARD_3:107;
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = MultBy (a,b) as Element of SCM-Instr ;
set S1 = SCM-Chg (S,(I address_1),((S . (I address_1)) * (S . (I address_2))));
reconsider i = 4 as Element of Segm 9 by NAT_1:44;
A1: I = [i,{},<*mk,ml*>] ;
then A2: I address_1 = mk by SCM_INST:5;
A3: I address_2 = ml by A1, SCM_INST:5;
A4: Exec ((MultBy (a,b)),s) = SCM-Exec-Res (I,S) by AMI_2:def_15
.= SCM-Chg ((SCM-Chg (S,(I address_1),((S . (I address_1)) * (S . (I address_2))))),(succ (IC S))) by A1, AMI_2:def_14 ;
hence  (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) by Th1, AMI_2:11; ::_thesis: ( (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) & ( for c being Data-Location st c <> a holds
(Exec ((MultBy (a,b)),s)) . c = s . c ) )
thus (Exec ((MultBy (a,b)),s)) . a = (SCM-Chg (S,(I address_1),((S . (I address_1)) * (S . (I address_2))))) . mk by A4, AMI_2:12
.= (s . a) * (s . b) by A2, A3, AMI_2:15 ; ::_thesis: for c being Data-Location st c <> a holds
(Exec ((MultBy (a,b)),s)) . c = s . c
let c be Data-Location; ::_thesis: ( c <> a implies (Exec ((MultBy (a,b)),s)) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def_16;
assume A5: c <> a ; ::_thesis: (Exec ((MultBy (a,b)),s)) . c = s . c
thus (Exec ((MultBy (a,b)),s)) . c = (SCM-Chg (S,(I address_1),((S . (I address_1)) * (S . (I address_2))))) . mn by A4, AMI_2:12
.= s . c by A2, A5, AMI_2:16 ; ::_thesis: verum
end;

theorem Th6: :: AMI_3:6
for a, b being Data-Location
for s being State of SCM holds
( (Exec ((Divide (a,b)),s)) . (IC ) = succ (IC s) & ( a <> b implies (Exec ((Divide (a,b)),s)) . a = (s . a) div (s . b) ) & (Exec ((Divide (a,b)),s)) . b = (s . a) mod (s . b) & ( for c being Data-Location st c <> a & c <> b holds
(Exec ((Divide (a,b)),s)) . c = s . c ) )
proof
let a, b be Data-Location; ::_thesis: for s being State of SCM holds
( (Exec ((Divide (a,b)),s)) . (IC ) = succ (IC s) & ( a <> b implies (Exec ((Divide (a,b)),s)) . a = (s . a) div (s . b) ) & (Exec ((Divide (a,b)),s)) . b = (s . a) mod (s . b) & ( for c being Data-Location st c <> a & c <> b holds
(Exec ((Divide (a,b)),s)) . c = s . c ) )
let s be State of SCM; ::_thesis: ( (Exec ((Divide (a,b)),s)) . (IC ) = succ (IC s) & ( a <> b implies (Exec ((Divide (a,b)),s)) . a = (s . a) div (s . b) ) & (Exec ((Divide (a,b)),s)) . b = (s . a) mod (s . b) & ( for c being Data-Location st c <> a & c <> b holds
(Exec ((Divide (a,b)),s)) . c = s . c ) )
reconsider S = s as SCM-State by CARD_3:107;
reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = Divide (a,b) as Element of SCM-Instr ;
set S1 = SCM-Chg (S,(I address_1),((S . (I address_1)) div (S . (I address_2))));
set S19 = SCM-Chg ((SCM-Chg (S,(I address_1),((S . (I address_1)) div (S . (I address_2))))),(I address_2),((S . (I address_1)) mod (S . (I address_2))));
reconsider i = 5 as Element of Segm 9 by NAT_1:44;
A1: I = [i,{},<*mk,ml*>] ;
then A2: I address_1 = mk by SCM_INST:5;
A3: Exec ((Divide (a,b)),s) = SCM-Exec-Res (I,S) by AMI_2:def_15
.= SCM-Chg ((SCM-Chg ((SCM-Chg (S,(I address_1),((S . (I address_1)) div (S . (I address_2))))),(I address_2),((S . (I address_1)) mod (S . (I address_2))))),(succ (IC S))) by A1, AMI_2:def_14 ;
hence  (Exec ((Divide (a,b)),s)) . (IC ) = succ (IC s) by Th1, AMI_2:11; ::_thesis: ( ( a <> b implies (Exec ((Divide (a,b)),s)) . a = (s . a) div (s . b) ) & (Exec ((Divide (a,b)),s)) . b = (s . a) mod (s . b) & ( for c being Data-Location st c <> a & c <> b holds
(Exec ((Divide (a,b)),s)) . c = s . c ) )
A4: I address_2 = ml by A1, SCM_INST:5;
hereby  ::_thesis: ( (Exec ((Divide (a,b)),s)) . b = (s . a) mod (s . b) & ( for c being Data-Location st c <> a & c <> b holds
(Exec ((Divide (a,b)),s)) . c = s . c ) )
assume A5: a <> b ; ::_thesis: (Exec ((Divide (a,b)),s)) . a = (s . a) div (s . b)
thus (Exec ((Divide (a,b)),s)) . a = (SCM-Chg ((SCM-Chg (S,(I address_1),((S . (I address_1)) div (S . (I address_2))))),(I address_2),((S . (I address_1)) mod (S . (I address_2))))) . mk by A3, AMI_2:12
.= (SCM-Chg (S,(I address_1),((S . (I address_1)) div (S . (I address_2))))) . mk by A4, A5, AMI_2:16
.= (s . a) div (s . b) by A2, A4, AMI_2:15 ; ::_thesis: verum
end;
thus (Exec ((Divide (a,b)),s)) . b = (SCM-Chg ((SCM-Chg (S,(I address_1),((S . (I address_1)) div (S . (I address_2))))),(I address_2),((S . (I address_1)) mod (S . (I address_2))))) . ml by A3, AMI_2:12
.= (s . a) mod (s . b) by A2, A4, AMI_2:15 ; ::_thesis: for c being Data-Location st c <> a & c <> b holds
(Exec ((Divide (a,b)),s)) . c = s . c
let c be Data-Location; ::_thesis: ( c <> a & c <> b implies (Exec ((Divide (a,b)),s)) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def_16;
assume that
A6: c <> a and
A7: c <> b ; ::_thesis: (Exec ((Divide (a,b)),s)) . c = s . c
thus (Exec ((Divide (a,b)),s)) . c = (SCM-Chg ((SCM-Chg (S,(I address_1),((S . (I address_1)) div (S . (I address_2))))),(I address_2),((S . (I address_1)) mod (S . (I address_2))))) . mn by A3, AMI_2:12
.= (SCM-Chg (S,(I address_1),((S . (I address_1)) div (S . (I address_2))))) . mn by A4, A7, AMI_2:16
.= s . c by A2, A6, AMI_2:16 ; ::_thesis: verum
end;

theorem :: AMI_3:7
for c being Data-Location
for loc being Nat
for s being State of SCM holds
( (Exec ((SCM-goto loc),s)) . (IC ) = loc & (Exec ((SCM-goto loc),s)) . c = s . c )
proof
let c be Data-Location; ::_thesis: for loc being Nat
for s being State of SCM holds
( (Exec ((SCM-goto loc),s)) . (IC ) = loc & (Exec ((SCM-goto loc),s)) . c = s . c )
let loc be Nat; ::_thesis: for s being State of SCM holds
( (Exec ((SCM-goto loc),s)) . (IC ) = loc & (Exec ((SCM-goto loc),s)) . c = s . c )
let s be State of SCM; ::_thesis: ( (Exec ((SCM-goto loc),s)) . (IC ) = loc & (Exec ((SCM-goto loc),s)) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider mj = loc as Element of NAT by ORDINAL1:def_12;
reconsider I = SCM-goto loc as Element of SCM-Instr ;
reconsider S = s as SCM-State by CARD_3:107;
reconsider i = 6 as Element of Segm 9 by NAT_1:44;
A1: I = [i,<*mj*>,{}] ;
A2: Exec ((SCM-goto loc),s) = SCM-Exec-Res (I,S) by AMI_2:def_15
.= SCM-Chg (S,(I jump_address)) by A1, AMI_2:def_14 ;
 I jump_address = mj by A1, SCM_INST:6;
hence  (Exec ((SCM-goto loc),s)) . (IC ) = loc by A2, Th1, AMI_2:11; ::_thesis: (Exec ((SCM-goto loc),s)) . c = s . c
thus (Exec ((SCM-goto loc),s)) . c = S . mn by A2, AMI_2:12
.= s . c ; ::_thesis: verum
end;

theorem Th8: :: AMI_3:8
for a, c being Data-Location
for loc being Nat
for s being State of SCM holds
( ( s . a = 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = loc ) & ( s . a <> 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = succ (IC s) ) & (Exec ((a =0_goto loc),s)) . c = s . c )
proof
let a, c be Data-Location; ::_thesis: for loc being Nat
for s being State of SCM holds
( ( s . a = 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = loc ) & ( s . a <> 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = succ (IC s) ) & (Exec ((a =0_goto loc),s)) . c = s . c )
let loc be Nat; ::_thesis: for s being State of SCM holds
( ( s . a = 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = loc ) & ( s . a <> 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = succ (IC s) ) & (Exec ((a =0_goto loc),s)) . c = s . c )
let s be State of SCM; ::_thesis: ( ( s . a = 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = loc ) & ( s . a <> 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = succ (IC s) ) & (Exec ((a =0_goto loc),s)) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = a =0_goto loc as Element of SCM-Instr ;
reconsider S = s as SCM-State by CARD_3:107;
reconsider i = 7 as Element of Segm 9 by NAT_1:44;
reconsider a9 = a as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider mj = loc as Element of NAT by ORDINAL1:def_12;
A1: I = [i,<*mj*>,<*a9*>] ;
A2: Exec ((a =0_goto loc),s) = SCM-Exec-Res (I,S) by AMI_2:def_15
.= SCM-Chg (S,(IFEQ ((S . (I cond_address)),0,(I cjump_address),(succ (IC S))))) by A1, AMI_2:def_14 ;
thus  ( s . a = 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = loc ) ::_thesis: ( ( s . a <> 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = succ (IC s) ) & (Exec ((a =0_goto loc),s)) . c = s . c )
proof
assume  s . a = 0 ; ::_thesis: (Exec ((a =0_goto loc),s)) . (IC ) = loc
then A3: S . (I cond_address) = 0 by A1, SCM_INST:7;
thus (Exec ((a =0_goto loc),s)) . (IC ) = IFEQ ((S . (I cond_address)),0,(I cjump_address),(succ (IC S))) by A2, Th1, AMI_2:11
.= I cjump_address by A3, FUNCOP_1:def_8
.= loc by A1, SCM_INST:7 ; ::_thesis: verum
end;
thus  ( s . a <> 0 implies (Exec ((a =0_goto loc),s)) . (IC ) = succ (IC s) ) ::_thesis: (Exec ((a =0_goto loc),s)) . c = s . c
proof
assume  s . a <> 0 ; ::_thesis: (Exec ((a =0_goto loc),s)) . (IC ) = succ (IC s)
then A4: S . (I cond_address) <> 0 by A1, SCM_INST:7;
thus (Exec ((a =0_goto loc),s)) . (IC ) = IFEQ ((S . (I cond_address)),0,(I cjump_address),(succ (IC S))) by A2, Th1, AMI_2:11
.= succ (IC s) by A4, Th1, FUNCOP_1:def_8 ; ::_thesis: verum
end;
thus (Exec ((a =0_goto loc),s)) . c = S . mn by A2, AMI_2:12
.= s . c ; ::_thesis: verum
end;

theorem Th9: :: AMI_3:9
for a, c being Data-Location
for loc being Nat
for s being State of SCM holds
( ( s . a > 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = loc ) & ( s . a <= 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = succ (IC s) ) & (Exec ((a >0_goto loc),s)) . c = s . c )
proof
let a, c be Data-Location; ::_thesis: for loc being Nat
for s being State of SCM holds
( ( s . a > 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = loc ) & ( s . a <= 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = succ (IC s) ) & (Exec ((a >0_goto loc),s)) . c = s . c )
let loc be Nat; ::_thesis: for s being State of SCM holds
( ( s . a > 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = loc ) & ( s . a <= 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = succ (IC s) ) & (Exec ((a >0_goto loc),s)) . c = s . c )
let s be State of SCM; ::_thesis: ( ( s . a > 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = loc ) & ( s . a <= 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = succ (IC s) ) & (Exec ((a >0_goto loc),s)) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = a >0_goto loc as Element of SCM-Instr ;
reconsider S = s as SCM-State by CARD_3:107;
reconsider i = 8 as Element of Segm 9 by NAT_1:44;
reconsider a9 = a as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider mj = loc as Element of NAT by ORDINAL1:def_12;
A1: I = [i,<*mj*>,<*a9*>] ;
A2: Exec ((a >0_goto loc),s) = SCM-Exec-Res (I,S) by AMI_2:def_15
.= SCM-Chg (S,(IFGT ((S . (I cond_address)),0,(I cjump_address),(succ (IC S))))) by A1, AMI_2:def_14 ;
thus  ( s . a > 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = loc ) ::_thesis: ( ( s . a <= 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = succ (IC s) ) & (Exec ((a >0_goto loc),s)) . c = s . c )
proof
assume  s . a > 0 ; ::_thesis: (Exec ((a >0_goto loc),s)) . (IC ) = loc
then A3: S . (I cond_address) > 0 by A1, SCM_INST:7;
thus (Exec ((a >0_goto loc),s)) . (IC ) = IFGT ((S . (I cond_address)),0,(I cjump_address),(succ (IC S))) by A2, Th1, AMI_2:11
.= I cjump_address by A3, XXREAL_0:def_11
.= loc by A1, SCM_INST:7 ; ::_thesis: verum
end;
thus  ( s . a <= 0 implies (Exec ((a >0_goto loc),s)) . (IC ) = succ (IC s) ) ::_thesis: (Exec ((a >0_goto loc),s)) . c = s . c
proof
assume  s . a <= 0 ; ::_thesis: (Exec ((a >0_goto loc),s)) . (IC ) = succ (IC s)
then A4: S . (I cond_address) <= 0 by A1, SCM_INST:7;
thus (Exec ((a >0_goto loc),s)) . (IC ) = IFGT ((S . (I cond_address)),0,(I cjump_address),(succ (IC S))) by A2, Th1, AMI_2:11
.= succ (IC s) by A4, Th1, XXREAL_0:def_11 ; ::_thesis: verum
end;
thus (Exec ((a >0_goto loc),s)) . c = S . mn by A2, AMI_2:12
.= s . c ; ::_thesis: verum
end;

           Lm2:  for I being Instruction of SCM st ex s being State of SCM st (Exec (I,s)) . (IC ) = succ (IC s) holds
not I is halting
proof
let I be Instruction of SCM; ::_thesis: ( ex s being State of SCM st (Exec (I,s)) . (IC ) = succ (IC s) implies not I is halting )
given s being State of SCM such that A1: (Exec (I,s)) . (IC ) = succ (IC s) ; ::_thesis: not I is halting
assume  I is halting ; ::_thesis: contradiction
then  (Exec (I,s)) . (IC ) = s . NAT by Th1, EXTPRO_1:def_3;
hence  contradiction by A1, Th1; ::_thesis: verum
 IC s = s . NAT by AMI_2:22, FUNCT_7:def_1;
then reconsider w = s . NAT as Element of NAT ;
end;

Lm3:  for I being Instruction of SCM st I = [0,{},{}] holds
I is halting
proof
let I be Instruction of SCM; ::_thesis: ( I = [0,{},{}] implies I is halting )
assume A1: I = [0,{},{}] ; ::_thesis: I is halting
then A2: I `3_3 = {} by RECDEF_2:def_3;
then A3: ( ( for mk, ml being Element of SCM-Data-Loc holds not I = [1,{},<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not I = [2,{},<*mk,ml*>] ) ) by RECDEF_2:def_3;
A4: ( ( for mk being Element of NAT
for ml being Element of SCM-Data-Loc holds not I = [7,<*mk*>,<*ml*>] ) & ( for mk being Element of NAT
for ml being Element of SCM-Data-Loc holds not I = [8,<*mk*>,<*ml*>] ) ) by A2, RECDEF_2:def_3;
 I `2_3 = {} by A1, RECDEF_2:def_2;
then A5: ( ( for mk, ml being Element of SCM-Data-Loc holds not I = [5,{},<*mk,ml*>] ) & ( for mk being Element of NAT holds not I = [6,<*mk*>,{}] ) ) by A2, RECDEF_2:def_2, RECDEF_2:def_3;
reconsider L = I as Element of SCM-Instr ;
let s be State of SCM; :: according to EXTPRO_1:def_3 ::_thesis: Exec (I,s) = s
reconsider t = s as SCM-State by CARD_3:107;
A6: ( ( for mk, ml being Element of SCM-Data-Loc holds not I = [3,{},<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not I = [4,{},<*mk,ml*>] ) ) by A2, RECDEF_2:def_3;
thus  Exec (I,s) = SCM-Exec-Res (L,t) by AMI_2:def_15
.= s by A3, A6, A5, A4, AMI_2:def_14 ; ::_thesis: verum
end;

Lm4:  for a, b being Data-Location holds not a := b is halting
proof
let a, b be Data-Location; ::_thesis: not a := b is halting
set s = the State of SCM;
 (Exec ((a := b), the State of SCM)) . (IC ) = succ (IC the State of SCM) by Th2;
hence  not a := b is halting by Lm2; ::_thesis: verum
end;

Lm5:  for a, b being Data-Location holds not AddTo (a,b) is halting
proof
let a, b be Data-Location; ::_thesis: not AddTo (a,b) is halting
set s = the State of SCM;
 (Exec ((AddTo (a,b)), the State of SCM)) . (IC ) = succ (IC the State of SCM) by Th3;
hence  not AddTo (a,b) is halting by Lm2; ::_thesis: verum
end;

Lm6:  for a, b being Data-Location holds not SubFrom (a,b) is halting
proof
let a, b be Data-Location; ::_thesis: not SubFrom (a,b) is halting
set s = the State of SCM;
 (Exec ((SubFrom (a,b)), the State of SCM)) . (IC ) = succ (IC the State of SCM) by Th4;
hence  not SubFrom (a,b) is halting by Lm2; ::_thesis: verum
end;

Lm7:  for a, b being Data-Location holds not MultBy (a,b) is halting
proof
let a, b be Data-Location; ::_thesis: not MultBy (a,b) is halting
set s = the State of SCM;
 (Exec ((MultBy (a,b)), the State of SCM)) . (IC ) = succ (IC the State of SCM) by Th5;
hence  not MultBy (a,b) is halting by Lm2; ::_thesis: verum
end;

Lm8:  for a, b being Data-Location holds not Divide (a,b) is halting
proof
let a, b be Data-Location; ::_thesis: not Divide (a,b) is halting
set s = the State of SCM;
 (Exec ((Divide (a,b)), the State of SCM)) . (IC ) = succ (IC the State of SCM) by Th6;
hence  not Divide (a,b) is halting by Lm2; ::_thesis: verum
end;

Lm9:  for loc being Nat holds not SCM-goto loc is halting
proof
let loc be Nat; ::_thesis: not SCM-goto loc is halting
set f = the_Values_of SCM;
set s = the SCM-State;
assume A1: SCM-goto loc is halting ; ::_thesis: contradiction
reconsider a3 = loc as Element of NAT by ORDINAL1:def_12;
reconsider V = SCM-goto loc as Element of SCM-Instr ;
set t = the SCM-State +* (NAT .--> (succ a3));
A2: dom the SCM-State = the carrier of SCM by AMI_2:28;
A3: dom (NAT .--> (succ a3)) = {NAT} by FUNCOP_1:13;
then  NAT in dom (NAT .--> (succ a3)) by TARSKI:def_1;
then A4: ( the SCM-State +* (NAT .--> (succ a3))) . NAT = (NAT .--> (succ a3)) . NAT by FUNCT_4:13
.= succ a3 by FUNCOP_1:72 ;
A5: for x being set st x in dom (the_Values_of SCM) holds
( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x
proof
let x be set ; ::_thesis: ( x in dom (the_Values_of SCM) implies ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x )
assume A6: x in dom (the_Values_of SCM) ; ::_thesis: ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x
percases ( x = NAT or x <> NAT ) ;
supposeA7: x = NAT ; ::_thesis: ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x
then  (the_Values_of SCM) . x = NAT by AMI_2:6;
hence  ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x by A4, A7; ::_thesis: verum
end;
suppose x <> NAT ; ::_thesis: ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x
then  not x in dom (NAT .--> (succ a3)) by A3, TARSKI:def_1;
then  ( the SCM-State +* (NAT .--> (succ a3))) . x = the SCM-State . x by FUNCT_4:11;
hence  ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x by A6, CARD_3:9; ::_thesis: verum
end;
end;
end;
A8: {NAT} c= SCM-Memory by AMI_2:22, ZFMISC_1:31;
A9: dom ( the SCM-State +* (NAT .--> (succ a3))) = (dom the SCM-State) \/ (dom (NAT .--> (succ a3))) by FUNCT_4:def_1
.= SCM-Memory \/ (dom (NAT .--> (succ a3))) by A2
.= SCM-Memory \/ {NAT} by FUNCOP_1:13
.= SCM-Memory by A8, XBOOLE_1:12 ;
 dom (the_Values_of SCM) = SCM-Memory by AMI_2:27;
then reconsider t = the SCM-State +* (NAT .--> (succ a3)) as State of SCM by A9, A5, FUNCT_1:def_14, PARTFUN1:def_2, RELAT_1:def_18;
reconsider w = t as SCM-State by CARD_3:107;
 dom (NAT .--> loc) = {NAT} by FUNCOP_1:13;
then  NAT in dom (NAT .--> loc) by TARSKI:def_1;
then A10: (w +* (NAT .--> loc)) . NAT = (NAT .--> loc) . NAT by FUNCT_4:13
.= loc by FUNCOP_1:72 ;
 6 is Element of Segm 9 by NAT_1:44;
then w +* (NAT .--> loc) = SCM-Chg (w,(V jump_address)) by SCM_INST:6
.= SCM-Exec-Res (V,w) by AMI_2:def_14
.= Exec ((SCM-goto loc),t) by AMI_2:def_15
.= t by A1, EXTPRO_1:def_3 ;
hence  contradiction by A4, A10; ::_thesis: verum
end;

Lm10:  for a being Data-Location
for loc being Nat holds not a =0_goto loc is halting
proof
let a be Data-Location; ::_thesis: for loc being Nat holds not a =0_goto loc is halting
let loc be Nat; ::_thesis: not a =0_goto loc is halting
set f = the_Values_of SCM;
set s = the SCM-State;
reconsider V = a =0_goto loc as Element of SCM-Instr ;
reconsider a3 = loc as Element of NAT by ORDINAL1:def_12;
set t = the SCM-State +* (NAT .--> (succ a3));
A1: {NAT} c= SCM-Memory by AMI_2:22, ZFMISC_1:31;
A2: dom the SCM-State = the carrier of SCM by AMI_2:28;
A3: dom ( the SCM-State +* (NAT .--> (succ a3))) = (dom the SCM-State) \/ (dom (NAT .--> (succ a3))) by FUNCT_4:def_1
.= SCM-Memory \/ (dom (NAT .--> (succ a3))) by A2
.= SCM-Memory \/ {NAT} by FUNCOP_1:13
.= SCM-Memory by A1, XBOOLE_1:12 ;
A4: 7 is Element of Segm 9 by NAT_1:44;
A5: dom (NAT .--> (succ a3)) = {NAT} by FUNCOP_1:13;
then  NAT in dom (NAT .--> (succ a3)) by TARSKI:def_1;
then A6: ( the SCM-State +* (NAT .--> (succ a3))) . NAT = (NAT .--> (succ a3)) . NAT by FUNCT_4:13
.= succ a3 by FUNCOP_1:72 ;
A7: for x being set st x in dom (the_Values_of SCM) holds
( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x
proof
let x be set ; ::_thesis: ( x in dom (the_Values_of SCM) implies ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x )
assume A8: x in dom (the_Values_of SCM) ; ::_thesis: ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x
percases ( x = NAT or x <> NAT ) ;
supposeA9: x = NAT ; ::_thesis: ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x
then  (the_Values_of SCM) . x = NAT by AMI_2:6;
hence  ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x by A6, A9; ::_thesis: verum
end;
suppose x <> NAT ; ::_thesis: ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x
then  not x in dom (NAT .--> (succ a3)) by A5, TARSKI:def_1;
then  ( the SCM-State +* (NAT .--> (succ a3))) . x = the SCM-State . x by FUNCT_4:11;
hence  ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x by A8, CARD_3:9; ::_thesis: verum
end;
end;
end;
 dom (the_Values_of SCM) = SCM-Memory by AMI_2:27;
then reconsider t = the SCM-State +* (NAT .--> (succ a3)) as State of SCM by A3, A7, FUNCT_1:def_14, PARTFUN1:def_2, RELAT_1:def_18;
reconsider w = t as SCM-State by CARD_3:107;
 dom (NAT .--> loc) = {NAT} by FUNCOP_1:13;
then  NAT in dom (NAT .--> loc) by TARSKI:def_1;
then A10: (w +* (NAT .--> loc)) . NAT = (NAT .--> loc) . NAT by FUNCT_4:13
.= loc by FUNCOP_1:72 ;
assume A11: a =0_goto loc is halting ; ::_thesis: contradiction
A12: a is Element of SCM-Data-Loc by AMI_2:def_16;
percases ( w . (V cond_address) <> 0 or w . (V cond_address) = 0 ) ;
supposeA13: w . (V cond_address) <> 0 ; ::_thesis: contradiction
 IC w = w . NAT ;
then reconsider e = w . NAT as Element of NAT ;
 ( IC t = IC w & t . a <> 0 ) by A4, A12, A13, AMI_2:22, FUNCT_7:def_1, SCM_INST:7;
then A14: (Exec ((a =0_goto loc),t)) . (IC ) = succ e by Th8;
 (Exec ((a =0_goto loc),t)) . (IC ) = w . NAT by A11, Th1, EXTPRO_1:def_3;
hence  contradiction by A14; ::_thesis: verum
end;
suppose w . (V cond_address) = 0 ; ::_thesis: contradiction
then  IFEQ ((w . (V cond_address)),0,(V cjump_address),(succ (IC w))) = V cjump_address by FUNCOP_1:def_8;
then w +* (NAT .--> loc) = SCM-Chg (w,(IFEQ ((w . (V cond_address)),0,(V cjump_address),(succ (IC w))))) by A4, A12, SCM_INST:7
.= SCM-Exec-Res (V,w) by A12, AMI_2:def_14
.= Exec ((a =0_goto loc),t) by AMI_2:def_15
.= t by A11, EXTPRO_1:def_3 ;
hence  contradiction by A6, A10; ::_thesis: verum
end;
end;
end;

Lm11:  for a being Data-Location
for loc being Nat holds not a >0_goto loc is halting
proof
let a be Data-Location; ::_thesis: for loc being Nat holds not a >0_goto loc is halting
let loc be Nat; ::_thesis: not a >0_goto loc is halting
set f = the_Values_of SCM;
set s = the SCM-State;
reconsider V = a >0_goto loc as Element of SCM-Instr ;
reconsider a3 = loc as Element of NAT by ORDINAL1:def_12;
set t = the SCM-State +* (NAT .--> (succ a3));
A1: {NAT} c= SCM-Memory by AMI_2:22, ZFMISC_1:31;
A2: dom the SCM-State = the carrier of SCM by AMI_2:28;
A3: dom ( the SCM-State +* (NAT .--> (succ a3))) = (dom the SCM-State) \/ (dom (NAT .--> (succ a3))) by FUNCT_4:def_1
.= SCM-Memory \/ (dom (NAT .--> (succ a3))) by A2
.= SCM-Memory \/ {NAT} by FUNCOP_1:13
.= SCM-Memory by A1, XBOOLE_1:12 ;
A4: 8 is Element of Segm 9 by NAT_1:44;
A5: dom (NAT .--> (succ a3)) = {NAT} by FUNCOP_1:13;
then  NAT in dom (NAT .--> (succ a3)) by TARSKI:def_1;
then A6: ( the SCM-State +* (NAT .--> (succ a3))) . NAT = (NAT .--> (succ a3)) . NAT by FUNCT_4:13
.= succ a3 by FUNCOP_1:72 ;
A7: for x being set st x in dom (the_Values_of SCM) holds
( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x
proof
let x be set ; ::_thesis: ( x in dom (the_Values_of SCM) implies ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x )
assume A8: x in dom (the_Values_of SCM) ; ::_thesis: ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x
percases ( x = NAT or x <> NAT ) ;
supposeA9: x = NAT ; ::_thesis: ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x
then  (the_Values_of SCM) . x = NAT by AMI_2:6;
hence  ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x by A6, A9; ::_thesis: verum
end;
suppose x <> NAT ; ::_thesis: ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x
then  not x in dom (NAT .--> (succ a3)) by A5, TARSKI:def_1;
then  ( the SCM-State +* (NAT .--> (succ a3))) . x = the SCM-State . x by FUNCT_4:11;
hence  ( the SCM-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM) . x by A8, CARD_3:9; ::_thesis: verum
end;
end;
end;
 dom (the_Values_of SCM) = SCM-Memory by AMI_2:27;
then reconsider t = the SCM-State +* (NAT .--> (succ a3)) as State of SCM by A3, A7, FUNCT_1:def_14, PARTFUN1:def_2, RELAT_1:def_18;
reconsider w = t as SCM-State by CARD_3:107;
 dom (NAT .--> loc) = {NAT} by FUNCOP_1:13;
then  NAT in dom (NAT .--> loc) by TARSKI:def_1;
then A10: (w +* (NAT .--> loc)) . NAT = (NAT .--> loc) . NAT by FUNCT_4:13
.= loc by FUNCOP_1:72 ;
assume A11: a >0_goto loc is halting ; ::_thesis: contradiction
A12: a is Element of SCM-Data-Loc by AMI_2:def_16;
percases ( w . (V cond_address) <= 0 or w . (V cond_address) > 0 ) ;
supposeA13: w . (V cond_address) <= 0 ; ::_thesis: contradiction
 IC w = w . NAT ;
then reconsider e = w . NAT as Element of NAT ;
 ( IC t = IC w & t . a <= 0 ) by A4, A12, A13, AMI_2:22, FUNCT_7:def_1, SCM_INST:7;
then A14: (Exec ((a >0_goto loc),t)) . (IC ) = succ e by Th9;
 (Exec ((a >0_goto loc),t)) . (IC ) = w . NAT by A11, Th1, EXTPRO_1:def_3;
hence  contradiction by A14; ::_thesis: verum
end;
suppose w . (V cond_address) > 0 ; ::_thesis: contradiction
then  IFGT ((w . (V cond_address)),0,(V cjump_address),(succ (IC w))) = V cjump_address by XXREAL_0:def_11;
then w +* (NAT .--> loc) = SCM-Chg (w,(IFGT ((w . (V cond_address)),0,(V cjump_address),(succ (IC w))))) by A4, A12, SCM_INST:7
.= SCM-Exec-Res (V,w) by A12, AMI_2:def_14
.= Exec ((a >0_goto loc),t) by AMI_2:def_15
.= t by A11, EXTPRO_1:def_3 ;
hence  contradiction by A6, A10; ::_thesis: verum
end;
end;
end;

Lm12:  for I being set holds
( I is Instruction of SCM iff ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) )
proof
let I be set ; ::_thesis: ( I is Instruction of SCM iff ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) )
thus  ( not I is Instruction of SCM or I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) ::_thesis: ( ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) implies I is Instruction of SCM )
proof
assume  I is Instruction of SCM ; ::_thesis: ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc )
then  ( I in ({[SCM-Halt,{},{}]} \/  {  [Y,<*a3*>,{}] where Y is Element of Segm 9, a3 is Element of NAT : Y = 6  }  ) \/  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  or I in  {  [T,{},<*c2,c3*>] where T is Element of Segm 9, c2, c3 is Element of SCM-Data-Loc : T in {1,2,3,4,5}  }  ) by XBOOLE_0:def_3;
then A1: ( I in {[SCM-Halt,{},{}]} \/  {  [Y,<*a3*>,{}] where Y is Element of Segm 9, a3 is Element of NAT : Y = 6  }  or I in  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  or I in  {  [T,{},<*c2,c3*>] where T is Element of Segm 9, c2, c3 is Element of SCM-Data-Loc : T in {1,2,3,4,5}  }  ) by XBOOLE_0:def_3;
percases ( I in {[SCM-Halt,{},{}]} or I in  {  [Y,<*a3*>,{}] where Y is Element of Segm 9, a3 is Element of NAT : Y = 6  }  or I in  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  or I in  {  [T,{},<*c2,c3*>] where T is Element of Segm 9, c2, c3 is Element of SCM-Data-Loc : T in {1,2,3,4,5}  }  ) by A1, XBOOLE_0:def_3;
suppose I in {[SCM-Halt,{},{}]} ; ::_thesis: ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc )
hence  ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) by TARSKI:def_1; ::_thesis: verum
end;
suppose I in  {  [Y,<*a3*>,{}] where Y is Element of Segm 9, a3 is Element of NAT : Y = 6  }  ; ::_thesis: ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc )
then consider Y being Element of Segm 9, a3 being Element of NAT  such that
A2: ( I = [Y,<*a3*>,{}] & Y = 6 ) ;
 I = SCM-goto a3 by A2;
hence  ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) ; ::_thesis: verum
end;
suppose I in  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  ; ::_thesis: ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc )
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of SCM-Data-Loc  such that
A3: ( I = [K,<*a1*>,<*b1*>] & K in {7,8} ) ;
reconsider a = b1 as Data-Location by AMI_2:def_16;
reconsider loc = a1 as Element of NAT ;
 ( I = a =0_goto a1 or I = a >0_goto a1 ) by A3, TARSKI:def_2;
hence  ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) ; ::_thesis: verum
end;
suppose I in  {  [T,{},<*c2,c3*>] where T is Element of Segm 9, c2, c3 is Element of SCM-Data-Loc : T in {1,2,3,4,5}  }  ; ::_thesis: ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc )
then consider T being Element of Segm 9, c2, c3 being Element of SCM-Data-Loc  such that
A4: ( I = [T,{},<*c2,c3*>] & T in {1,2,3,4,5} ) ;
reconsider a = c2, b = c3 as Data-Location by AMI_2:def_16;
 ( I = a := b or I = AddTo (a,b) or I = SubFrom (a,b) or I = MultBy (a,b) or I = Divide (a,b) ) by A4, ENUMSET1:def_3;
hence  ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) ; ::_thesis: verum
end;
end;
end;
thus  ( ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) implies I is Instruction of SCM ) by SCM_INST:1; ::_thesis: verum
end;

Lm13:  for W being Instruction of SCM st W is halting holds
W = [0,{},{}]
proof
set I = [0,{},{}];
let W be Instruction of SCM; ::_thesis: ( W is halting implies W = [0,{},{}] )
assume A1: W is halting ; ::_thesis: W = [0,{},{}]
assume A2: [0,{},{}] <> W ; ::_thesis: contradiction
percases ( W = [0,{},{}] or ex a, b being Data-Location st W = a := b or ex a, b being Data-Location st W = AddTo (a,b) or ex a, b being Data-Location st W = SubFrom (a,b) or ex a, b being Data-Location st W = MultBy (a,b) or ex a, b being Data-Location st W = Divide (a,b) or ex loc being Nat st W = SCM-goto loc or ex a being Data-Location ex loc being Nat st W = a =0_goto loc or ex a being Data-Location ex loc being Nat st W = a >0_goto loc ) by Lm12;
suppose W = [0,{},{}] ; ::_thesis: contradiction
hence  contradiction by A2; ::_thesis: verum
end;
suppose ex a, b being Data-Location st W = a := b ; ::_thesis: contradiction
hence  contradiction by A1, Lm4; ::_thesis: verum
end;
suppose ex a, b being Data-Location st W = AddTo (a,b) ; ::_thesis: contradiction
hence  contradiction by A1, Lm5; ::_thesis: verum
end;
suppose ex a, b being Data-Location st W = SubFrom (a,b) ; ::_thesis: contradiction
hence  contradiction by A1, Lm6; ::_thesis: verum
end;
suppose ex a, b being Data-Location st W = MultBy (a,b) ; ::_thesis: contradiction
hence  contradiction by A1, Lm7; ::_thesis: verum
end;
suppose ex a, b being Data-Location st W = Divide (a,b) ; ::_thesis: contradiction
hence  contradiction by A1, Lm8; ::_thesis: verum
end;
suppose ex loc being Nat st W = SCM-goto loc ; ::_thesis: contradiction
hence  contradiction by A1, Lm9; ::_thesis: verum
end;
suppose ex a being Data-Location ex loc being Nat st W = a =0_goto loc ; ::_thesis: contradiction
hence  contradiction by A1, Lm10; ::_thesis: verum
end;
suppose ex a being Data-Location ex loc being Nat st W = a >0_goto loc ; ::_thesis: contradiction
hence  contradiction by A1, Lm11; ::_thesis: verum
end;
end;
end;

registration
cluster SCM  ->  strict halting ;
coherence
 SCM is halting
proof
thus  halt SCM is halting by Lm3; :: according to EXTPRO_1:def_4 ::_thesis: verum
end;
end;

begin

definition
let k be Nat;
func dl. k ->  Data-Location equals :: AMI_3:def 11
[1,k];
coherence
 [1,k] is Data-Location
proof
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 1 in {1} by TARSKI:def_1;
then  [1,k] in SCM-Data-Loc by ZFMISC_1:87;
hence  [1,k] is Data-Location by AMI_2:def_16; ::_thesis: verum
end;
end;

:: deftheorem  defines dl. AMI_3:def_11_:_
 for k being Nat holds dl. k = [1,k];


theorem :: AMI_3:10
for i, j being Nat st i <> j holds
dl. i <> dl. j by XTUPLE_0:1;

theorem Th11: :: AMI_3:11
for l being Data-Location holds Values l = INT
proof
let l be Data-Location; ::_thesis: Values l = INT
 l in SCM-Data-Loc by AMI_2:def_16;
hence  Values l = INT by AMI_2:7; ::_thesis: verum
end;

definition
let la be Data-Location;
let a be Integer;
:: original: .-->
redefine funcla .--> a ->  PartState of SCM;
coherence
 la .--> a is PartState of SCM
proof
A1: ( a is Element of INT & Values la = INT ) by Th11, INT_1:def_2;
then reconsider a = a as Element of (the_Values_of SCM) . la ;
 la .--> a is PartState of SCM by A1;
hence  la .--> a is PartState of SCM ; ::_thesis: verum
end;
end;

definition
let la, lb be Data-Location;
let a, b be Integer;
:: original: -->
redefine func(la,lb) --> (a,b) ->  PartState of SCM;
coherence
 (la,lb) --> (a,b) is PartState of SCM
proof
A1: ( a is Element of INT & b is Element of INT ) by INT_1:def_2;
A2: ( Values la = INT & Values lb = INT ) by Th11;
then reconsider a = a as Element of Values la by A1;
reconsider b = b as Element of Values lb by A1, A2;
 (la,lb) --> (a,b) is PartState of SCM ;
hence  (la,lb) --> (a,b) is PartState of SCM ; ::_thesis: verum
end;
end;

theorem :: AMI_3:12
for i, j being Nat holds dl. i <> j ;

theorem :: AMI_3:13
for i being Nat holds
( IC <> dl. i & IC <> i )
proof
let i be Nat; ::_thesis: ( IC <> dl. i & IC <> i )
thus  IC <> dl. i by Th1; ::_thesis: IC <> i
assume  IC = i ; ::_thesis: contradiction
then  IC in NAT by ORDINAL1:def_12;
hence  contradiction by Th1; ::_thesis: verum
end;

begin

theorem :: AMI_3:14
for I being Instruction of SCM st ex s being State of SCM st (Exec (I,s)) . (IC ) = succ (IC s) holds
not I is halting by Lm2;

theorem :: AMI_3:15
for I being Instruction of SCM st I = [0,{},{}] holds
I is halting by Lm3;

theorem :: AMI_3:16
for a, b being Data-Location holds not a := b is halting by Lm4;

theorem :: AMI_3:17
for a, b being Data-Location holds not AddTo (a,b) is halting by Lm5;

theorem :: AMI_3:18
for a, b being Data-Location holds not SubFrom (a,b) is halting by Lm6;

theorem :: AMI_3:19
for a, b being Data-Location holds not MultBy (a,b) is halting by Lm7;

theorem :: AMI_3:20
for a, b being Data-Location holds not Divide (a,b) is halting by Lm8;

theorem :: AMI_3:21
for loc being Nat holds not SCM-goto loc is halting by Lm9;

theorem :: AMI_3:22
for a being Data-Location
for loc being Nat holds not a =0_goto loc is halting by Lm10;

theorem :: AMI_3:23
for a being Data-Location
for loc being Nat holds not a >0_goto loc is halting by Lm11;

theorem :: AMI_3:24
for I being set holds
( I is Instruction of SCM iff ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) ) by Lm12;

theorem :: AMI_3:25
for I being Instruction of SCM st I is halting holds
I = halt SCM by Lm13;

theorem :: AMI_3:26
halt SCM = [0,{},{}] ;

theorem Th27: :: AMI_3:27
Data-Locations = SCM-Data-Loc
proof
 SCM-Data-Loc misses {NAT} by AMI_2:20, ZFMISC_1:50;
then A1: SCM-Data-Loc misses {NAT} ;
thus  Data-Locations = ({NAT} \/ SCM-Data-Loc) \ {NAT} by AMI_2:22, FUNCT_7:def_1
.= (SCM-Data-Loc \/ {NAT}) \ {NAT}
.= SCM-Data-Loc \ {NAT} by XBOOLE_1:40
.= SCM-Data-Loc by A1, XBOOLE_1:83 ; ::_thesis: verum
end;

theorem :: AMI_3:28
for d being Data-Location holds d in Data-Locations by Th27, AMI_2:def_16;

theorem :: AMI_3:29
for s being SCM-State holds s is State of SCM by Lm1;

theorem :: AMI_3:30
for l being Element of SCM-Instr holds InsCode l <= 8 by SCM_INST:10;