:: SCMFSA6C semantic presentation
begin
set SA0 = Start-At (0,SCM+FSA);
theorem :: SCMFSA6C:1
for a being Int-Location
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being keeping_0 parahalting Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds (IExec ((I ";" J),P,s)) . a = (IExec (J,P,(IExec (I,P,s)))) . a
proof
let a be Int-Location; ::_thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being keeping_0 parahalting Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds (IExec ((I ";" J),P,s)) . a = (IExec (J,P,(IExec (I,P,s)))) . a
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being keeping_0 parahalting Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds (IExec ((I ";" J),P,s)) . a = (IExec (J,P,(IExec (I,P,s)))) . a
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being keeping_0 parahalting Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds (IExec ((I ";" J),P,s)) . a = (IExec (J,P,(IExec (I,P,s)))) . a
let I be keeping_0 parahalting Program of SCM+FSA; ::_thesis: for J being parahalting Program of SCM+FSA holds (IExec ((I ";" J),P,s)) . a = (IExec (J,P,(IExec (I,P,s)))) . a
let J be parahalting Program of SCM+FSA; ::_thesis: (IExec ((I ";" J),P,s)) . a = (IExec (J,P,(IExec (I,P,s)))) . a
A1: not a in dom (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA)) by SCMFSA_2:102;
IExec ((I ";" J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I)) by SCMFSA6B:20;
hence (IExec ((I ";" J),P,s)) . a = (IExec (J,P,(IExec (I,P,s)))) . a by A1, FUNCT_4:11; ::_thesis: verum
end;
theorem :: SCMFSA6C:2
for f being FinSeq-Location
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being keeping_0 parahalting Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds (IExec ((I ";" J),P,s)) . f = (IExec (J,P,(IExec (I,P,s)))) . f
proof
let f be FinSeq-Location ; ::_thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being keeping_0 parahalting Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds (IExec ((I ";" J),P,s)) . f = (IExec (J,P,(IExec (I,P,s)))) . f
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being keeping_0 parahalting Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds (IExec ((I ";" J),P,s)) . f = (IExec (J,P,(IExec (I,P,s)))) . f
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being keeping_0 parahalting Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds (IExec ((I ";" J),P,s)) . f = (IExec (J,P,(IExec (I,P,s)))) . f
let I be keeping_0 parahalting Program of SCM+FSA; ::_thesis: for J being parahalting Program of SCM+FSA holds (IExec ((I ";" J),P,s)) . f = (IExec (J,P,(IExec (I,P,s)))) . f
let J be parahalting Program of SCM+FSA; ::_thesis: (IExec ((I ";" J),P,s)) . f = (IExec (J,P,(IExec (I,P,s)))) . f
A1: not f in dom (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA)) by SCMFSA_2:103;
IExec ((I ";" J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I)) by SCMFSA6B:20;
hence (IExec ((I ";" J),P,s)) . f = (IExec (J,P,(IExec (I,P,s)))) . f by A1, FUNCT_4:11; ::_thesis: verum
end;
begin
definition
let i be Instruction of SCM+FSA;
attri is parahalting means :Def1: :: SCMFSA6C:def 1
Macro i is parahalting ;
attri is keeping_0 means :Def2: :: SCMFSA6C:def 2
Macro i is keeping_0 ;
end;
:: deftheorem Def1 defines parahalting SCMFSA6C:def_1_:_
for i being Instruction of SCM+FSA holds
( i is parahalting iff Macro i is parahalting );
:: deftheorem Def2 defines keeping_0 SCMFSA6C:def_2_:_
for i being Instruction of SCM+FSA holds
( i is keeping_0 iff Macro i is keeping_0 );
Lm1: Macro (halt SCM+FSA) is parahalting
proof
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_11 ::_thesis: for b1 being set holds
( not Macro (halt SCM+FSA) c= b1 or b1 halts_on s )
set m = Macro (halt SCM+FSA);
set m1 = Macro (halt SCM+FSA);
A1: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (halt SCM+FSA) c= P or P halts_on s )
assume A2: Macro (halt SCM+FSA) c= P ; ::_thesis: P halts_on s
A3: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
take 0 ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,0)) in dom P & CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA )
A4: dom P = NAT by PARTFUN1:def_2;
thus IC (Comput (P,s,0)) in dom P by A4; ::_thesis: CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA
dom (Macro (halt SCM+FSA)) = {0,1} by COMPOS_1:61;
then A5: 0 in dom (Macro (halt SCM+FSA)) by TARSKI:def_2;
CurInstr (P,(Comput (P,s,0))) = CurInstr (P,s)
.= P . (IC s) by A4, PARTFUN1:def_6
.= P . (IC (Start-At (0,SCM+FSA))) by A1, A3, GRFUNC_1:2
.= P . 0 by FUNCOP_1:72
.= (Macro (halt SCM+FSA)) . 0 by A2, A5, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:58 ;
hence CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA ; ::_thesis: verum
end;
Lm2: Macro (halt SCM+FSA) is keeping_0
proof
set Mi = Macro (halt SCM+FSA);
let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def_4 ::_thesis: for b1 being set holds
( not Macro (halt SCM+FSA) c= b1 or for b2 being Element of NAT holds (Comput (b1,s,b2)) . (intloc 0) = s . (intloc 0) )
A1: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (halt SCM+FSA) c= P or for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) )
assume A2: Macro (halt SCM+FSA) c= P ; ::_thesis: for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A3: P /. (IC s) = P . (IC s) by PBOOLE:143;
A4: 0 in dom (Macro (halt SCM+FSA)) by COMPOS_1:60;
CurInstr (P,(Comput (P,s,0))) = P . 0 by A1, A3, MEMSTR_0:39
.= (Macro (halt SCM+FSA)) . 0 by A2, A4, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:58 ;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by EXTPRO_1:5, NAT_1:2; ::_thesis: verum
end;
registration
cluster halt SCM+FSA -> parahalting keeping_0 ;
coherence
( halt SCM+FSA is keeping_0 & halt SCM+FSA is parahalting )
proof
thus ( Macro (halt SCM+FSA) is keeping_0 & Macro (halt SCM+FSA) is parahalting ) by Lm1, Lm2; :: according to SCMFSA6C:def_1,SCMFSA6C:def_2 ::_thesis: verum
end;
end;
registration
cluster with_explicit_jumps IC-relocable parahalting keeping_0 for Element of the InstructionsF of SCM+FSA;
existence
ex b1 being Instruction of SCM+FSA st
( b1 is keeping_0 & b1 is parahalting )
proof
take halt SCM+FSA ; ::_thesis: ( halt SCM+FSA is keeping_0 & halt SCM+FSA is parahalting )
thus ( halt SCM+FSA is keeping_0 & halt SCM+FSA is parahalting ) ; ::_thesis: verum
end;
end;
registration
let i be parahalting Instruction of SCM+FSA;
cluster Macro i -> parahalting ;
coherence
Macro i is parahalting by Def1;
end;
registration
let i be keeping_0 Instruction of SCM+FSA;
cluster Macro i -> keeping_0 ;
coherence
Macro i is keeping_0 by Def2;
end;
registration
let a, b be Int-Location;
clustera := b -> parahalting ;
coherence
a := b is parahalting
proof
set Ma = Macro (a := b);
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_11,SCMFSA6C:def_1 ::_thesis: for b1 being set holds
( not Macro (a := b) c= b1 or b1 halts_on s )
A1: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (a := b) c= P or P halts_on s )
assume A2: Macro (a := b) c= P ; ::_thesis: P halts_on s
take 1 ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,1)) in dom P & CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA )
A3: dom P = NAT by PARTFUN1:def_2;
thus IC (Comput (P,s,1)) in dom P by A3; ::_thesis: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A4: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A5: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A4, A1, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
then A6: IC (Exec ((a := b),s)) = succ 0 by SCMFSA_2:63
.= 0 + 1 ;
A7: 1 in dom (Macro (a := b)) by COMPOS_1:60;
A8: 0 in dom (Macro (a := b)) by COMPOS_1:60;
A9: P . 0 = (Macro (a := b)) . 0 by A2, A8, GRFUNC_1:2
.= a := b by COMPOS_1:58 ;
A10: P . 1 = (Macro (a := b)) . 1 by A2, A7, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:59 ;
Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec ((a := b),s) by A5, A3, A9, PARTFUN1:def_6 ;
hence CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A6, A3, A10, PARTFUN1:def_6; ::_thesis: verum
end;
cluster AddTo (a,b) -> parahalting ;
coherence
AddTo (a,b) is parahalting
proof
set Ma = Macro (AddTo (a,b));
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_11,SCMFSA6C:def_1 ::_thesis: for b1 being set holds
( not Macro (AddTo (a,b)) c= b1 or b1 halts_on s )
A11: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (AddTo (a,b)) c= P or P halts_on s )
assume A12: Macro (AddTo (a,b)) c= P ; ::_thesis: P halts_on s
take 1 ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,1)) in dom P & CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA )
A13: dom P = NAT by PARTFUN1:def_2;
thus IC (Comput (P,s,1)) in dom P by A13; ::_thesis: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A14: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A15: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A14, A11, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
then A16: IC (Exec ((AddTo (a,b)),s)) = succ 0 by SCMFSA_2:64
.= 0 + 1 ;
A17: 1 in dom (Macro (AddTo (a,b))) by COMPOS_1:60;
A18: 0 in dom (Macro (AddTo (a,b))) by COMPOS_1:60;
A19: P . 0 = (Macro (AddTo (a,b))) . 0 by A12, A18, GRFUNC_1:2
.= AddTo (a,b) by COMPOS_1:58 ;
A20: P . 1 = (Macro (AddTo (a,b))) . 1 by A12, A17, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:59 ;
Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec ((AddTo (a,b)),s) by A15, A13, A19, PARTFUN1:def_6 ;
hence CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A16, A13, A20, PARTFUN1:def_6; ::_thesis: verum
end;
cluster SubFrom (a,b) -> parahalting ;
coherence
SubFrom (a,b) is parahalting
proof
set Ma = Macro (SubFrom (a,b));
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_11,SCMFSA6C:def_1 ::_thesis: for b1 being set holds
( not Macro (SubFrom (a,b)) c= b1 or b1 halts_on s )
A21: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (SubFrom (a,b)) c= P or P halts_on s )
assume A22: Macro (SubFrom (a,b)) c= P ; ::_thesis: P halts_on s
take 1 ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,1)) in dom P & CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA )
A23: dom P = NAT by PARTFUN1:def_2;
thus IC (Comput (P,s,1)) in dom P by A23; ::_thesis: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A24: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A25: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A24, A21, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
then A26: IC (Exec ((SubFrom (a,b)),s)) = succ 0 by SCMFSA_2:65
.= 0 + 1 ;
A27: 1 in dom (Macro (SubFrom (a,b))) by COMPOS_1:60;
A28: 0 in dom (Macro (SubFrom (a,b))) by COMPOS_1:60;
A29: P . 0 = (Macro (SubFrom (a,b))) . 0 by A22, A28, GRFUNC_1:2
.= SubFrom (a,b) by COMPOS_1:58 ;
A30: P . 1 = (Macro (SubFrom (a,b))) . 1 by A22, A27, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:59 ;
Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec ((SubFrom (a,b)),s) by A25, A23, A29, PARTFUN1:def_6 ;
hence CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A26, A23, A30, PARTFUN1:def_6; ::_thesis: verum
end;
cluster MultBy (a,b) -> parahalting ;
coherence
MultBy (a,b) is parahalting
proof
set Ma = Macro (MultBy (a,b));
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_11,SCMFSA6C:def_1 ::_thesis: for b1 being set holds
( not Macro (MultBy (a,b)) c= b1 or b1 halts_on s )
A31: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (MultBy (a,b)) c= P or P halts_on s )
assume A32: Macro (MultBy (a,b)) c= P ; ::_thesis: P halts_on s
take 1 ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,1)) in dom P & CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA )
A33: dom P = NAT by PARTFUN1:def_2;
thus IC (Comput (P,s,1)) in dom P by A33; ::_thesis: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A34: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A35: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A34, A31, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
then A36: IC (Exec ((MultBy (a,b)),s)) = succ 0 by SCMFSA_2:66
.= 0 + 1 ;
A37: 1 in dom (Macro (MultBy (a,b))) by COMPOS_1:60;
A38: 0 in dom (Macro (MultBy (a,b))) by COMPOS_1:60;
A39: P . 0 = (Macro (MultBy (a,b))) . 0 by A32, A38, GRFUNC_1:2
.= MultBy (a,b) by COMPOS_1:58 ;
A40: P . 1 = (Macro (MultBy (a,b))) . 1 by A32, A37, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:59 ;
Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec ((MultBy (a,b)),s) by A35, A33, A39, PARTFUN1:def_6 ;
hence CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A36, A33, A40, PARTFUN1:def_6; ::_thesis: verum
end;
cluster Divide (a,b) -> parahalting ;
coherence
Divide (a,b) is parahalting
proof
set Ma = Macro (Divide (a,b));
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_11,SCMFSA6C:def_1 ::_thesis: for b1 being set holds
( not Macro (Divide (a,b)) c= b1 or b1 halts_on s )
A41: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (Divide (a,b)) c= P or P halts_on s )
assume A42: Macro (Divide (a,b)) c= P ; ::_thesis: P halts_on s
take 1 ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,1)) in dom P & CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA )
A43: dom P = NAT by PARTFUN1:def_2;
thus IC (Comput (P,s,1)) in dom P by A43; ::_thesis: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A44: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A45: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A44, A41, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
then A46: IC (Exec ((Divide (a,b)),s)) = succ 0 by SCMFSA_2:67
.= 0 + 1 ;
A47: 1 in dom (Macro (Divide (a,b))) by COMPOS_1:60;
A48: 0 in dom (Macro (Divide (a,b))) by COMPOS_1:60;
A49: P . 0 = (Macro (Divide (a,b))) . 0 by A42, A48, GRFUNC_1:2
.= Divide (a,b) by COMPOS_1:58 ;
A50: P . 1 = (Macro (Divide (a,b))) . 1 by A42, A47, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:59 ;
Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec ((Divide (a,b)),s) by A45, A43, A49, PARTFUN1:def_6 ;
hence CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A46, A43, A50, PARTFUN1:def_6; ::_thesis: verum
end;
let f be FinSeq-Location ;
clusterb := (f,a) -> parahalting ;
coherence
b := (f,a) is parahalting
proof
set Ma = Macro (b := (f,a));
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_11,SCMFSA6C:def_1 ::_thesis: for b1 being set holds
( not Macro (b := (f,a)) c= b1 or b1 halts_on s )
A51: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (b := (f,a)) c= P or P halts_on s )
assume A52: Macro (b := (f,a)) c= P ; ::_thesis: P halts_on s
take 1 ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,1)) in dom P & CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA )
A53: dom P = NAT by PARTFUN1:def_2;
thus IC (Comput (P,s,1)) in dom P by A53; ::_thesis: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A54: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A55: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A54, A51, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
then A56: IC (Exec ((b := (f,a)),s)) = succ 0 by SCMFSA_2:72
.= 0 + 1 ;
A57: 1 in dom (Macro (b := (f,a))) by COMPOS_1:60;
A58: 0 in dom (Macro (b := (f,a))) by COMPOS_1:60;
A59: P . 0 = (Macro (b := (f,a))) . 0 by A52, A58, GRFUNC_1:2
.= b := (f,a) by COMPOS_1:58 ;
A60: P . 1 = (Macro (b := (f,a))) . 1 by A52, A57, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:59 ;
Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec ((b := (f,a)),s) by A55, A53, A59, PARTFUN1:def_6 ;
hence CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A56, A53, A60, PARTFUN1:def_6; ::_thesis: verum
end;
cluster(f,a) := b -> parahalting keeping_0 ;
coherence
( (f,a) := b is parahalting & (f,a) := b is keeping_0 )
proof
thus (f,a) := b is parahalting ::_thesis: (f,a) := b is keeping_0
proof
set Ma = Macro ((f,a) := b);
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_11,SCMFSA6C:def_1 ::_thesis: for b1 being set holds
( not Macro ((f,a) := b) c= b1 or b1 halts_on s )
A61: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro ((f,a) := b) c= P or P halts_on s )
assume A62: Macro ((f,a) := b) c= P ; ::_thesis: P halts_on s
take 1 ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,1)) in dom P & CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA )
A63: dom P = NAT by PARTFUN1:def_2;
thus IC (Comput (P,s,1)) in dom P by A63; ::_thesis: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A64: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A65: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A64, A61, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
then A66: IC (Exec (((f,a) := b),s)) = succ 0 by SCMFSA_2:73
.= 0 + 1 ;
A67: 1 in dom (Macro ((f,a) := b)) by COMPOS_1:60;
A68: 0 in dom (Macro ((f,a) := b)) by COMPOS_1:60;
A69: P . 0 = (Macro ((f,a) := b)) . 0 by A62, A68, GRFUNC_1:2
.= (f,a) := b by COMPOS_1:58 ;
A70: P . 1 = (Macro ((f,a) := b)) . 1 by A62, A67, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:59 ;
Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec (((f,a) := b),s) by A65, A63, A69, PARTFUN1:def_6 ;
hence CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A66, A63, A70, PARTFUN1:def_6; ::_thesis: verum
end;
thus (f,a) := b is keeping_0 ::_thesis: verum
proof
set Ma = Macro ((f,a) := b);
let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def_4,SCMFSA6C:def_2 ::_thesis: for b1 being set holds
( not Macro ((f,a) := b) c= b1 or for b2 being Element of NAT holds (Comput (b1,s,b2)) . (intloc 0) = s . (intloc 0) )
A71: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro ((f,a) := b) c= P or for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) )
assume A72: Macro ((f,a) := b) c= P ; ::_thesis: for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A73: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A74: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A73, A71, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
0 in dom (Macro ((f,a) := b)) by COMPOS_1:60;
then A75: (Macro ((f,a) := b)) . 0 = P . 0 by A72, GRFUNC_1:2;
A76: P /. (IC s) = P . (IC s) by PBOOLE:143;
A77: Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec (((f,a) := b),s) by A74, A75, A76, COMPOS_1:58 ;
1 in dom (Macro ((f,a) := b)) by COMPOS_1:60;
then (Macro ((f,a) := b)) . 1 = P . 1 by A72, GRFUNC_1:2;
then A78: P . 1 = halt SCM+FSA by COMPOS_1:59;
IC (Exec (((f,a) := b),s)) = succ 0 by A74, SCMFSA_2:73
.= 0 + 1 ;
then A79: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A78, A77, PBOOLE:143;
percases ( k = 0 or 1 <= k ) by NAT_1:14;
suppose k = 0 ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by EXTPRO_1:2; ::_thesis: verum
end;
supposeA80: 1 <= k ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
(Comput (P,s,1)) . (intloc 0) = s . (intloc 0) by A77, SCMFSA_2:73;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A79, A80, EXTPRO_1:5; ::_thesis: verum
end;
end;
end;
end;
end;
registration
let a be Int-Location;
let f be FinSeq-Location ;
clustera :=len f -> parahalting ;
coherence
a :=len f is parahalting
proof
set Ma = Macro (a :=len f);
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_11,SCMFSA6C:def_1 ::_thesis: for b1 being set holds
( not Macro (a :=len f) c= b1 or b1 halts_on s )
A1: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (a :=len f) c= P or P halts_on s )
assume A2: Macro (a :=len f) c= P ; ::_thesis: P halts_on s
take 1 ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,1)) in dom P & CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA )
A3: dom P = NAT by PARTFUN1:def_2;
thus IC (Comput (P,s,1)) in dom P by A3; ::_thesis: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A4: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A5: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A4, A1, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
then A6: IC (Exec ((a :=len f),s)) = succ 0 by SCMFSA_2:74
.= 0 + 1 ;
A7: 1 in dom (Macro (a :=len f)) by COMPOS_1:60;
A8: 0 in dom (Macro (a :=len f)) by COMPOS_1:60;
A9: P . 0 = (Macro (a :=len f)) . 0 by A2, A8, GRFUNC_1:2
.= a :=len f by COMPOS_1:58 ;
A10: P . 1 = (Macro (a :=len f)) . 1 by A2, A7, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:59 ;
Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec ((a :=len f),s) by A5, A3, A9, PARTFUN1:def_6 ;
hence CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A6, A3, A10, PARTFUN1:def_6; ::_thesis: verum
end;
clusterf :=<0,...,0> a -> parahalting keeping_0 ;
coherence
( f :=<0,...,0> a is parahalting & f :=<0,...,0> a is keeping_0 )
proof
thus f :=<0,...,0> a is parahalting ::_thesis: f :=<0,...,0> a is keeping_0
proof
set Ma = Macro (f :=<0,...,0> a);
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_11,SCMFSA6C:def_1 ::_thesis: for b1 being set holds
( not Macro (f :=<0,...,0> a) c= b1 or b1 halts_on s )
A11: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (f :=<0,...,0> a) c= P or P halts_on s )
assume A12: Macro (f :=<0,...,0> a) c= P ; ::_thesis: P halts_on s
take 1 ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,1)) in dom P & CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA )
A13: dom P = NAT by PARTFUN1:def_2;
thus IC (Comput (P,s,1)) in dom P by A13; ::_thesis: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A14: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A15: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A14, A11, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
then A16: IC (Exec ((f :=<0,...,0> a),s)) = succ 0 by SCMFSA_2:75
.= 0 + 1 ;
A17: 1 in dom (Macro (f :=<0,...,0> a)) by COMPOS_1:60;
A18: 0 in dom (Macro (f :=<0,...,0> a)) by COMPOS_1:60;
A19: P . 0 = (Macro (f :=<0,...,0> a)) . 0 by A12, A18, GRFUNC_1:2
.= f :=<0,...,0> a by COMPOS_1:58 ;
A20: P . 1 = (Macro (f :=<0,...,0> a)) . 1 by A12, A17, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:59 ;
Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec ((f :=<0,...,0> a),s) by A15, A13, A19, PARTFUN1:def_6 ;
hence CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A16, A13, A20, PARTFUN1:def_6; ::_thesis: verum
end;
thus f :=<0,...,0> a is keeping_0 ::_thesis: verum
proof
set Ma = Macro (f :=<0,...,0> a);
let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def_4,SCMFSA6C:def_2 ::_thesis: for b1 being set holds
( not Macro (f :=<0,...,0> a) c= b1 or for b2 being Element of NAT holds (Comput (b1,s,b2)) . (intloc 0) = s . (intloc 0) )
A21: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (f :=<0,...,0> a) c= P or for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) )
assume A22: Macro (f :=<0,...,0> a) c= P ; ::_thesis: for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A23: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A24: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A23, A21, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
0 in dom (Macro (f :=<0,...,0> a)) by COMPOS_1:60;
then A25: (Macro (f :=<0,...,0> a)) . 0 = P . 0 by A22, GRFUNC_1:2;
A26: P /. (IC s) = P . (IC s) by PBOOLE:143;
A27: Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec ((f :=<0,...,0> a),s) by A24, A25, A26, COMPOS_1:58 ;
1 in dom (Macro (f :=<0,...,0> a)) by COMPOS_1:60;
then (Macro (f :=<0,...,0> a)) . 1 = P . 1 by A22, GRFUNC_1:2;
then A28: P . 1 = halt SCM+FSA by COMPOS_1:59;
IC (Exec ((f :=<0,...,0> a),s)) = succ 0 by A24, SCMFSA_2:75
.= 0 + 1 ;
then A29: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A28, A27, PBOOLE:143;
percases ( k = 0 or 1 <= k ) by NAT_1:14;
suppose k = 0 ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by EXTPRO_1:2; ::_thesis: verum
end;
supposeA30: 1 <= k ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
(Comput (P,s,1)) . (intloc 0) = s . (intloc 0) by A27, SCMFSA_2:75;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A29, A30, EXTPRO_1:5; ::_thesis: verum
end;
end;
end;
end;
end;
registration
let a be read-write Int-Location;
let b be Int-Location;
clustera := b -> keeping_0 ;
coherence
a := b is keeping_0
proof
set Ma = Macro (a := b);
let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def_4,SCMFSA6C:def_2 ::_thesis: for b1 being set holds
( not Macro (a := b) c= b1 or for b2 being Element of NAT holds (Comput (b1,s,b2)) . (intloc 0) = s . (intloc 0) )
A1: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (a := b) c= P or for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) )
assume A2: Macro (a := b) c= P ; ::_thesis: for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A3: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A4: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A3, A1, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
0 in dom (Macro (a := b)) by COMPOS_1:60;
then A5: (Macro (a := b)) . 0 = P . 0 by A2, GRFUNC_1:2;
A6: P /. (IC s) = P . (IC s) by PBOOLE:143;
A7: Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec ((a := b),s) by A4, A5, A6, COMPOS_1:58 ;
1 in dom (Macro (a := b)) by COMPOS_1:60;
then (Macro (a := b)) . 1 = P . 1 by A2, GRFUNC_1:2;
then A8: P . 1 = halt SCM+FSA by COMPOS_1:59;
IC (Exec ((a := b),s)) = succ 0 by A4, SCMFSA_2:63
.= 0 + 1 ;
then A9: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A8, A7, PBOOLE:143;
percases ( k = 0 or 1 <= k ) by NAT_1:14;
suppose k = 0 ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by EXTPRO_1:2; ::_thesis: verum
end;
supposeA10: 1 <= k ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
(Comput (P,s,1)) . (intloc 0) = s . (intloc 0) by A7, SCMFSA_2:63;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A9, A10, EXTPRO_1:5; ::_thesis: verum
end;
end;
end;
cluster AddTo (a,b) -> keeping_0 ;
coherence
AddTo (a,b) is keeping_0
proof
set Ma = Macro (AddTo (a,b));
let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def_4,SCMFSA6C:def_2 ::_thesis: for b1 being set holds
( not Macro (AddTo (a,b)) c= b1 or for b2 being Element of NAT holds (Comput (b1,s,b2)) . (intloc 0) = s . (intloc 0) )
A11: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (AddTo (a,b)) c= P or for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) )
assume A12: Macro (AddTo (a,b)) c= P ; ::_thesis: for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A13: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A14: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A13, A11, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
0 in dom (Macro (AddTo (a,b))) by COMPOS_1:60;
then A15: (Macro (AddTo (a,b))) . 0 = P . 0 by A12, GRFUNC_1:2;
A16: P /. (IC s) = P . (IC s) by PBOOLE:143;
A17: Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec ((AddTo (a,b)),s) by A14, A15, A16, COMPOS_1:58 ;
1 in dom (Macro (AddTo (a,b))) by COMPOS_1:60;
then (Macro (AddTo (a,b))) . 1 = P . 1 by A12, GRFUNC_1:2;
then A18: P . 1 = halt SCM+FSA by COMPOS_1:59;
IC (Exec ((AddTo (a,b)),s)) = succ 0 by A14, SCMFSA_2:64
.= 0 + 1 ;
then A19: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A18, A17, PBOOLE:143;
percases ( k = 0 or 1 <= k ) by NAT_1:14;
suppose k = 0 ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by EXTPRO_1:2; ::_thesis: verum
end;
supposeA20: 1 <= k ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
(Comput (P,s,1)) . (intloc 0) = s . (intloc 0) by A17, SCMFSA_2:64;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A19, A20, EXTPRO_1:5; ::_thesis: verum
end;
end;
end;
cluster SubFrom (a,b) -> keeping_0 ;
coherence
SubFrom (a,b) is keeping_0
proof
set Ma = Macro (SubFrom (a,b));
let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def_4,SCMFSA6C:def_2 ::_thesis: for b1 being set holds
( not Macro (SubFrom (a,b)) c= b1 or for b2 being Element of NAT holds (Comput (b1,s,b2)) . (intloc 0) = s . (intloc 0) )
A21: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (SubFrom (a,b)) c= P or for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) )
assume A22: Macro (SubFrom (a,b)) c= P ; ::_thesis: for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A23: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A24: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A23, A21, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
0 in dom (Macro (SubFrom (a,b))) by COMPOS_1:60;
then A25: (Macro (SubFrom (a,b))) . 0 = P . 0 by A22, GRFUNC_1:2;
A26: P /. (IC s) = P . (IC s) by PBOOLE:143;
A27: Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec ((SubFrom (a,b)),s) by A24, A25, A26, COMPOS_1:58 ;
1 in dom (Macro (SubFrom (a,b))) by COMPOS_1:60;
then (Macro (SubFrom (a,b))) . 1 = P . 1 by A22, GRFUNC_1:2;
then A28: P . 1 = halt SCM+FSA by COMPOS_1:59;
IC (Exec ((SubFrom (a,b)),s)) = succ 0 by A24, SCMFSA_2:65
.= 0 + 1 ;
then A29: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A28, A27, PBOOLE:143;
percases ( k = 0 or 1 <= k ) by NAT_1:14;
suppose k = 0 ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by EXTPRO_1:2; ::_thesis: verum
end;
supposeA30: 1 <= k ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
(Comput (P,s,1)) . (intloc 0) = s . (intloc 0) by A27, SCMFSA_2:65;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A29, A30, EXTPRO_1:5; ::_thesis: verum
end;
end;
end;
cluster MultBy (a,b) -> keeping_0 ;
coherence
MultBy (a,b) is keeping_0
proof
set Ma = Macro (MultBy (a,b));
let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def_4,SCMFSA6C:def_2 ::_thesis: for b1 being set holds
( not Macro (MultBy (a,b)) c= b1 or for b2 being Element of NAT holds (Comput (b1,s,b2)) . (intloc 0) = s . (intloc 0) )
A31: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (MultBy (a,b)) c= P or for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) )
assume A32: Macro (MultBy (a,b)) c= P ; ::_thesis: for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A33: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A34: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A33, A31, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
0 in dom (Macro (MultBy (a,b))) by COMPOS_1:60;
then A35: (Macro (MultBy (a,b))) . 0 = P . 0 by A32, GRFUNC_1:2;
A36: P /. (IC s) = P . (IC s) by PBOOLE:143;
A37: Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec ((MultBy (a,b)),s) by A34, A35, A36, COMPOS_1:58 ;
1 in dom (Macro (MultBy (a,b))) by COMPOS_1:60;
then (Macro (MultBy (a,b))) . 1 = P . 1 by A32, GRFUNC_1:2;
then A38: P . 1 = halt SCM+FSA by COMPOS_1:59;
IC (Exec ((MultBy (a,b)),s)) = succ 0 by A34, SCMFSA_2:66
.= 0 + 1 ;
then A39: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A38, A37, PBOOLE:143;
percases ( k = 0 or 1 <= k ) by NAT_1:14;
suppose k = 0 ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by EXTPRO_1:2; ::_thesis: verum
end;
supposeA40: 1 <= k ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
(Comput (P,s,1)) . (intloc 0) = s . (intloc 0) by A37, SCMFSA_2:66;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A39, A40, EXTPRO_1:5; ::_thesis: verum
end;
end;
end;
end;
registration
let a, b be read-write Int-Location;
cluster Divide (a,b) -> keeping_0 ;
coherence
Divide (a,b) is keeping_0
proof
set Ma = Macro (Divide (a,b));
let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def_4,SCMFSA6C:def_2 ::_thesis: for b1 being set holds
( not Macro (Divide (a,b)) c= b1 or for b2 being Element of NAT holds (Comput (b1,s,b2)) . (intloc 0) = s . (intloc 0) )
A1: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (Divide (a,b)) c= P or for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) )
assume A2: Macro (Divide (a,b)) c= P ; ::_thesis: for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A3: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A4: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A3, A1, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
0 in dom (Macro (Divide (a,b))) by COMPOS_1:60;
then A5: (Macro (Divide (a,b))) . 0 = P . 0 by A2, GRFUNC_1:2;
A6: P /. (IC s) = P . (IC s) by PBOOLE:143;
A7: Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec ((Divide (a,b)),s) by A4, A5, A6, COMPOS_1:58 ;
1 in dom (Macro (Divide (a,b))) by COMPOS_1:60;
then (Macro (Divide (a,b))) . 1 = P . 1 by A2, GRFUNC_1:2;
then A8: P . 1 = halt SCM+FSA by COMPOS_1:59;
IC (Exec ((Divide (a,b)),s)) = succ 0 by A4, SCMFSA_2:67
.= 0 + 1 ;
then A9: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A8, A7, PBOOLE:143;
percases ( k = 0 or 1 <= k ) by NAT_1:14;
suppose k = 0 ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by EXTPRO_1:2; ::_thesis: verum
end;
supposeA10: 1 <= k ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
(Comput (P,s,1)) . (intloc 0) = s . (intloc 0) by A7, SCMFSA_2:67;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A9, A10, EXTPRO_1:5; ::_thesis: verum
end;
end;
end;
end;
registration
let a be Int-Location;
let f be FinSeq-Location ;
let b be read-write Int-Location;
clusterb := (f,a) -> keeping_0 ;
coherence
b := (f,a) is keeping_0
proof
set Ma = Macro (b := (f,a));
let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def_4,SCMFSA6C:def_2 ::_thesis: for b1 being set holds
( not Macro (b := (f,a)) c= b1 or for b2 being Element of NAT holds (Comput (b1,s,b2)) . (intloc 0) = s . (intloc 0) )
A1: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (b := (f,a)) c= P or for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) )
assume A2: Macro (b := (f,a)) c= P ; ::_thesis: for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A3: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A4: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A3, A1, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
0 in dom (Macro (b := (f,a))) by COMPOS_1:60;
then A5: (Macro (b := (f,a))) . 0 = P . 0 by A2, GRFUNC_1:2;
A6: P /. (IC s) = P . (IC s) by PBOOLE:143;
A7: Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec ((b := (f,a)),s) by A4, A5, A6, COMPOS_1:58 ;
1 in dom (Macro (b := (f,a))) by COMPOS_1:60;
then (Macro (b := (f,a))) . 1 = P . 1 by A2, GRFUNC_1:2;
then A8: P . 1 = halt SCM+FSA by COMPOS_1:59;
IC (Exec ((b := (f,a)),s)) = succ 0 by A4, SCMFSA_2:72
.= 0 + 1 ;
then A9: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A8, A7, PBOOLE:143;
percases ( k = 0 or 1 <= k ) by NAT_1:14;
suppose k = 0 ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by EXTPRO_1:2; ::_thesis: verum
end;
supposeA10: 1 <= k ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
(Comput (P,s,1)) . (intloc 0) = s . (intloc 0) by A7, SCMFSA_2:72;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A9, A10, EXTPRO_1:5; ::_thesis: verum
end;
end;
end;
end;
registration
let f be FinSeq-Location ;
let b be read-write Int-Location;
clusterb :=len f -> keeping_0 ;
coherence
b :=len f is keeping_0
proof
set Ma = Macro (b :=len f);
let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def_4,SCMFSA6C:def_2 ::_thesis: for b1 being set holds
( not Macro (b :=len f) c= b1 or for b2 being Element of NAT holds (Comput (b1,s,b2)) . (intloc 0) = s . (intloc 0) )
A1: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (b :=len f) c= P or for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) )
assume A2: Macro (b :=len f) c= P ; ::_thesis: for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A3: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A4: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A3, A1, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
0 in dom (Macro (b :=len f)) by COMPOS_1:60;
then A5: (Macro (b :=len f)) . 0 = P . 0 by A2, GRFUNC_1:2;
A6: P /. (IC s) = P . (IC s) by PBOOLE:143;
A7: Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s)
.= Exec ((b :=len f),s) by A4, A5, A6, COMPOS_1:58 ;
1 in dom (Macro (b :=len f)) by COMPOS_1:60;
then (Macro (b :=len f)) . 1 = P . 1 by A2, GRFUNC_1:2;
then A8: P . 1 = halt SCM+FSA by COMPOS_1:59;
IC (Exec ((b :=len f),s)) = succ 0 by A4, SCMFSA_2:74
.= 0 + 1 ;
then A9: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A8, A7, PBOOLE:143;
percases ( k = 0 or 1 <= k ) by NAT_1:14;
suppose k = 0 ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by EXTPRO_1:2; ::_thesis: verum
end;
supposeA10: 1 <= k ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
(Comput (P,s,1)) . (intloc 0) = s . (intloc 0) by A7, SCMFSA_2:74;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A9, A10, EXTPRO_1:5; ::_thesis: verum
end;
end;
end;
end;
registration
let i be parahalting Instruction of SCM+FSA;
let J be parahalting Program of SCM+FSA;
clusteri ";" J -> parahalting ;
coherence
i ";" J is parahalting ;
end;
registration
let I be parahalting Program of SCM+FSA;
let j be parahalting Instruction of SCM+FSA;
clusterI ";" j -> parahalting ;
coherence
I ";" j is parahalting ;
end;
registration
let i, j be parahalting Instruction of SCM+FSA;
clusteri ";" j -> parahalting ;
coherence
i ";" j is parahalting ;
end;
registration
let i be keeping_0 Instruction of SCM+FSA;
let J be keeping_0 Program of SCM+FSA;
clusteri ";" J -> keeping_0 ;
coherence
i ";" J is keeping_0 ;
end;
registration
let I be keeping_0 Program of SCM+FSA;
let j be keeping_0 Instruction of SCM+FSA;
clusterI ";" j -> keeping_0 ;
coherence
I ";" j is keeping_0 ;
end;
registration
let i, j be keeping_0 Instruction of SCM+FSA;
clusteri ";" j -> keeping_0 ;
coherence
i ";" j is keeping_0 ;
end;
begin
theorem :: SCMFSA6C:3
canceled;
theorem Th4: :: SCMFSA6C:4
for i being Instruction of SCM+FSA
for s1, s2 being State of SCM+FSA st DataPart s1 = DataPart s2 holds
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
proof
let i be Instruction of SCM+FSA; ::_thesis: for s1, s2 being State of SCM+FSA st DataPart s1 = DataPart s2 holds
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
let s1, s2 be State of SCM+FSA; ::_thesis: ( DataPart s1 = DataPart s2 implies DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
assume A1: DataPart s1 = DataPart s2 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
set l = i;
A2: dom (Exec (i,s1)) = the carrier of SCM+FSA by PARTFUN1:def_2;
then A3: dom (Exec (i,s1)) = dom (Exec (i,s2)) by PARTFUN1:def_2;
A4: dom ((Exec (i,s1)) | (Data-Locations )) = Data-Locations by A2, RELAT_1:62;
A5: dom (Exec (i,s2)) = the carrier of SCM+FSA by PARTFUN1:def_2;
then A6: dom ((Exec (i,s2)) | (Data-Locations )) = Data-Locations by RELAT_1:62;
percases ( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by NAT_1:36, SCMFSA_2:16;
suppose InsCode i = 0 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
then A7: i = halt SCM+FSA by SCMFSA_2:95;
then Exec (i,s1) = s1 by EXTPRO_1:def_3;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A1, A7, EXTPRO_1:def_3; ::_thesis: verum
end;
suppose InsCode i = 1 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
then consider db, da being Int-Location such that
A8: i = db := da by SCMFSA_2:30;
A9: for x being set st x in (Data-Locations ) \ {db} holds
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
proof
let x be set ; ::_thesis: ( x in (Data-Locations ) \ {db} implies ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x )
assume A10: x in (Data-Locations ) \ {db} ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then A11: x in Data-Locations by XBOOLE_0:def_5;
A12: not x in {db} by A10, XBOOLE_0:def_5;
percases ( x in Int-Locations or x in FinSeq-Locations ) by A11, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then reconsider a = x as Int-Location by AMI_2:def_16;
A13: a <> db by A12, TARSKI:def_1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = (Exec (i,s1)) . a by A10, FUNCT_1:49
.= s1 . a by A8, A13, SCMFSA_2:63
.= (DataPart s1) . a by A11, FUNCT_1:49
.= s2 . a by A1, A11, FUNCT_1:49
.= (Exec (i,s2)) . a by A8, A13, SCMFSA_2:63
.= ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x by A10, FUNCT_1:49 ; ::_thesis: verum
end;
suppose x in FinSeq-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then reconsider a = x as FinSeq-Location by SCMFSA_2:def_5;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = (Exec (i,s1)) . a by A10, FUNCT_1:49
.= s1 . a by A8, SCMFSA_2:63
.= (DataPart s1) . a by A11, FUNCT_1:49
.= s2 . a by A1, A11, FUNCT_1:49
.= (Exec (i,s2)) . a by A8, SCMFSA_2:63
.= ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x by A10, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
A14: dom ((Exec (i,s2)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db} by A5, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db} by A2, RELAT_1:62;
then A15: (Exec (i,s1)) | ((Data-Locations ) \ {db}) = (Exec (i,s2)) | ((Data-Locations ) \ {db}) by A14, A9, FUNCT_1:2;
db in Int-Locations by AMI_2:def_16;
then db in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A16: Data-Locations = (Data-Locations ) \/ {db} by ZFMISC_1:40
.= ((Data-Locations ) \ {db}) \/ {db} by XBOOLE_1:39 ;
A17: (Exec (i,s2)) . db = s2 . da by A8, SCMFSA_2:63;
A18: (Exec (i,s1)) . db = s1 . da by A8, SCMFSA_2:63;
da in Int-Locations by AMI_2:def_16;
then A19: da in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then s1 . da = (DataPart s1) . da by FUNCT_1:49
.= s2 . da by A1, A19, FUNCT_1:49 ;
then (Exec (i,s1)) | {db} = (Exec (i,s2)) | {db} by A3, A18, A17, GRFUNC_1:29;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A16, A15, RELAT_1:150; ::_thesis: verum
end;
suppose InsCode i = 2 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
then consider db, da being Int-Location such that
A20: i = AddTo (db,da) by SCMFSA_2:31;
A21: for x being set st x in (Data-Locations ) \ {db} holds
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
proof
let x be set ; ::_thesis: ( x in (Data-Locations ) \ {db} implies ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x )
assume A22: x in (Data-Locations ) \ {db} ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then A23: x in Data-Locations by XBOOLE_0:def_5;
A24: not x in {db} by A22, XBOOLE_0:def_5;
percases ( x in Int-Locations or x in FinSeq-Locations ) by A23, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then reconsider a = x as Int-Location by AMI_2:def_16;
A25: a <> db by A24, TARSKI:def_1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = (Exec (i,s1)) . a by A22, FUNCT_1:49
.= s1 . a by A20, A25, SCMFSA_2:64
.= (DataPart s1) . a by A23, FUNCT_1:49
.= s2 . a by A1, A23, FUNCT_1:49
.= (Exec (i,s2)) . a by A20, A25, SCMFSA_2:64
.= ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x by A22, FUNCT_1:49 ; ::_thesis: verum
end;
suppose x in FinSeq-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then reconsider a = x as FinSeq-Location by SCMFSA_2:def_5;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = (Exec (i,s1)) . a by A22, FUNCT_1:49
.= s1 . a by A20, SCMFSA_2:64
.= (DataPart s1) . a by A23, FUNCT_1:49
.= s2 . a by A1, A23, FUNCT_1:49
.= (Exec (i,s2)) . a by A20, SCMFSA_2:64
.= ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x by A22, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
A26: dom ((Exec (i,s2)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db} by A5, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db} by A2, RELAT_1:62;
then A27: (Exec (i,s1)) | ((Data-Locations ) \ {db}) = (Exec (i,s2)) | ((Data-Locations ) \ {db}) by A26, A21, FUNCT_1:2;
db in Int-Locations by AMI_2:def_16;
then db in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A28: Data-Locations = (Data-Locations ) \/ {db} by ZFMISC_1:40
.= ((Data-Locations ) \ {db}) \/ {db} by XBOOLE_1:39 ;
A29: (Exec (i,s2)) . db = (s2 . db) + (s2 . da) by A20, SCMFSA_2:64;
A30: (Exec (i,s1)) . db = (s1 . db) + (s1 . da) by A20, SCMFSA_2:64;
db in Int-Locations by AMI_2:def_16;
then A31: db in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A32: s1 . db = (DataPart s1) . db by FUNCT_1:49
.= s2 . db by A1, A31, FUNCT_1:49 ;
da in Int-Locations by AMI_2:def_16;
then A33: da in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then s1 . da = (DataPart s1) . da by FUNCT_1:49
.= s2 . da by A1, A33, FUNCT_1:49 ;
then (Exec (i,s1)) | {db} = (Exec (i,s2)) | {db} by A3, A30, A29, A32, GRFUNC_1:29;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A28, A27, RELAT_1:150; ::_thesis: verum
end;
suppose InsCode i = 3 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
then consider db, da being Int-Location such that
A34: i = SubFrom (db,da) by SCMFSA_2:32;
A35: for x being set st x in (Data-Locations ) \ {db} holds
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
proof
let x be set ; ::_thesis: ( x in (Data-Locations ) \ {db} implies ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x )
assume A36: x in (Data-Locations ) \ {db} ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then A37: x in Data-Locations by XBOOLE_0:def_5;
A38: not x in {db} by A36, XBOOLE_0:def_5;
percases ( x in Int-Locations or x in FinSeq-Locations ) by A37, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then reconsider a = x as Int-Location by AMI_2:def_16;
A39: a <> db by A38, TARSKI:def_1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = (Exec (i,s1)) . a by A36, FUNCT_1:49
.= s1 . a by A34, A39, SCMFSA_2:65
.= (DataPart s1) . a by A37, FUNCT_1:49
.= s2 . a by A1, A37, FUNCT_1:49
.= (Exec (i,s2)) . a by A34, A39, SCMFSA_2:65
.= ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x by A36, FUNCT_1:49 ; ::_thesis: verum
end;
suppose x in FinSeq-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then reconsider a = x as FinSeq-Location by SCMFSA_2:def_5;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = (Exec (i,s1)) . a by A36, FUNCT_1:49
.= s1 . a by A34, SCMFSA_2:65
.= (DataPart s1) . a by A37, FUNCT_1:49
.= s2 . a by A1, A37, FUNCT_1:49
.= (Exec (i,s2)) . a by A34, SCMFSA_2:65
.= ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x by A36, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
A40: dom ((Exec (i,s2)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db} by A5, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db} by A2, RELAT_1:62;
then A41: (Exec (i,s1)) | ((Data-Locations ) \ {db}) = (Exec (i,s2)) | ((Data-Locations ) \ {db}) by A40, A35, FUNCT_1:2;
db in Int-Locations by AMI_2:def_16;
then db in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A42: Data-Locations = (Data-Locations ) \/ {db} by ZFMISC_1:40
.= ((Data-Locations ) \ {db}) \/ {db} by XBOOLE_1:39 ;
A43: (Exec (i,s2)) . db = (s2 . db) - (s2 . da) by A34, SCMFSA_2:65;
A44: (Exec (i,s1)) . db = (s1 . db) - (s1 . da) by A34, SCMFSA_2:65;
db in Int-Locations by AMI_2:def_16;
then A45: db in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A46: s1 . db = (DataPart s1) . db by FUNCT_1:49
.= s2 . db by A1, A45, FUNCT_1:49 ;
da in Int-Locations by AMI_2:def_16;
then A47: da in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then s1 . da = (DataPart s1) . da by FUNCT_1:49
.= s2 . da by A1, A47, FUNCT_1:49 ;
then (Exec (i,s1)) | {db} = (Exec (i,s2)) | {db} by A3, A44, A43, A46, GRFUNC_1:29;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A42, A41, RELAT_1:150; ::_thesis: verum
end;
suppose InsCode i = 4 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
then consider db, da being Int-Location such that
A48: i = MultBy (db,da) by SCMFSA_2:33;
A49: for x being set st x in (Data-Locations ) \ {db} holds
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
proof
let x be set ; ::_thesis: ( x in (Data-Locations ) \ {db} implies ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x )
assume A50: x in (Data-Locations ) \ {db} ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then A51: x in Data-Locations by XBOOLE_0:def_5;
A52: not x in {db} by A50, XBOOLE_0:def_5;
percases ( x in Int-Locations or x in FinSeq-Locations ) by A51, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then reconsider a = x as Int-Location by AMI_2:def_16;
A53: a <> db by A52, TARSKI:def_1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = (Exec (i,s1)) . a by A50, FUNCT_1:49
.= s1 . a by A48, A53, SCMFSA_2:66
.= (DataPart s1) . a by A51, FUNCT_1:49
.= s2 . a by A1, A51, FUNCT_1:49
.= (Exec (i,s2)) . a by A48, A53, SCMFSA_2:66
.= ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x by A50, FUNCT_1:49 ; ::_thesis: verum
end;
suppose x in FinSeq-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then reconsider a = x as FinSeq-Location by SCMFSA_2:def_5;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = (Exec (i,s1)) . a by A50, FUNCT_1:49
.= s1 . a by A48, SCMFSA_2:66
.= (DataPart s1) . a by A51, FUNCT_1:49
.= s2 . a by A1, A51, FUNCT_1:49
.= (Exec (i,s2)) . a by A48, SCMFSA_2:66
.= ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x by A50, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
A54: dom ((Exec (i,s2)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db} by A5, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db} by A2, RELAT_1:62;
then A55: (Exec (i,s1)) | ((Data-Locations ) \ {db}) = (Exec (i,s2)) | ((Data-Locations ) \ {db}) by A54, A49, FUNCT_1:2;
db in Int-Locations by AMI_2:def_16;
then db in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A56: Data-Locations = (Data-Locations ) \/ {db} by ZFMISC_1:40
.= ((Data-Locations ) \ {db}) \/ {db} by XBOOLE_1:39 ;
A57: (Exec (i,s2)) . db = (s2 . db) * (s2 . da) by A48, SCMFSA_2:66;
A58: (Exec (i,s1)) . db = (s1 . db) * (s1 . da) by A48, SCMFSA_2:66;
db in Int-Locations by AMI_2:def_16;
then A59: db in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A60: s1 . db = (DataPart s1) . db by FUNCT_1:49
.= s2 . db by A1, A59, FUNCT_1:49 ;
da in Int-Locations by AMI_2:def_16;
then A61: da in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then s1 . da = (DataPart s1) . da by FUNCT_1:49
.= s2 . da by A1, A61, FUNCT_1:49 ;
then (Exec (i,s1)) | {db} = (Exec (i,s2)) | {db} by A3, A58, A57, A60, GRFUNC_1:29;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A56, A55, RELAT_1:150; ::_thesis: verum
end;
suppose InsCode i = 5 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
then consider db, da being Int-Location such that
A62: i = Divide (db,da) by SCMFSA_2:34;
hereby ::_thesis: verum
percases ( da <> db or da = db ) ;
supposeA63: da <> db ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
A64: for x being set st x in (Data-Locations ) \ {db,da} holds
((Exec (i,s1)) | ((Data-Locations ) \ {db,da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db,da})) . x
proof
let x be set ; ::_thesis: ( x in (Data-Locations ) \ {db,da} implies ((Exec (i,s1)) | ((Data-Locations ) \ {db,da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db,da})) . x )
assume A65: x in (Data-Locations ) \ {db,da} ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db,da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db,da})) . x
then A66: x in Data-Locations by XBOOLE_0:def_5;
A67: not x in {db,da} by A65, XBOOLE_0:def_5;
percases ( x in Int-Locations or x in FinSeq-Locations ) by A66, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db,da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db,da})) . x
then reconsider a = x as Int-Location by AMI_2:def_16;
A68: a <> da by A67, TARSKI:def_2;
A69: a <> db by A67, TARSKI:def_2;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db,da})) . x = (Exec (i,s1)) . a by A65, FUNCT_1:49
.= s1 . a by A62, A68, A69, SCMFSA_2:67
.= (DataPart s1) . a by A66, FUNCT_1:49
.= s2 . a by A1, A66, FUNCT_1:49
.= (Exec (i,s2)) . a by A62, A68, A69, SCMFSA_2:67
.= ((Exec (i,s2)) | ((Data-Locations ) \ {db,da})) . x by A65, FUNCT_1:49 ; ::_thesis: verum
end;
suppose x in FinSeq-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db,da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db,da})) . x
then reconsider a = x as FinSeq-Location by SCMFSA_2:def_5;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db,da})) . x = (Exec (i,s1)) . a by A65, FUNCT_1:49
.= s1 . a by A62, SCMFSA_2:67
.= (DataPart s1) . a by A66, FUNCT_1:49
.= s2 . a by A1, A66, FUNCT_1:49
.= (Exec (i,s2)) . a by A62, SCMFSA_2:67
.= ((Exec (i,s2)) | ((Data-Locations ) \ {db,da})) . x by A65, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
A70: dom ((Exec (i,s2)) | ((Data-Locations ) \ {db,da})) = (Data-Locations ) \ {db,da} by A5, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {db,da})) = (Data-Locations ) \ {db,da} by A2, RELAT_1:62;
then A71: (Exec (i,s1)) | ((Data-Locations ) \ {db,da}) = (Exec (i,s2)) | ((Data-Locations ) \ {db,da}) by A70, A64, FUNCT_1:2;
A72: (Exec (i,s2)) . da = (s2 . db) mod (s2 . da) by A62, SCMFSA_2:67;
db in Int-Locations by AMI_2:def_16;
then A73: db in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A74: s1 . db = (DataPart s1) . db by FUNCT_1:49
.= s2 . db by A1, A73, FUNCT_1:49 ;
da in Int-Locations by AMI_2:def_16;
then A75: da in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
db in Int-Locations by AMI_2:def_16;
then db in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A76: Data-Locations = (Data-Locations ) \/ {db,da} by A75, ZFMISC_1:42
.= ((Data-Locations ) \ {db,da}) \/ {db,da} by XBOOLE_1:39 ;
A77: (Exec (i,s1)) . da = (s1 . db) mod (s1 . da) by A62, SCMFSA_2:67;
A78: (Exec (i,s2)) . db = (s2 . db) div (s2 . da) by A62, A63, SCMFSA_2:67;
A79: (Exec (i,s1)) . db = (s1 . db) div (s1 . da) by A62, A63, SCMFSA_2:67;
da in Int-Locations by AMI_2:def_16;
then A80: da in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then s1 . da = (DataPart s1) . da by FUNCT_1:49
.= s2 . da by A1, A80, FUNCT_1:49 ;
then (Exec (i,s1)) | {db,da} = (Exec (i,s2)) | {db,da} by A3, A79, A77, A78, A72, A74, GRFUNC_1:30;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A76, A71, RELAT_1:150; ::_thesis: verum
end;
supposeA81: da = db ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
A82: for x being set st x in (Data-Locations ) \ {db} holds
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
proof
let x be set ; ::_thesis: ( x in (Data-Locations ) \ {db} implies ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x )
assume A83: x in (Data-Locations ) \ {db} ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then A84: x in Data-Locations by XBOOLE_0:def_5;
A85: not x in {db} by A83, XBOOLE_0:def_5;
percases ( x in Int-Locations or x in FinSeq-Locations ) by A84, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then reconsider a = x as Int-Location by AMI_2:def_16;
A86: a <> db by A85, TARSKI:def_1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = (Exec (i,s1)) . a by A83, FUNCT_1:49
.= s1 . a by A62, A81, A86, SCMFSA_2:68
.= (DataPart s1) . a by A84, FUNCT_1:49
.= s2 . a by A1, A84, FUNCT_1:49
.= (Exec (i,s2)) . a by A62, A81, A86, SCMFSA_2:68
.= ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x by A83, FUNCT_1:49 ; ::_thesis: verum
end;
suppose x in FinSeq-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then reconsider a = x as FinSeq-Location by SCMFSA_2:def_5;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = (Exec (i,s1)) . a by A83, FUNCT_1:49
.= s1 . a by A62, A81, SCMFSA_2:68
.= (s1 | (Data-Locations )) . a by A84, FUNCT_1:49
.= s2 . a by A1, A84, FUNCT_1:49
.= (Exec (i,s2)) . a by A62, A81, SCMFSA_2:68
.= ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x by A83, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
A87: dom ((Exec (i,s2)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db} by A5, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db} by A2, RELAT_1:62;
then A88: (Exec (i,s1)) | ((Data-Locations ) \ {db}) = (Exec (i,s2)) | ((Data-Locations ) \ {db}) by A87, A82, FUNCT_1:2;
db in Int-Locations by AMI_2:def_16;
then db in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A89: Data-Locations = (Data-Locations ) \/ {db} by ZFMISC_1:40
.= ((Data-Locations ) \ {db}) \/ {db} by XBOOLE_1:39 ;
A90: (Exec (i,s2)) . db = (s2 . db) mod (s2 . da) by A62, A81, SCMFSA_2:68;
A91: (Exec (i,s1)) . db = (s1 . db) mod (s1 . da) by A62, A81, SCMFSA_2:68;
db in Int-Locations by AMI_2:def_16;
then A92: db in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A93: s1 . db = (DataPart s1) . db by FUNCT_1:49
.= s2 . db by A1, A92, FUNCT_1:49 ;
da in Int-Locations by AMI_2:def_16;
then A94: da in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then s1 . da = (DataPart s1) . da by FUNCT_1:49
.= s2 . da by A1, A94, FUNCT_1:49 ;
then (Exec (i,s1)) | {db} = (Exec (i,s2)) | {db} by A3, A91, A90, A93, GRFUNC_1:29;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A89, A88, RELAT_1:150; ::_thesis: verum
end;
end;
end;
end;
suppose InsCode i = 6 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
then A95: ex l1 being Element of NAT st i = goto l1 by SCMFSA_2:35;
for x being set st x in Data-Locations holds
(DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
proof
let x be set ; ::_thesis: ( x in Data-Locations implies (DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x )
assume A96: x in Data-Locations ; ::_thesis: (DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
percases ( x in Int-Locations or x in FinSeq-Locations ) by A96, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: (DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
then reconsider a = x as Int-Location by AMI_2:def_16;
thus (DataPart (Exec (i,s1))) . x = (Exec (i,s1)) . a by A96, FUNCT_1:49
.= s1 . a by A95, SCMFSA_2:69
.= (DataPart s1) . a by A96, FUNCT_1:49
.= s2 . a by A1, A96, FUNCT_1:49
.= (Exec (i,s2)) . a by A95, SCMFSA_2:69
.= (DataPart (Exec (i,s2))) . x by A96, FUNCT_1:49 ; ::_thesis: verum
end;
suppose x in FinSeq-Locations ; ::_thesis: (DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
then reconsider a = x as FinSeq-Location by SCMFSA_2:def_5;
thus (DataPart (Exec (i,s1))) . x = (Exec (i,s1)) . a by A96, FUNCT_1:49
.= s1 . a by A95, SCMFSA_2:69
.= (DataPart s1) . a by A96, FUNCT_1:49
.= s2 . a by A1, A96, FUNCT_1:49
.= (Exec (i,s2)) . a by A95, SCMFSA_2:69
.= (DataPart (Exec (i,s2))) . x by A96, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A4, A6, FUNCT_1:2; ::_thesis: verum
end;
suppose InsCode i = 7 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
then A97: ex l1 being Element of NAT ex a being Int-Location st i = a =0_goto l1 by SCMFSA_2:36;
for x being set st x in Data-Locations holds
(DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
proof
let x be set ; ::_thesis: ( x in Data-Locations implies (DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x )
assume A98: x in Data-Locations ; ::_thesis: (DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
percases ( x in Int-Locations or x in FinSeq-Locations ) by A98, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: (DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
then reconsider a = x as Int-Location by AMI_2:def_16;
thus (DataPart (Exec (i,s1))) . x = (Exec (i,s1)) . a by A98, FUNCT_1:49
.= s1 . a by A97, SCMFSA_2:70
.= (DataPart s1) . a by A98, FUNCT_1:49
.= s2 . a by A1, A98, FUNCT_1:49
.= (Exec (i,s2)) . a by A97, SCMFSA_2:70
.= (DataPart (Exec (i,s2))) . x by A98, FUNCT_1:49 ; ::_thesis: verum
end;
suppose x in FinSeq-Locations ; ::_thesis: (DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
then reconsider a = x as FinSeq-Location by SCMFSA_2:def_5;
thus (DataPart (Exec (i,s1))) . x = (Exec (i,s1)) . a by A98, FUNCT_1:49
.= s1 . a by A97, SCMFSA_2:70
.= (DataPart s1) . a by A98, FUNCT_1:49
.= s2 . a by A1, A98, FUNCT_1:49
.= (Exec (i,s2)) . a by A97, SCMFSA_2:70
.= (DataPart (Exec (i,s2))) . x by A98, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A4, A6, FUNCT_1:2; ::_thesis: verum
end;
suppose InsCode i = 8 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
then A99: ex l1 being Element of NAT ex a being Int-Location st i = a >0_goto l1 by SCMFSA_2:37;
for x being set st x in Data-Locations holds
(DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
proof
let x be set ; ::_thesis: ( x in Data-Locations implies (DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x )
assume A100: x in Data-Locations ; ::_thesis: (DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
percases ( x in Int-Locations or x in FinSeq-Locations ) by A100, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: (DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
then reconsider a = x as Int-Location by AMI_2:def_16;
thus (DataPart (Exec (i,s1))) . x = (Exec (i,s1)) . a by A100, FUNCT_1:49
.= s1 . a by A99, SCMFSA_2:71
.= (DataPart s1) . a by A100, FUNCT_1:49
.= s2 . a by A1, A100, FUNCT_1:49
.= (Exec (i,s2)) . a by A99, SCMFSA_2:71
.= (DataPart (Exec (i,s2))) . x by A100, FUNCT_1:49 ; ::_thesis: verum
end;
suppose x in FinSeq-Locations ; ::_thesis: (DataPart (Exec (i,s1))) . x = (DataPart (Exec (i,s2))) . x
then reconsider a = x as FinSeq-Location by SCMFSA_2:def_5;
thus (DataPart (Exec (i,s1))) . x = (Exec (i,s1)) . a by A100, FUNCT_1:49
.= s1 . a by A99, SCMFSA_2:71
.= (DataPart s1) . a by A100, FUNCT_1:49
.= s2 . a by A1, A100, FUNCT_1:49
.= (Exec (i,s2)) . a by A99, SCMFSA_2:71
.= (DataPart (Exec (i,s2))) . x by A100, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A4, A6, FUNCT_1:2; ::_thesis: verum
end;
suppose InsCode i = 9 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
then consider da, db being Int-Location, fa being FinSeq-Location such that
A101: i = db := (fa,da) by SCMFSA_2:38;
A102: for x being set st x in (Data-Locations ) \ {db} holds
((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
proof
let x be set ; ::_thesis: ( x in (Data-Locations ) \ {db} implies ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x )
assume A103: x in (Data-Locations ) \ {db} ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then A104: x in Data-Locations by XBOOLE_0:def_5;
A105: not x in {db} by A103, XBOOLE_0:def_5;
percases ( x in Int-Locations or x in FinSeq-Locations ) by A104, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then reconsider a = x as Int-Location by AMI_2:def_16;
A106: a <> db by A105, TARSKI:def_1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = (Exec (i,s1)) . a by A103, FUNCT_1:49
.= s1 . a by A101, A106, SCMFSA_2:72
.= (DataPart s1) . a by A104, FUNCT_1:49
.= s2 . a by A1, A104, FUNCT_1:49
.= (Exec (i,s2)) . a by A101, A106, SCMFSA_2:72
.= ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x by A103, FUNCT_1:49 ; ::_thesis: verum
end;
suppose x in FinSeq-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x
then reconsider a = x as FinSeq-Location by SCMFSA_2:def_5;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {db})) . x = (Exec (i,s1)) . a by A103, FUNCT_1:49
.= s1 . a by A101, SCMFSA_2:72
.= (DataPart s1) . a by A104, FUNCT_1:49
.= s2 . a by A1, A104, FUNCT_1:49
.= (Exec (i,s2)) . a by A101, SCMFSA_2:72
.= ((Exec (i,s2)) | ((Data-Locations ) \ {db})) . x by A103, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
A107: dom ((Exec (i,s2)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db} by A5, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {db})) = (Data-Locations ) \ {db} by A2, RELAT_1:62;
then A108: (Exec (i,s1)) | ((Data-Locations ) \ {db}) = (Exec (i,s2)) | ((Data-Locations ) \ {db}) by A107, A102, FUNCT_1:2;
db in Int-Locations by AMI_2:def_16;
then db in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A109: Data-Locations = (Data-Locations ) \/ {db} by ZFMISC_1:40
.= ((Data-Locations ) \ {db}) \/ {db} by XBOOLE_1:39 ;
A110: ex k2 being Element of NAT st
( k2 = abs (s2 . da) & (Exec (i,s2)) . db = (s2 . fa) /. k2 ) by A101, SCMFSA_2:72;
A111: ex k1 being Element of NAT st
( k1 = abs (s1 . da) & (Exec (i,s1)) . db = (s1 . fa) /. k1 ) by A101, SCMFSA_2:72;
fa in FinSeq-Locations by SCMFSA_2:def_5;
then A112: fa in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A113: s1 . fa = (DataPart s1) . fa by FUNCT_1:49
.= s2 . fa by A1, A112, FUNCT_1:49 ;
da in Int-Locations by AMI_2:def_16;
then A114: da in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then s1 . da = (DataPart s1) . da by FUNCT_1:49
.= s2 . da by A1, A114, FUNCT_1:49 ;
then (Exec (i,s1)) | {db} = (Exec (i,s2)) | {db} by A3, A111, A110, A113, GRFUNC_1:29;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A109, A108, RELAT_1:150; ::_thesis: verum
end;
suppose InsCode i = 10 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
then consider da, db being Int-Location, fa being FinSeq-Location such that
A115: i = (fa,da) := db by SCMFSA_2:39;
A116: for x being set st x in (Data-Locations ) \ {fa} holds
((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x
proof
let x be set ; ::_thesis: ( x in (Data-Locations ) \ {fa} implies ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x )
assume A117: x in (Data-Locations ) \ {fa} ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x
then A118: x in Data-Locations by XBOOLE_0:def_5;
A119: not x in {fa} by A117, XBOOLE_0:def_5;
percases ( x in Int-Locations or x in FinSeq-Locations ) by A118, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x
then reconsider a = x as Int-Location by AMI_2:def_16;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = (Exec (i,s1)) . a by A117, FUNCT_1:49
.= s1 . a by A115, SCMFSA_2:73
.= (DataPart s1) . a by A118, FUNCT_1:49
.= s2 . a by A1, A118, FUNCT_1:49
.= (Exec (i,s2)) . a by A115, SCMFSA_2:73
.= ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x by A117, FUNCT_1:49 ; ::_thesis: verum
end;
suppose x in FinSeq-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x
then reconsider a = x as FinSeq-Location by SCMFSA_2:def_5;
A120: a <> fa by A119, TARSKI:def_1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = (Exec (i,s1)) . a by A117, FUNCT_1:49
.= s1 . a by A115, A120, SCMFSA_2:73
.= (DataPart s1) . a by A118, FUNCT_1:49
.= s2 . a by A1, A118, FUNCT_1:49
.= (Exec (i,s2)) . a by A115, A120, SCMFSA_2:73
.= ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x by A117, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
A121: dom ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) = (Data-Locations ) \ {fa} by A5, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) = (Data-Locations ) \ {fa} by A2, RELAT_1:62;
then A122: (Exec (i,s1)) | ((Data-Locations ) \ {fa}) = (Exec (i,s2)) | ((Data-Locations ) \ {fa}) by A121, A116, FUNCT_1:2;
fa in FinSeq-Locations by SCMFSA_2:def_5;
then fa in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A123: Data-Locations = (Data-Locations ) \/ {fa} by ZFMISC_1:40
.= ((Data-Locations ) \ {fa}) \/ {fa} by XBOOLE_1:39 ;
fa in FinSeq-Locations by SCMFSA_2:def_5;
then A124: fa in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A125: s1 . fa = (DataPart s1) . fa by FUNCT_1:49
.= s2 . fa by A1, A124, FUNCT_1:49 ;
db in Int-Locations by AMI_2:def_16;
then A126: db in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A127: s1 . db = (DataPart s1) . db by FUNCT_1:49
.= s2 . db by A1, A126, FUNCT_1:49 ;
A128: ex k2 being Element of NAT st
( k2 = abs (s2 . da) & (Exec (i,s2)) . fa = (s2 . fa) +* (k2,(s2 . db)) ) by A115, SCMFSA_2:73;
A129: ex k1 being Element of NAT st
( k1 = abs (s1 . da) & (Exec (i,s1)) . fa = (s1 . fa) +* (k1,(s1 . db)) ) by A115, SCMFSA_2:73;
da in Int-Locations by AMI_2:def_16;
then A130: da in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then s1 . da = (DataPart s1) . da by FUNCT_1:49
.= s2 . da by A1, A130, FUNCT_1:49 ;
then (Exec (i,s1)) | {fa} = (Exec (i,s2)) | {fa} by A3, A129, A128, A127, A125, GRFUNC_1:29;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A123, A122, RELAT_1:150; ::_thesis: verum
end;
suppose InsCode i = 11 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
then consider da being Int-Location, fa being FinSeq-Location such that
A131: i = da :=len fa by SCMFSA_2:40;
A132: for x being set st x in (Data-Locations ) \ {da} holds
((Exec (i,s1)) | ((Data-Locations ) \ {da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {da})) . x
proof
let x be set ; ::_thesis: ( x in (Data-Locations ) \ {da} implies ((Exec (i,s1)) | ((Data-Locations ) \ {da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {da})) . x )
assume A133: x in (Data-Locations ) \ {da} ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {da})) . x
then A134: x in Data-Locations by XBOOLE_0:def_5;
A135: not x in {da} by A133, XBOOLE_0:def_5;
percases ( x in Int-Locations or x in FinSeq-Locations ) by A134, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {da})) . x
then reconsider a = x as Int-Location by AMI_2:def_16;
A136: a <> da by A135, TARSKI:def_1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {da})) . x = (Exec (i,s1)) . a by A133, FUNCT_1:49
.= s1 . a by A131, A136, SCMFSA_2:74
.= (DataPart s1) . a by A134, FUNCT_1:49
.= s2 . a by A1, A134, FUNCT_1:49
.= (Exec (i,s2)) . a by A131, A136, SCMFSA_2:74
.= ((Exec (i,s2)) | ((Data-Locations ) \ {da})) . x by A133, FUNCT_1:49 ; ::_thesis: verum
end;
suppose x in FinSeq-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {da})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {da})) . x
then reconsider a = x as FinSeq-Location by SCMFSA_2:def_5;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {da})) . x = (Exec (i,s1)) . a by A133, FUNCT_1:49
.= s1 . a by A131, SCMFSA_2:74
.= (DataPart s1) . a by A134, FUNCT_1:49
.= s2 . a by A1, A134, FUNCT_1:49
.= (Exec (i,s2)) . a by A131, SCMFSA_2:74
.= ((Exec (i,s2)) | ((Data-Locations ) \ {da})) . x by A133, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
da in Int-Locations by AMI_2:def_16;
then da in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A137: Data-Locations = (Data-Locations ) \/ {da} by ZFMISC_1:40
.= ((Data-Locations ) \ {da}) \/ {da} by XBOOLE_1:39 ;
fa in FinSeq-Locations by SCMFSA_2:def_5;
then A138: fa in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then s1 . fa = (s1 | (Data-Locations )) . fa by FUNCT_1:49
.= s2 . fa by A1, A138, FUNCT_1:49 ;
then (Exec (i,s1)) . da = len (s2 . fa) by A131, SCMFSA_2:74
.= (Exec (i,s2)) . da by A131, SCMFSA_2:74 ;
then A139: (Exec (i,s1)) | {da} = (Exec (i,s2)) | {da} by A2, A5, GRFUNC_1:29;
A140: dom ((Exec (i,s2)) | ((Data-Locations ) \ {da})) = (Data-Locations ) \ {da} by A5, RELAT_1:62;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {da})) = (Data-Locations ) \ {da} by A2, RELAT_1:62;
then (Exec (i,s1)) | ((Data-Locations ) \ {da}) = (Exec (i,s2)) | ((Data-Locations ) \ {da}) by A140, A132, FUNCT_1:2;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A137, A139, RELAT_1:150; ::_thesis: verum
end;
suppose InsCode i = 12 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
then consider da being Int-Location, fa being FinSeq-Location such that
A141: i = fa :=<0,...,0> da by SCMFSA_2:41;
set l = i;
A142: dom ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) = (Data-Locations ) \ {fa} by A5, RELAT_1:62;
A143: ex k2 being Element of NAT st
( k2 = abs (s2 . da) & (Exec (i,s2)) . fa = k2 |-> 0 ) by A141, SCMFSA_2:75;
A144: ex k1 being Element of NAT st
( k1 = abs (s1 . da) & (Exec (i,s1)) . fa = k1 |-> 0 ) by A141, SCMFSA_2:75;
A145: for x being set st x in (Data-Locations ) \ {fa} holds
((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x
proof
let x be set ; ::_thesis: ( x in (Data-Locations ) \ {fa} implies ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x )
assume A146: x in (Data-Locations ) \ {fa} ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x
then A147: x in Data-Locations by XBOOLE_0:def_5;
A148: not x in {fa} by A146, XBOOLE_0:def_5;
percases ( x in Int-Locations or x in FinSeq-Locations ) by A147, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x
then reconsider a = x as Int-Location by AMI_2:def_16;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = (Exec (i,s1)) . a by A146, FUNCT_1:49
.= s1 . a by A141, SCMFSA_2:75
.= (DataPart s1) . a by A147, FUNCT_1:49
.= s2 . a by A1, A147, FUNCT_1:49
.= (Exec (i,s2)) . a by A141, SCMFSA_2:75
.= ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x by A146, FUNCT_1:49 ; ::_thesis: verum
end;
suppose x in FinSeq-Locations ; ::_thesis: ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x
then reconsider a = x as FinSeq-Location by SCMFSA_2:def_5;
A149: a <> fa by A148, TARSKI:def_1;
thus ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) . x = (Exec (i,s1)) . a by A146, FUNCT_1:49
.= s1 . a by A141, A149, SCMFSA_2:75
.= (DataPart s1) . a by A147, FUNCT_1:49
.= s2 . a by A1, A147, FUNCT_1:49
.= (Exec (i,s2)) . a by A141, A149, SCMFSA_2:75
.= ((Exec (i,s2)) | ((Data-Locations ) \ {fa})) . x by A146, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
dom ((Exec (i,s1)) | ((Data-Locations ) \ {fa})) = (Data-Locations ) \ {fa} by A2, RELAT_1:62;
then A150: (Exec (i,s1)) | ((Data-Locations ) \ {fa}) = (Exec (i,s2)) | ((Data-Locations ) \ {fa}) by A142, A145, FUNCT_1:2;
fa in FinSeq-Locations by SCMFSA_2:def_5;
then fa in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then A151: Data-Locations = (Data-Locations ) \/ {fa} by ZFMISC_1:40
.= ((Data-Locations ) \ {fa}) \/ {fa} by XBOOLE_1:39 ;
da in Int-Locations by AMI_2:def_16;
then A152: da in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
then s1 . da = (DataPart s1) . da by FUNCT_1:49
.= s2 . da by A1, A152, FUNCT_1:49 ;
then (Exec (i,s1)) | {fa} = (Exec (i,s2)) | {fa} by A3, A144, A143, GRFUNC_1:29;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A151, A150, RELAT_1:150; ::_thesis: verum
end;
end;
end;
Lm3: now__::_thesis:_for_I_being_keeping_0_parahalting_Program_of_SCM+FSA
for_s_being_State_of_SCM+FSA
for_P_being_Instruction-Sequence_of_SCM+FSA_holds_DataPart_(Initialized_(IExec_(I,P,s)))_=_DataPart_(IExec_(I,P,s))
set IF = Data-Locations ;
let I be keeping_0 parahalting Program of SCM+FSA; ::_thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA holds DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))
let P be Instruction-Sequence of SCM+FSA; ::_thesis: DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))
set IE = IExec (I,P,s);
now__::_thesis:_(_dom_(DataPart_(Initialized_(IExec_(I,P,s))))_=_(dom_(IExec_(I,P,s)))_/\_(Data-Locations_)_&_(_for_x_being_set_st_x_in_dom_(DataPart_(Initialized_(IExec_(I,P,s))))_holds_
(DataPart_(Initialized_(IExec_(I,P,s))))_._x_=_(IExec_(I,P,s))_._x_)_)
A1: dom (Initialized (IExec (I,P,s))) = the carrier of SCM+FSA by PARTFUN1:def_2;
A2: the carrier of SCM+FSA = {(IC )} \/ (Data-Locations ) by STRUCT_0:4;
A3: dom (IExec (I,P,s)) = the carrier of SCM+FSA by PARTFUN1:def_2;
hence dom (DataPart (Initialized (IExec (I,P,s)))) = (dom (IExec (I,P,s))) /\ (Data-Locations ) by A1, RELAT_1:61; ::_thesis: for x being set st x in dom (DataPart (Initialized (IExec (I,P,s)))) holds
(DataPart (Initialized (IExec (I,P,s)))) . b2 = (IExec (I,P,s)) . b2
then A4: dom (DataPart (Initialized (IExec (I,P,s)))) = Data-Locations by A3, A2, XBOOLE_1:21;
let x be set ; ::_thesis: ( x in dom (DataPart (Initialized (IExec (I,P,s)))) implies (DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1 )
assume A5: x in dom (DataPart (Initialized (IExec (I,P,s)))) ; ::_thesis: (DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1
percases ( x in Int-Locations or x in FinSeq-Locations ) by A5, A4, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: (DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1
then reconsider x9 = x as Int-Location by AMI_2:def_16;
percases ( x9 is read-write or x9 is read-only ) ;
supposeA6: x9 is read-write ; ::_thesis: (DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1
thus (DataPart (Initialized (IExec (I,P,s)))) . x = (Initialized (IExec (I,P,s))) . x by A5, A4, FUNCT_1:49
.= (IExec (I,P,s)) . x by A6, SCMFSA_M:37 ; ::_thesis: verum
end;
suppose x9 is read-only ; ::_thesis: (DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1
then A7: x9 = intloc 0 by SCMFSA_M:def_2;
thus (DataPart (Initialized (IExec (I,P,s)))) . x = (Initialized (IExec (I,P,s))) . x9 by A5, A4, FUNCT_1:49
.= 1 by A7, SCMFSA_M:9
.= (IExec (I,P,s)) . x by A7, SCMFSA6B:11 ; ::_thesis: verum
end;
end;
end;
suppose x in FinSeq-Locations ; ::_thesis: (DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1
then reconsider x9 = x as FinSeq-Location by SCMFSA_2:def_5;
thus (DataPart (Initialized (IExec (I,P,s)))) . x = (Initialized (IExec (I,P,s))) . x9 by A5, A4, FUNCT_1:49
.= (IExec (I,P,s)) . x by SCMFSA_M:37 ; ::_thesis: verum
end;
end;
end;
hence DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s)) by FUNCT_1:46; ::_thesis: verum
end;
theorem Th5: :: SCMFSA6C:5
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for i being parahalting Instruction of SCM+FSA holds Exec (i,(Initialized s)) = IExec ((Macro i),P,s)
proof
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for i being parahalting Instruction of SCM+FSA holds Exec (i,(Initialized s)) = IExec ((Macro i),P,s)
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for i being parahalting Instruction of SCM+FSA holds Exec (i,(Initialized s)) = IExec ((Macro i),P,s)
let i be parahalting Instruction of SCM+FSA; ::_thesis: Exec (i,(Initialized s)) = IExec ((Macro i),P,s)
set Mi = Macro i;
set sI = s +* (Initialize ((intloc 0) .--> 1));
set pI = P +* (Macro i);
A1: Macro i c= P +* (Macro i) by FUNCT_4:25;
set Is = Initialized s;
set IC1 = IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1));
reconsider Mi = Macro i as parahalting Program of SCM+FSA ;
A2: IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) in dom Mi by A1, AMISTD_1:def_10;
A3: 1 in dom Mi by COMPOS_1:60;
A4: 0 in dom Mi by COMPOS_1:60;
A5: Mi . 0 = i by COMPOS_1:58;
A6: IC (s +* (Initialize ((intloc 0) .--> 1))) = 0 by MEMSTR_0:def_11;
A7: Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),(0 + 1)) = Following ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),0))) by EXTPRO_1:3
.= Following ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))))
.= Exec (((P +* (Macro i)) . 0),(s +* (Initialize ((intloc 0) .--> 1)))) by A6, PBOOLE:143
.= Exec (i,(s +* (Initialize ((intloc 0) .--> 1)))) by A5, A1, A4, GRFUNC_1:2 ;
percases ( IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) = 0 or IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) = 1 ) by A2, COMPOS_1:60;
supposeA8: IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) = 0 ; ::_thesis: Exec (i,(Initialized s)) = IExec ((Macro i),P,s)
then A9: CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),1))) = (P +* Mi) . 0 by PBOOLE:143
.= i by A5, A4, FUNCT_4:13 ;
succ (IC (s +* (Initialize ((intloc 0) .--> 1)))) = 1 by A6;
then A10: InsCode i in {0,6,7,8} by A7, A8, SCMFSA6A:3;
hereby ::_thesis: verum
percases ( InsCode i = 0 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) by A10, ENUMSET1:def_2;
suppose InsCode i = 0 ; ::_thesis: Exec (i,(Initialized s)) = IExec ((Macro i),P,s)
then A11: i = halt SCM+FSA by SCMFSA_2:95;
then P +* Mi halts_on s +* (Initialize ((intloc 0) .--> 1)) by A9, EXTPRO_1:29;
hence Exec (i,(Initialized s)) = IExec ((Macro i),P,s) by A7, A9, A11, EXTPRO_1:def_9; ::_thesis: verum
end;
supposeA12: ( InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) ; ::_thesis: Exec (i,(Initialized s)) = IExec ((Macro i),P,s)
A13: now__::_thesis:_for_a_being_Int-Location_holds_(s_+*_(Initialize_((intloc_0)_.-->_1)))_._a_=_(Exec_(i,(s_+*_(Initialize_((intloc_0)_.-->_1)))))_._a
let a be Int-Location; ::_thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b1 = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b1
percases ( InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) by A12;
suppose InsCode i = 6 ; ::_thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b1 = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b1
then ex l being Element of NAT st i = goto l by SCMFSA_2:35;
hence (s +* (Initialize ((intloc 0) .--> 1))) . a = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . a by SCMFSA_2:69; ::_thesis: verum
end;
suppose InsCode i = 7 ; ::_thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b1 = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b1
then ex l being Element of NAT ex b being Int-Location st i = b =0_goto l by SCMFSA_2:36;
hence (s +* (Initialize ((intloc 0) .--> 1))) . a = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . a by SCMFSA_2:70; ::_thesis: verum
end;
suppose InsCode i = 8 ; ::_thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b1 = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b1
then ex l being Element of NAT ex b being Int-Location st i = b >0_goto l by SCMFSA_2:37;
hence (s +* (Initialize ((intloc 0) .--> 1))) . a = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . a by SCMFSA_2:71; ::_thesis: verum
end;
end;
end;
A14: now__::_thesis:_for_f_being_FinSeq-Location_holds_(s_+*_(Initialize_((intloc_0)_.-->_1)))_._f_=_(Exec_(i,(s_+*_(Initialize_((intloc_0)_.-->_1)))))_._f
let f be FinSeq-Location ; ::_thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b1 = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b1
percases ( InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) by A12;
suppose InsCode i = 6 ; ::_thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b1 = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b1
then ex l being Element of NAT st i = goto l by SCMFSA_2:35;
hence (s +* (Initialize ((intloc 0) .--> 1))) . f = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . f by SCMFSA_2:69; ::_thesis: verum
end;
suppose InsCode i = 7 ; ::_thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b1 = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b1
then ex l being Element of NAT ex a being Int-Location st i = a =0_goto l by SCMFSA_2:36;
hence (s +* (Initialize ((intloc 0) .--> 1))) . f = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . f by SCMFSA_2:70; ::_thesis: verum
end;
suppose InsCode i = 8 ; ::_thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b1 = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b1
then ex l being Element of NAT ex a being Int-Location st i = a >0_goto l by SCMFSA_2:37;
hence (s +* (Initialize ((intloc 0) .--> 1))) . f = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . f by SCMFSA_2:71; ::_thesis: verum
end;
end;
end;
A15: Following ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1)))) = Following ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),0)))
.= Exec (i,(s +* (Initialize ((intloc 0) .--> 1)))) by A7, EXTPRO_1:3 ;
A16: InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
for n being Element of NAT holds CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),n))) <> halt SCM+FSA by A9, A12, A13, A14, A7, A8, A6, A15, AMISTD_2:11, SCMFSA_2:104, A16;
then A17: not P +* Mi halts_on s +* (Initialize ((intloc 0) .--> 1)) by EXTPRO_1:29;
Mi c= P +* Mi by FUNCT_4:25;
hence Exec (i,(Initialized s)) = IExec ((Macro i),P,s) by A17, AMISTD_1:def_11; ::_thesis: verum
end;
end;
end;
end;
supposeA18: IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) = 1 ; ::_thesis: Exec (i,(Initialized s)) = IExec ((Macro i),P,s)
A19: Mi . 1 = halt SCM+FSA by COMPOS_1:59;
A20: CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),1))) = (P +* Mi) . 1 by A18, PBOOLE:143
.= halt SCM+FSA by A19, A1, A3, GRFUNC_1:2 ;
then P +* Mi halts_on s +* (Initialize ((intloc 0) .--> 1)) by EXTPRO_1:29;
hence Exec (i,(Initialized s)) = IExec ((Macro i),P,s) by A7, A20, EXTPRO_1:def_9; ::_thesis: verum
end;
end;
end;
theorem Th6: :: SCMFSA6C:6
for a being Int-Location
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being keeping_0 parahalting Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((I ";" j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a
proof
let a be Int-Location; ::_thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being keeping_0 parahalting Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((I ";" j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being keeping_0 parahalting Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((I ";" j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being keeping_0 parahalting Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((I ";" j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a
let I be keeping_0 parahalting Program of SCM+FSA; ::_thesis: for j being parahalting Instruction of SCM+FSA holds (IExec ((I ";" j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a
let j be parahalting Instruction of SCM+FSA; ::_thesis: (IExec ((I ";" j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a
set Mj = Macro j;
set SA = Start-At (((IC (IExec ((Macro j),P,(IExec (I,P,s))))) + (card I)),SCM+FSA);
A1: not a in dom (Start-At (((IC (IExec ((Macro j),P,(IExec (I,P,s))))) + (card I)),SCM+FSA)) by SCMFSA_2:102;
A2: DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s)) by Lm3;
a in Int-Locations by AMI_2:def_16;
then A3: a in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
thus (IExec ((I ";" j),P,s)) . a = (IncIC ((IExec ((Macro j),P,(IExec (I,P,s)))),(card I))) . a by SCMFSA6B:20
.= (IExec ((Macro j),P,(IExec (I,P,s)))) . a by A1, FUNCT_4:11
.= (Exec (j,(Initialized (IExec (I,P,s))))) . a by Th5
.= (DataPart (Exec (j,(Initialized (IExec (I,P,s)))))) . a by A3, FUNCT_1:49
.= (DataPart (Exec (j,(IExec (I,P,s))))) . a by A2, Th4
.= (Exec (j,(IExec (I,P,s)))) . a by A3, FUNCT_1:49 ; ::_thesis: verum
end;
theorem Th7: :: SCMFSA6C:7
for f being FinSeq-Location
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being keeping_0 parahalting Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((I ";" j),P,s)) . f = (Exec (j,(IExec (I,P,s)))) . f
proof
let f be FinSeq-Location ; ::_thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being keeping_0 parahalting Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((I ";" j),P,s)) . f = (Exec (j,(IExec (I,P,s)))) . f
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being keeping_0 parahalting Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((I ";" j),P,s)) . f = (Exec (j,(IExec (I,P,s)))) . f
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being keeping_0 parahalting Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((I ";" j),P,s)) . f = (Exec (j,(IExec (I,P,s)))) . f
let I be keeping_0 parahalting Program of SCM+FSA; ::_thesis: for j being parahalting Instruction of SCM+FSA holds (IExec ((I ";" j),P,s)) . f = (Exec (j,(IExec (I,P,s)))) . f
let j be parahalting Instruction of SCM+FSA; ::_thesis: (IExec ((I ";" j),P,s)) . f = (Exec (j,(IExec (I,P,s)))) . f
set Mj = Macro j;
set SA = Start-At (((IC (IExec ((Macro j),P,(IExec (I,P,s))))) + (card I)),SCM+FSA);
A1: not f in dom (Start-At (((IC (IExec ((Macro j),P,(IExec (I,P,s))))) + (card I)),SCM+FSA)) by SCMFSA_2:103;
A2: DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s)) by Lm3;
f in FinSeq-Locations by SCMFSA_2:def_5;
then A3: f in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
thus (IExec ((I ";" j),P,s)) . f = (IncIC ((IExec ((Macro j),P,(IExec (I,P,s)))),(card I))) . f by SCMFSA6B:20
.= (IExec ((Macro j),P,(IExec (I,P,s)))) . f by A1, FUNCT_4:11
.= (Exec (j,(Initialized (IExec (I,P,s))))) . f by Th5
.= (DataPart (Exec (j,(Initialized (IExec (I,P,s)))))) . f by A3, FUNCT_1:49
.= (DataPart (Exec (j,(IExec (I,P,s))))) . f by A2, Th4
.= (Exec (j,(IExec (I,P,s)))) . f by A3, FUNCT_1:49 ; ::_thesis: verum
end;
theorem Th8: :: SCMFSA6C:8
for a being Int-Location
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . a = (Exec (j,(Exec (i,(Initialized s))))) . a
proof
let a be Int-Location; ::_thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . a = (Exec (j,(Exec (i,(Initialized s))))) . a
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . a = (Exec (j,(Exec (i,(Initialized s))))) . a
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for i being parahalting keeping_0 Instruction of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . a = (Exec (j,(Exec (i,(Initialized s))))) . a
let i be parahalting keeping_0 Instruction of SCM+FSA; ::_thesis: for j being parahalting Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . a = (Exec (j,(Exec (i,(Initialized s))))) . a
let j be parahalting Instruction of SCM+FSA; ::_thesis: (IExec ((i ";" j),P,s)) . a = (Exec (j,(Exec (i,(Initialized s))))) . a
set Mi = Macro i;
thus (IExec ((i ";" j),P,s)) . a = (IExec (((Macro i) ";" j),P,s)) . a
.= (Exec (j,(IExec ((Macro i),P,s)))) . a by Th6
.= (Exec (j,(Exec (i,(Initialized s))))) . a by Th5 ; ::_thesis: verum
end;
theorem :: SCMFSA6C:9
for f being FinSeq-Location
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . f = (Exec (j,(Exec (i,(Initialized s))))) . f
proof
let f be FinSeq-Location ; ::_thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . f = (Exec (j,(Exec (i,(Initialized s))))) . f
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . f = (Exec (j,(Exec (i,(Initialized s))))) . f
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for i being parahalting keeping_0 Instruction of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . f = (Exec (j,(Exec (i,(Initialized s))))) . f
let i be parahalting keeping_0 Instruction of SCM+FSA; ::_thesis: for j being parahalting Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . f = (Exec (j,(Exec (i,(Initialized s))))) . f
let j be parahalting Instruction of SCM+FSA; ::_thesis: (IExec ((i ";" j),P,s)) . f = (Exec (j,(Exec (i,(Initialized s))))) . f
set Mi = Macro i;
thus (IExec ((i ";" j),P,s)) . f = (IExec (((Macro i) ";" j),P,s)) . f
.= (Exec (j,(IExec ((Macro i),P,s)))) . f by Th7
.= (Exec (j,(Exec (i,(Initialized s))))) . f by Th5 ; ::_thesis: verum
end;
begin
definition
let a, b be Int-Location;
func swap (a,b) -> Program of SCM+FSA equals :: SCMFSA6C:def 3
(((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)) ";" (b := (FirstNotUsed (Macro (a := b))));
correctness
coherence
(((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)) ";" (b := (FirstNotUsed (Macro (a := b)))) is Program of SCM+FSA;
;
end;
:: deftheorem defines swap SCMFSA6C:def_3_:_
for a, b being Int-Location holds swap (a,b) = (((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)) ";" (b := (FirstNotUsed (Macro (a := b))));
registration
let a, b be Int-Location;
cluster swap (a,b) -> parahalting ;
coherence
swap (a,b) is parahalting ;
end;
registration
let a, b be read-write Int-Location;
cluster swap (a,b) -> keeping_0 ;
coherence
swap (a,b) is keeping_0 ;
end;
theorem :: SCMFSA6C:10
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for a, b being read-write Int-Location holds
( (IExec ((swap (a,b)),P,s)) . a = s . b & (IExec ((swap (a,b)),P,s)) . b = s . a )
proof
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for a, b being read-write Int-Location holds
( (IExec ((swap (a,b)),P,s)) . a = s . b & (IExec ((swap (a,b)),P,s)) . b = s . a )
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for a, b being read-write Int-Location holds
( (IExec ((swap (a,b)),P,s)) . a = s . b & (IExec ((swap (a,b)),P,s)) . b = s . a )
let a, b be read-write Int-Location; ::_thesis: ( (IExec ((swap (a,b)),P,s)) . a = s . b & (IExec ((swap (a,b)),P,s)) . b = s . a )
set i0 = (FirstNotUsed (Macro (a := b))) := a;
set i1 = a := b;
set i2 = b := (FirstNotUsed (Macro (a := b)));
set i01 = ((FirstNotUsed (Macro (a := b))) := a) ";" (a := b);
UsedIntLoc (Macro (a := b)) = UsedIntLoc (a := b) by SF_MASTR:28;
then UsedIntLoc (Macro (a := b)) = {a,b} by SF_MASTR:14;
then A1: not FirstNotUsed (Macro (a := b)) in {a,b} by SF_MASTR:50;
then A2: FirstNotUsed (Macro (a := b)) <> a by TARSKI:def_2;
A3: FirstNotUsed (Macro (a := b)) <> b by A1, TARSKI:def_2;
hereby ::_thesis: (IExec ((swap (a,b)),P,s)) . b = s . a
percases ( a <> b or a = b ) ;
supposeA4: a <> b ; ::_thesis: (IExec ((swap (a,b)),P,s)) . a = s . b
thus (IExec ((swap (a,b)),P,s)) . a = (Exec ((b := (FirstNotUsed (Macro (a := b)))),(IExec ((((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)),P,s)))) . a by Th6
.= (IExec ((((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)),P,s)) . a by A4, SCMFSA_2:63
.= (Exec ((a := b),(Exec (((FirstNotUsed (Macro (a := b))) := a),(Initialized s))))) . a by Th8
.= (Exec (((FirstNotUsed (Macro (a := b))) := a),(Initialized s))) . b by SCMFSA_2:63
.= (Initialized s) . b by A3, SCMFSA_2:63
.= s . b by SCMFSA_M:37 ; ::_thesis: verum
end;
supposeA5: a = b ; ::_thesis: (IExec ((swap (a,b)),P,s)) . a = s . b
thus (IExec ((swap (a,b)),P,s)) . a = (Exec ((b := (FirstNotUsed (Macro (a := b)))),(IExec ((((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)),P,s)))) . a by Th6
.= (IExec ((((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)),P,s)) . (FirstNotUsed (Macro (a := b))) by A5, SCMFSA_2:63
.= (Exec ((a := b),(Exec (((FirstNotUsed (Macro (a := b))) := a),(Initialized s))))) . (FirstNotUsed (Macro (a := b))) by Th8
.= (Exec (((FirstNotUsed (Macro (a := b))) := a),(Initialized s))) . (FirstNotUsed (Macro (a := b))) by A2, SCMFSA_2:63
.= (Initialized s) . a by SCMFSA_2:63
.= s . b by A5, SCMFSA_M:37 ; ::_thesis: verum
end;
end;
end;
thus (IExec ((swap (a,b)),P,s)) . b = (Exec ((b := (FirstNotUsed (Macro (a := b)))),(IExec ((((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)),P,s)))) . b by Th6
.= (IExec ((((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)),P,s)) . (FirstNotUsed (Macro (a := b))) by SCMFSA_2:63
.= (Exec ((a := b),(Exec (((FirstNotUsed (Macro (a := b))) := a),(Initialized s))))) . (FirstNotUsed (Macro (a := b))) by Th8
.= (Exec (((FirstNotUsed (Macro (a := b))) := a),(Initialized s))) . (FirstNotUsed (Macro (a := b))) by A2, SCMFSA_2:63
.= (Initialized s) . a by SCMFSA_2:63
.= s . a by SCMFSA_M:37 ; ::_thesis: verum
end;
theorem :: SCMFSA6C:11
for a, b being Int-Location holds UsedInt*Loc (swap (a,b)) = {}
proof
let a, b be Int-Location; ::_thesis: UsedInt*Loc (swap (a,b)) = {}
set i0 = (FirstNotUsed (Macro (a := b))) := a;
set i1 = a := b;
set i2 = b := (FirstNotUsed (Macro (a := b)));
thus UsedInt*Loc (swap (a,b)) = (UsedInt*Loc (((FirstNotUsed (Macro (a := b))) := a) ";" (a := b))) \/ (UsedInt*Loc (b := (FirstNotUsed (Macro (a := b))))) by SF_MASTR:46
.= (UsedInt*Loc (((FirstNotUsed (Macro (a := b))) := a) ";" (a := b))) \/ {} by SF_MASTR:32
.= (UsedInt*Loc ((FirstNotUsed (Macro (a := b))) := a)) \/ (UsedInt*Loc (a := b)) by SF_MASTR:47
.= (UsedInt*Loc ((FirstNotUsed (Macro (a := b))) := a)) \/ {} by SF_MASTR:32
.= {} by SF_MASTR:32 ; ::_thesis: verum
end;