:: 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;