:: On the Instructions of { \bf SCM+FSA } :: by Artur Korni{\l}owicz :: :: Received May 8, 2001 :: Copyright (c) 2001-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SCMFSA_2, AMI_3, AMI_1, FSM_1, INT_1, FUNCOP_1, SUBSET_1, SCMFSA_1, CAT_1, XBOOLE_0, GRAPHSP, FINSEQ_1, RELAT_1, CARD_1, AMI_2, AMISTD_2, CARD_3, FUNCT_1, AMISTD_1, CIRCUIT2, FUNCT_4, SETFAM_1, XXREAL_0, TARSKI, ARYTM_3, GOBOARD5, FRECHET, ARYTM_1, COMPLEX1, PARTFUN1, FINSEQ_2, RECDEF_2, NAT_1, COMPOS_1, GOBRD13, MEMSTR_0; notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, PARTFUN1, ORDINAL1, XCMPLX_0, INT_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, FUNCT_4, FUNCT_7, COMPLEX1, CARD_1, CARD_3, XXREAL_0, NAT_1, RECDEF_2, VALUED_1, NUMBERS, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMISTD_1, AMISTD_2, AMI_3, SCM_INST, SCMFSA_1, SCMFSA_3, SCMFSA_2; constructors REAL_1, NAT_D, AMI_3, SCMFSA_3, AMISTD_2, RELSET_1, AMISTD_1, SCMFSA_1, PRE_POLY, FUNCT_7, DOMAIN_1; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, NUMBERS, XREAL_0, NAT_1, INT_1, SCMFSA_2, AMISTD_2, CARD_3, AMI_3, FUNCT_4, VALUED_0, EXTPRO_1, FUNCT_7, PRE_POLY, MEMSTR_0, CARD_1, COMPOS_0, XTUPLE_0, FINSEQ_1; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; definitions TARSKI, AMISTD_1, AMISTD_2, XBOOLE_0, COMPOS_0; equalities SCMFSA_2, AMISTD_1, FUNCOP_1, COMPOS_1, EXTPRO_1, AMI_3, NAT_1, MEMSTR_0, COMPOS_0; expansions AMISTD_1, XBOOLE_0; theorems TARSKI, NAT_1, AMI_3, FUNCT_4, FUNCT_1, FUNCOP_1, SETFAM_1, AMISTD_1, FINSEQ_1, FUNCT_7, CARD_3, SCMFSA_2, INT_1, BVFUNC14, ABSVALUE, FINSEQ_2, XBOOLE_0, XBOOLE_1, NAT_D, MEMSTR_0, PARTFUN1, PBOOLE, VALUED_1, EXTPRO_1, AMI_2, COMPOS_0, ORDINAL1; begin reserve a, b, d1, d2, d3, d4 for Int-Location, A, B for Data-Location, f, f1, f2, f3 for FinSeq-Location, il, i1, i2 for Nat, L for Nat, I for Instruction of SCM+FSA, s,s1,s2 for State of SCM+FSA, T for InsType of the InstructionsF of SCM+FSA, k for Nat; definition let la, lb be Int-Location, a, b be Integer; redefine func (la,lb) --> (a,b) -> PartState of SCM+FSA; coherence proof A1: Values lb = INT by SCMFSA_2:11; b is Element of INT by INT_1:def 2; then reconsider b as Element of Values lb by A1; A2: Values la = INT by SCMFSA_2:11; a is Element of INT by INT_1:def 2; then reconsider a as Element of Values la by A2; (la,lb) --> (a,b) is PartState of SCM+FSA; hence thesis; end; end; theorem Th1: for o being Object of SCM+FSA st o in Data-Locations SCM+FSA holds o is Int-Location or o is FinSeq-Location proof let o be Object of SCM+FSA; assume o in Data-Locations SCM+FSA; then o in SCM-Data-Loc or o in SCM+FSA-Data*-Loc by SCMFSA_2:100,XBOOLE_0:def 3; hence thesis by AMI_2:def 16,SCMFSA_2:def 5; end; theorem Th2: a := b = [1,{},<*a,b*>] proof ex A,B st a = A & b = B & a := b = A:=B by SCMFSA_2:def 8; hence thesis; end; theorem Th3: AddTo(a,b) = [2,{},<*a,b*>] proof ex A,B st a = A & b = B & AddTo(a,b) = AddTo(A,B) by SCMFSA_2:def 9; hence thesis; end; theorem Th4: SubFrom(a,b) = [3,{},<* a,b *>] proof ex A,B st a = A & b = B & SubFrom(a,b) = SubFrom(A,B) by SCMFSA_2:def 10; hence thesis; end; theorem Th5: MultBy(a,b) = [4,{},<* a,b *>] proof ex A,B st a = A & b = B & MultBy(a,b) = MultBy(A,B) by SCMFSA_2:def 11; hence thesis; end; theorem Th6: Divide(a,b) = [5,{},<* a,b *>] proof ex A,B st a = A & b = B & Divide(a,b) = Divide(A,B) by SCMFSA_2:def 12; hence thesis; end; theorem Th7: a=0_goto il = [7, <* il*>,<*a *>] proof ex A st A = a & A=0_goto il = a=0_goto il by SCMFSA_2:def 14; hence thesis; end; theorem Th8: a>0_goto il = [8, <* il*>,<*a *>] proof ex A st A = a & A>0_goto il = a>0_goto il by SCMFSA_2:def 15; hence thesis; end; reserve J,K for Element of Segm 13, b,b1,c,c1 for Element of SCM-Data-Loc, f,f1 for Element of SCM+FSA-Data*-Loc; theorem Th9: JumpPart halt SCM+FSA = {}; reserve a, b, d1, d2, d3, d4 for Int-Location, A, B for Data-Location, f, f1, f2, f3 for FinSeq-Location; theorem Th10: JumpPart (a:=b) = {} proof thus JumpPart (a:=b) = [ 1,{}, <*a,b*>]`2_3 by Th2 .= {}; end; theorem Th11: JumpPart AddTo(a,b) = {} proof thus JumpPart AddTo(a,b) = [ 2,{}, <*a,b*>]`2_3 by Th3 .= {}; end; theorem Th12: JumpPart SubFrom(a,b) = {} proof thus JumpPart SubFrom(a,b) = [ 3,{}, <*a,b*>]`2_3 by Th4 .= {}; end; theorem Th13: JumpPart MultBy(a,b) = {} proof thus JumpPart MultBy(a,b) = [ 4,{}, <*a,b*>]`2_3 by Th5 .= {}; end; theorem Th14: JumpPart Divide(a,b) = {} proof thus JumpPart Divide(a,b) = [ 5,{}, <*a,b*>]`2_3 by Th6 .= {}; end; theorem Th15: JumpPart (a=0_goto i1) = <*i1*> proof thus JumpPart (a=0_goto i1) = [ 7,<*i1*>,<*a*>]`2_3 by Th7 .= <*i1*>; end; theorem Th16: JumpPart (a>0_goto i1) = <*i1*> proof thus JumpPart (a>0_goto i1) = [ 8,<*i1*>,<*a*>]`2_3 by Th8 .= <*i1*>; end; theorem T = 0 implies JumpParts T = {0} proof assume A1: T = 0; hereby let a be object; assume a in JumpParts T; then consider I such that A2: a = JumpPart I and A3: InsCode I = T; I = halt SCM+FSA by A1,A3,SCMFSA_2:95; hence a in {0} by A2,TARSKI:def 1; end; let a be object; assume a in {0}; then A4: a = 0 by TARSKI:def 1; InsCode halt SCM+FSA = 0; hence thesis by A1,Th9,A4; end; theorem T = 1 implies JumpParts T = {{}} proof assume A1: T = 1; hereby let x be object; assume x in JumpParts T; then consider I being Instruction of SCM+FSA such that A2: x = JumpPart I and A3: InsCode I = T; consider a,b such that A4: I = a:=b by A1,A3,SCMFSA_2:30; x = {} by A2,Th10,A4; hence x in {{}} by TARSKI:def 1; end; set a = the Int-Location; let x be object; assume x in {{}}; then x = {} by TARSKI:def 1; then A5: x = JumpPart(a:= a) by Th10; InsCode(a:= a) = 1 by SCMFSA_2:18; hence thesis by A5,A1; end; theorem T = 2 implies JumpParts T = {{}} proof assume A1: T = 2; hereby let x be object; assume x in JumpParts T; then consider I being Instruction of SCM+FSA such that A2: x = JumpPart I and A3: InsCode I = T; consider a,b such that A4: I = AddTo(a,b) by A1,A3,SCMFSA_2:31; x = {} by A2,Th11,A4; hence x in {{}} by TARSKI:def 1; end; set a = the Int-Location; let x be object; assume x in {{}}; then x = {} by TARSKI:def 1; then A5: x = JumpPart AddTo(a,a) by Th11; InsCode AddTo(a,a) = 2 by SCMFSA_2:19; hence thesis by A5,A1; end; theorem T = 3 implies JumpParts T = {{}} proof assume A1: T = 3; hereby let x be object; assume x in JumpParts T; then consider I being Instruction of SCM+FSA such that A2: x = JumpPart I and A3: InsCode I = T; consider a,b such that A4: I = SubFrom(a,b) by A1,A3,SCMFSA_2:32; x = {} by A2,Th12,A4; hence x in {{}} by TARSKI:def 1; end; set a = the Int-Location; let x be object; assume x in {{}}; then x = {} by TARSKI:def 1; then A5: x = JumpPart SubFrom(a,a) by Th12; InsCode SubFrom(a,a) = 3 by SCMFSA_2:20; hence thesis by A5,A1; end; theorem T = 4 implies JumpParts T = {{}} proof assume A1: T = 4; hereby let x be object; assume x in JumpParts T; then consider I being Instruction of SCM+FSA such that A2: x = JumpPart I and A3: InsCode I = T; consider a,b such that A4: I = MultBy(a,b) by A1,A3,SCMFSA_2:33; x = {} by A2,Th13,A4; hence x in {{}} by TARSKI:def 1; end; set a = the Int-Location; let x be object; assume x in {{}}; then x = {} by TARSKI:def 1; then A5: x = JumpPart MultBy(a,a) by Th13; InsCode MultBy(a,a) = 4 by SCMFSA_2:21; hence thesis by A5,A1; end; theorem T = 5 implies JumpParts T = {{}} proof assume A1: T = 5; hereby let x be object; assume x in JumpParts T; then consider I being Instruction of SCM+FSA such that A2: x = JumpPart I and A3: InsCode I = T; consider a,b such that A4: I = Divide(a,b) by A1,A3,SCMFSA_2:34; x = {} by A2,Th14,A4; hence x in {{}} by TARSKI:def 1; end; set a = the Int-Location; let x be object; assume x in {{}}; then x = {} by TARSKI:def 1; then A5: x = JumpPart Divide(a,a) by Th14; InsCode Divide(a,a) = 5 by SCMFSA_2:22; hence thesis by A5,A1; end; theorem Th23: T = 6 implies dom product" JumpParts T = {1} proof set i1 = the Nat; assume A1: T = 6; hereby let x be object; InsCode goto i1 = 6; then A2: JumpPart goto i1 in JumpParts T by A1; assume x in dom product" JumpParts T; then x in DOM JumpParts T by CARD_3:def 12; then x in dom JumpPart goto i1 by A2,CARD_3:108; hence x in {1} by FINSEQ_1:2,def 8; end; let x be object; assume A3: x in {1}; for f being Function st f in JumpParts T holds x in dom f proof let f be Function; assume f in JumpParts T; then consider I being Instruction of SCM+FSA such that A4: f = JumpPart I and A5: InsCode I = T; consider i1 such that A6: I = goto i1 by A1,A5,SCMFSA_2:35; f = <*i1*> by A4,A6; hence thesis by A3,FINSEQ_1:2,def 8; end; then x in DOM JumpParts T by CARD_3:109; hence thesis by CARD_3:def 12; end; theorem Th24: T = 7 implies dom product" JumpParts T = {1} proof set i1 = the Nat,a = the Int-Location; assume A1: T = 7; A2: JumpPart (a =0_goto i1) = <*i1*> by Th15; hereby let x be object; InsCode (a =0_goto i1) = 7 by SCMFSA_2:24; then A3: JumpPart (a =0_goto i1) in JumpParts T by A1; assume x in dom product" JumpParts T; then x in DOM JumpParts T by CARD_3:def 12; then x in dom JumpPart (a =0_goto i1) by A3,CARD_3:108; hence x in {1} by A2,FINSEQ_1:2,38; end; let x be object; assume A4: x in {1}; for f being Function st f in JumpParts T holds x in dom f proof let f be Function; assume f in JumpParts T; then consider I being Instruction of SCM+FSA such that A5: f = JumpPart I and A6: InsCode I = T; consider i1, a such that A7: I = a =0_goto i1 by A1,A6,SCMFSA_2:36; f = <*i1*> by A5,A7,Th15; hence thesis by A4,FINSEQ_1:2,38; end; then x in DOM JumpParts T by CARD_3:109; hence thesis by CARD_3:def 12; end; theorem Th25: T = 8 implies dom product" JumpParts T = {1} proof set i1 = the Nat,a = the Int-Location; assume A1: T = 8; A2: JumpPart (a >0_goto i1) = <*i1*> by Th16; hereby let x be object; InsCode (a >0_goto i1) = 8 by SCMFSA_2:25; then A3: JumpPart (a >0_goto i1) in JumpParts T by A1; assume x in dom product" JumpParts T; then x in DOM JumpParts T by CARD_3:def 12; then x in dom JumpPart (a >0_goto i1) by A3,CARD_3:108; hence x in {1} by A2,FINSEQ_1:2,38; end; let x be object; assume A4: x in {1}; for f being Function st f in JumpParts T holds x in dom f proof let f be Function; assume f in JumpParts T; then consider I being Instruction of SCM+FSA such that A5: f = JumpPart I and A6: InsCode I = T; consider i1, a such that A7: I = a >0_goto i1 by A1,A6,SCMFSA_2:37; f = <*i1*> by A5,A7,Th16; hence thesis by A4,FINSEQ_1:2,38; end; then x in DOM JumpParts T by CARD_3:109; hence thesis by CARD_3:def 12; end; theorem T = 9 implies JumpParts T = {{}} proof assume A1: T = 9; hereby let x be object; assume x in JumpParts T; then consider I being Instruction of SCM+FSA such that A2: x = JumpPart I and A3: InsCode I = T; consider a,b,f such that A4: I = b:=(f,a) by A1,A3,SCMFSA_2:38; x = {} by A2,A4; hence x in {{}} by TARSKI:def 1; end; set a = the Int-Location, f = the FinSeq-Location; let x be object; assume x in {{}}; then x = {} by TARSKI:def 1; then A5: x = JumpPart(a:=(f,a)); InsCode(a:=(f,a)) = 9; hence thesis by A5,A1; end; theorem T = 10 implies JumpParts T = {{}} proof assume A1: T = 10; hereby let x be object; assume x in JumpParts T; then consider I being Instruction of SCM+FSA such that A2: x = JumpPart I and A3: InsCode I = T; consider a,b,f such that A4: I = (f,a):=b by A1,A3,SCMFSA_2:39; x = {} by A2,A4; hence x in {{}} by TARSKI:def 1; end; set a = the Int-Location, f = the FinSeq-Location; let x be object; assume x in {{}}; then x = {} by TARSKI:def 1; then A5: x = JumpPart((f,a):=a); InsCode((f,a):=a) = 10; hence thesis by A5,A1; end; theorem T = 11 implies JumpParts T = {{}} proof assume A1: T = 11; hereby let x be object; assume x in JumpParts T; then consider I being Instruction of SCM+FSA such that A2: x = JumpPart I and A3: InsCode I = T; consider a,f such that A4: I = a:=len f by A1,A3,SCMFSA_2:40; x = {} by A2,A4; hence x in {{}} by TARSKI:def 1; end; set a = the Int-Location, f = the FinSeq-Location; let x be object; assume x in {{}}; then x = {} by TARSKI:def 1; then A5: x = JumpPart(a:=len f); InsCode(a:=len f) = 11; hence thesis by A5,A1; end; theorem T = 12 implies JumpParts T = {{}} proof assume A1: T = 12; hereby let x be object; assume x in JumpParts T; then consider I being Instruction of SCM+FSA such that A2: x = JumpPart I and A3: InsCode I = T; consider a,f such that A4: I = f:=<0,...,0>a by A1,A3,SCMFSA_2:41; x = {} by A2,A4; hence x in {{}} by TARSKI:def 1; end; set a = the Int-Location, f = the FinSeq-Location; let x be object; assume x in {{}}; then x = {} by TARSKI:def 1; then A5: x = JumpPart(f:=<0,...,0>a); InsCode(f:=<0,...,0>a) = 12; hence thesis by A5,A1; end; theorem (product" JumpParts InsCode goto i1).1 = NAT proof dom product" JumpParts InsCode goto i1 = {1} by Th23; then A1: 1 in dom product" JumpParts InsCode goto i1 by TARSKI:def 1; hereby let x be object; assume x in (product" JumpParts InsCode goto i1).1; then x in pi(JumpParts InsCode goto i1,1) by A1,CARD_3:def 12; then consider g being Function such that A2: g in JumpParts InsCode goto i1 and A3: x = g.1 by CARD_3:def 6; consider I being Instruction of SCM+FSA such that A4: g = JumpPart I and A5: InsCode I = InsCode goto i1 by A2; consider i2 such that A6: I = goto i2 by A5,SCMFSA_2:35; g = <*i2*> by A4,A6; then x = i2 by A3,FINSEQ_1:def 8; hence x in NAT by ORDINAL1:def 12; end; let x be object; assume x in NAT; then reconsider x as Nat; A7: <*x*>.1 = x by FINSEQ_1:def 8; A8: InsCode goto i1 = InsCode goto x; JumpPart goto x = <*x*>; then <*x*> in JumpParts InsCode goto i1 by A8; then x in pi(JumpParts InsCode goto i1,1) by A7,CARD_3:def 6; hence thesis by A1,CARD_3:def 12; end; theorem (product" JumpParts InsCode (a =0_goto i1)).1 = NAT proof dom product" JumpParts InsCode (a =0_goto i1) = {1} by Th24,SCMFSA_2:24; then A1: 1 in dom product" JumpParts InsCode (a =0_goto i1) by TARSKI:def 1; hereby let x be object; assume x in (product" JumpParts InsCode (a =0_goto i1)).1; then x in pi(JumpParts InsCode (a =0_goto i1),1) by A1,CARD_3:def 12; then consider g being Function such that A2: g in JumpParts InsCode (a =0_goto i1) and A3: x = g.1 by CARD_3:def 6; consider I being Instruction of SCM+FSA such that A4: g = JumpPart I and A5: InsCode I = InsCode (a =0_goto i1) by A2; consider i2, b such that A6: I = b =0_goto i2 by A5,SCMFSA_2:24,36; g = <*i2*> qua FinSequence by A4,A6,Th15; then x = i2 by A3,FINSEQ_1:40; hence x in NAT by ORDINAL1:def 12; end; let x be object; assume x in NAT; then reconsider x as Element of NAT; A7: <*x*>.1 = x by FINSEQ_1:40; InsCode (a =0_goto i1) = 7 by SCMFSA_2:24; then A8: InsCode (a =0_goto i1) = InsCode (a =0_goto x) by SCMFSA_2:24; JumpPart (a =0_goto x) = <*x*> by Th15; then <*x*> in JumpParts InsCode (a =0_goto i1) by A8; then x in pi(JumpParts InsCode (a =0_goto i1),1) by A7,CARD_3:def 6; hence thesis by A1,CARD_3:def 12; end; theorem (product" JumpParts InsCode (a >0_goto i1)).1 = NAT proof dom product" JumpParts InsCode (a >0_goto i1) = {1} by Th25,SCMFSA_2:25; then A1: 1 in dom product" JumpParts InsCode (a >0_goto i1) by TARSKI:def 1; hereby let x be object; assume x in (product" JumpParts InsCode (a >0_goto i1)).1; then x in pi(JumpParts InsCode (a >0_goto i1),1) by A1,CARD_3:def 12; then consider g being Function such that A2: g in JumpParts InsCode (a >0_goto i1) and A3: x = g.1 by CARD_3:def 6; consider I being Instruction of SCM+FSA such that A4: g = JumpPart I and A5: InsCode I = InsCode (a >0_goto i1) by A2; consider i2, b such that A6: I = b >0_goto i2 by A5,SCMFSA_2:25,37; g = <*i2*> by A4,A6,Th16; then x = i2 by A3,FINSEQ_1:40; hence x in NAT by ORDINAL1:def 12; end; let x be object; assume x in NAT; then reconsider x as Element of NAT; A7: <*x*>.1 = x by FINSEQ_1:40; InsCode (a >0_goto i1) = 8 by SCMFSA_2:25; then A8: InsCode (a >0_goto i1) = InsCode (a >0_goto x) by SCMFSA_2:25; JumpPart (a >0_goto x) = <*x*> by Th16; then <*x*> in JumpParts InsCode (a >0_goto i1) by A8; then x in pi(JumpParts InsCode (a >0_goto i1),1) by A7,CARD_3:def 6; hence thesis by A1,CARD_3:def 12; end; Lm1: for i being Instruction of SCM+FSA holds (for l being Nat holds NIC(i,l)={l+1}) implies JUMP i is empty proof reconsider p=0, q=1 as Nat; let i be Instruction of SCM+FSA; assume A1: for l being Nat holds NIC(i,l)={l+1}; set X = the set of all NIC(i,f) where f is Nat; reconsider p, q as Nat; assume not thesis; then consider x being object such that A2: x in meet X; NIC(i,p) = {p + 1} by A1; then {p + 1} in X; then x in {p + 1} by A2,SETFAM_1:def 1; then A3: x = p + 1 by TARSKI:def 1; NIC(i,q) = {q + 1} by A1; then {q + 1} in X; then x in {q + 1} by A2,SETFAM_1:def 1; hence contradiction by A3,TARSKI:def 1; end; registration cluster JUMP halt SCM+FSA -> empty; coherence; end; registration let a, b; cluster a:=b -> sequential; coherence by SCMFSA_2:63; cluster AddTo(a,b) -> sequential; coherence by SCMFSA_2:64; cluster SubFrom(a,b) -> sequential; coherence by SCMFSA_2:65; cluster MultBy(a,b) -> sequential; coherence by SCMFSA_2:66; cluster Divide(a,b) -> sequential; coherence by SCMFSA_2:67; end; registration let a, b; cluster JUMP (a := b) -> empty; coherence proof for l being Nat holds NIC(a:=b,l)={l + 1} by AMISTD_1:12; hence thesis by Lm1; end; cluster JUMP AddTo(a, b) -> empty; coherence proof for l being Nat holds NIC(AddTo(a,b),l)={ l + 1 } by AMISTD_1:12; hence thesis by Lm1; end; cluster JUMP SubFrom(a, b) -> empty; coherence proof for l being Nat holds NIC(SubFrom(a,b),l)= {l + 1} by AMISTD_1:12; hence thesis by Lm1; end; cluster JUMP MultBy(a,b) -> empty; coherence proof for l being Nat holds NIC(MultBy(a,b),l)={ l + 1 } by AMISTD_1:12; hence thesis by Lm1; end; cluster JUMP Divide(a,b) -> empty; coherence proof for l being Nat holds NIC(Divide(a,b),l)={ l + 1 } by AMISTD_1:12; hence thesis by Lm1; end; end; theorem Th33: NIC(goto i1, il) = {i1} proof now let x be object; A1: now il in NAT by ORDINAL1:def 12; then reconsider il1 = il as Element of Values IC SCM+FSA by MEMSTR_0:def 6; reconsider n = il1 as Nat; set I = goto i1; set t = the State of SCM+FSA, Q = the Instruction-Sequence of SCM+FSA; assume A2: x = i1; reconsider u = t+*(IC SCM+FSA,il1) as Element of product the_Values_of SCM+FSA by CARD_3:107; reconsider P = Q +* (il,I) as Instruction-Sequence of SCM+FSA; IC SCM+FSA in dom t by MEMSTR_0:2; then A3: IC u = n by FUNCT_7:31; il in NAT by ORDINAL1:def 12; then A4: P/.il = P.il by PBOOLE:143; il in NAT by ORDINAL1:def 12; then il in dom Q by PARTFUN1:def 2; then A5: P.n = I by FUNCT_7:31; then IC Following(P,u) = i1 by A3,A4,SCMFSA_2:69; hence x in {IC Exec(goto i1,s) where s is Element of product the_Values_of SCM+FSA : IC s = il} by A2,A3,A5,A4; end; now assume x in {IC Exec(goto i1,s) where s is Element of product the_Values_of SCM+FSA : IC s = il}; then ex s being Element of product the_Values_of SCM+FSA st x = IC Exec(goto i1,s) & IC s = il; hence x = i1 by SCMFSA_2:69; end; hence x in {i1} iff x in {IC Exec(goto i1,s) where s is Element of product the_Values_of SCM+FSA : IC s = il} by A1,TARSKI:def 1; end; hence thesis by TARSKI:2; end; theorem Th34: JUMP goto i1 = {i1} proof set X = the set of all NIC(goto i1, il) ; now let x be object; hereby set il1 = 1; A1: NIC(goto i1, il1) in X; assume x in meet X; then x in NIC(goto i1, il1) by A1,SETFAM_1:def 1; hence x in {i1} by Th33; end; assume x in {i1}; then A2: x = i1 by TARSKI:def 1; A3: now let Y be set; assume Y in X; then consider il being Nat such that A4: Y = NIC(goto i1, il); NIC(goto i1, il) = {i1} by Th33; hence i1 in Y by A4,TARSKI:def 1; end; NIC(goto i1, i1) in X; hence x in meet X by A2,A3,SETFAM_1:def 1; end; hence thesis by TARSKI:2; end; registration let i1; cluster JUMP goto i1 -> 1-element; coherence proof JUMP goto i1 = {i1} by Th34; hence thesis; end; end; theorem Th35: NIC(a=0_goto i1, il) = {i1, il + 1} proof set t = the State of SCM+FSA, Q = the Instruction-Sequence of SCM+FSA; hereby let x be object; assume x in NIC(a=0_goto i1, il); then consider s being Element of product the_Values_of SCM+FSA such that A1: x = IC Exec(a=0_goto i1,s) and A2: IC s = il; per cases; suppose s.a = 0; then x = i1 by A1,SCMFSA_2:70; hence x in {i1, il + 1} by TARSKI:def 2; end; suppose s.a <> 0; then x = il + 1 by A1,A2,SCMFSA_2:70; hence x in {i1, il + 1} by TARSKI:def 2; end; end; let x be object; set I = a=0_goto i1; A3: IC SCM+FSA <> a by SCMFSA_2:56; il in NAT by ORDINAL1:def 12; then reconsider il1 = il as Element of Values IC SCM+FSA by MEMSTR_0:def 6; reconsider u = t+*(IC SCM+FSA,il1) as Element of product the_Values_of SCM+FSA by CARD_3:107; reconsider P = Q +* (il,I) as Instruction-Sequence of SCM+FSA; reconsider n = il as Nat; assume A4: x in {i1, il + 1}; per cases by A4,TARSKI:def 2; suppose A5: x = i1; reconsider v = u+*(a .--> 0) as Element of product the_Values_of SCM+FSA by CARD_3:107; A6: IC SCM+FSA in dom t by MEMSTR_0:2; not IC SCM+FSA in dom (a .--> 0) by A3,TARSKI:def 1; then A8: IC v = IC u by FUNCT_4:11 .= n by A6,FUNCT_7:31; il in NAT by ORDINAL1:def 12; then A9: P/.il = P.il by PBOOLE:143; il in NAT by ORDINAL1:def 12; then il in dom Q by PARTFUN1:def 2; then A10: P.il = I by FUNCT_7:31; a in dom (a .--> 0) by TARSKI:def 1; then v.a = (a .--> 0).a by FUNCT_4:13 .= 0 by FUNCOP_1:72; then IC Following(P,v) = i1 by A8,A10,A9,SCMFSA_2:70; hence thesis by A5,A8,A10,A9; end; suppose A11: x = il + 1; reconsider v = u+*(a .--> 1) as Element of product the_Values_of SCM+FSA by CARD_3:107; A12: IC SCM+FSA in dom t by MEMSTR_0:2; not IC SCM+FSA in dom (a .--> 1) by A3,TARSKI:def 1; then A14: IC v = IC u by FUNCT_4:11 .= n by A12,FUNCT_7:31; il in NAT by ORDINAL1:def 12; then A15: P/.il = P.il by PBOOLE:143; il in NAT by ORDINAL1:def 12; then il in dom Q by PARTFUN1:def 2; then A16: P.il = I by FUNCT_7:31; a in dom (a .--> 1) by TARSKI:def 1; then v.a = (a .--> 1).a by FUNCT_4:13 .= 1 by FUNCOP_1:72; then IC Following(P,v) = il + 1 by A14,A16,A15,SCMFSA_2:70; hence thesis by A11,A14,A16,A15; end; end; theorem Th36: JUMP (a=0_goto i1) = {i1} proof set X = the set of all NIC(a=0_goto i1, il) ; now let x be object; A1: now let Y be set; assume Y in X; then consider il being Nat such that A2: Y = NIC(a=0_goto i1, il); NIC(a=0_goto i1, il) = {i1, il + 1} by Th35; hence i1 in Y by A2,TARSKI:def 2; end; hereby set il1 = 1, il2 = 2; assume A3: x in meet X; A4: NIC(a=0_goto i1, il2) = {i1, il2 + 1} by Th35; NIC(a=0_goto i1, il2) in X; then x in NIC(a=0_goto i1, il2) by A3,SETFAM_1:def 1; then A5: x = i1 or x = il2 + 1 by A4,TARSKI:def 2; A6: NIC(a=0_goto i1, il1) = {i1, il1 + 1} by Th35; NIC(a=0_goto i1, il1) in X; then x in NIC(a=0_goto i1, il1) by A3,SETFAM_1:def 1; then x = i1 or x = il1 + 1 by A6,TARSKI:def 2; hence x in {i1} by A5,TARSKI:def 1; end; assume x in {i1}; then A7: x = i1 by TARSKI:def 1; NIC(a=0_goto i1, i1) in X; hence x in meet X by A7,A1,SETFAM_1:def 1; end; hence thesis by TARSKI:2; end; registration let a, i1; cluster JUMP (a =0_goto i1) -> 1-element; coherence proof JUMP (a =0_goto i1) = {i1} by Th36; hence thesis; end; end; theorem Th37: NIC(a>0_goto i1, il) = {i1, il + 1} proof set t = the State of SCM+FSA, Q = the Instruction-Sequence of SCM+FSA; hereby let x be object; assume x in NIC(a>0_goto i1, il); then consider s being Element of product the_Values_of SCM+FSA such that A1: x = IC Exec(a>0_goto i1,s) and A2: IC s = il; per cases; suppose s.a > 0; then x = i1 by A1,SCMFSA_2:71; hence x in {i1, il + 1} by TARSKI:def 2; end; suppose s.a <= 0; then x = il + 1 by A1,A2,SCMFSA_2:71; hence x in {i1, il + 1} by TARSKI:def 2; end; end; let x be object; set I = a>0_goto i1; A3: IC SCM+FSA <> a by SCMFSA_2:56; il in NAT by ORDINAL1:def 12; then reconsider il1 = il as Element of Values IC SCM+FSA by MEMSTR_0:def 6; reconsider n = il as Nat; reconsider u = t+*(IC SCM+FSA,il1) as Element of product the_Values_of SCM+FSA by CARD_3:107; reconsider P = Q +* (il,I) as Instruction-Sequence of SCM+FSA; assume A4: x in {i1, il + 1}; per cases by A4,TARSKI:def 2; suppose A5: x = i1; reconsider v = u+*(a .--> 1) as Element of product the_Values_of SCM+FSA by CARD_3:107; A6: IC SCM+FSA in dom t by MEMSTR_0:2; not IC SCM+FSA in dom (a .--> 1) by A3,TARSKI:def 1; then A8: IC v = IC u by FUNCT_4:11 .= n by A6,FUNCT_7:31; il in NAT by ORDINAL1:def 12; then A9: P/.il = P.il by PBOOLE:143; il in NAT by ORDINAL1:def 12; then il in dom Q by PARTFUN1:def 2; then A10: P.il = I by FUNCT_7:31; a in dom (a .--> 1) by TARSKI:def 1; then v.a = (a .--> 1).a by FUNCT_4:13 .= 1 by FUNCOP_1:72; then IC Following(P,v) = i1 by A8,A10,A9,SCMFSA_2:71; hence thesis by A5,A8,A10,A9; end; suppose A11: x = il + 1; reconsider v = u+*(a .--> 0) as Element of product the_Values_of SCM+FSA by CARD_3:107; A12: IC SCM+FSA in dom t by MEMSTR_0:2; not IC SCM+FSA in dom (a .--> 0) by A3,TARSKI:def 1; then A14: IC v = IC u by FUNCT_4:11 .= n by A12,FUNCT_7:31; il in NAT by ORDINAL1:def 12; then A15: P/.il = P.il by PBOOLE:143; il in NAT by ORDINAL1:def 12; then il in dom Q by PARTFUN1:def 2; then A16: P.il = I by FUNCT_7:31; a in dom (a .--> 0) by TARSKI:def 1; then v.a = (a .--> 0).a by FUNCT_4:13 .= 0 by FUNCOP_1:72; then IC Following(P,v) = il + 1 by A14,A16,A15,SCMFSA_2:71; hence thesis by A11,A14,A16,A15; end; end; theorem Th38: JUMP (a>0_goto i1) = {i1} proof set X = the set of all NIC(a>0_goto i1, il) ; now let x be object; A1: now let Y be set; assume Y in X; then consider il being Nat such that A2: Y = NIC(a>0_goto i1, il); NIC(a>0_goto i1, il) = {i1, il + 1} by Th37; hence i1 in Y by A2,TARSKI:def 2; end; hereby set il1 = 1, il2 = 2; assume A3: x in meet X; A4: NIC(a>0_goto i1, il2) = {i1, il2 + 1} by Th37; NIC(a>0_goto i1, il2) in X; then x in NIC(a>0_goto i1, il2) by A3,SETFAM_1:def 1; then A5: x = i1 or x = il2 + 1 by A4,TARSKI:def 2; A6: NIC(a>0_goto i1, il1) = {i1, il1 + 1} by Th37; NIC(a>0_goto i1, il1) in X; then x in NIC(a>0_goto i1, il1) by A3,SETFAM_1:def 1; then x = i1 or x = il1 + 1 by A6,TARSKI:def 2; hence x in {i1} by A5,TARSKI:def 1; end; assume x in {i1}; then A7: x = i1 by TARSKI:def 1; NIC(a>0_goto i1, i1) in X; hence x in meet X by A7,A1,SETFAM_1:def 1; end; hence thesis by TARSKI:2; end; registration let a, i1; cluster JUMP (a >0_goto i1) -> 1-element; coherence proof JUMP (a >0_goto i1) = {i1} by Th38; hence thesis; end; end; registration let a, b, f; cluster a:=(f,b) -> sequential; coherence by SCMFSA_2:72; end; registration let a, b, f; cluster JUMP (a:=(f,b)) -> empty; coherence proof for l being Nat holds NIC(a:=(f,b),l)={ l + 1} by AMISTD_1:12; hence thesis by Lm1; end; end; registration let a, b, f; cluster (f,b):=a -> sequential; coherence by SCMFSA_2:73; end; registration let a, b, f; cluster JUMP ((f,b):=a) -> empty; coherence proof for l being Nat holds NIC((f,b):=a,l)={ l + 1} by AMISTD_1:12; hence thesis by Lm1; end; end; registration let a, f; cluster a:=len f -> sequential; coherence by SCMFSA_2:74; end; registration let a, f; cluster JUMP (a:=len f) -> empty; coherence proof for l being Nat holds NIC(a:=len f,l)={ l + 1} by AMISTD_1:12; hence thesis by Lm1; end; end; registration let a, f; cluster f:=<0,...,0>a -> sequential; coherence by SCMFSA_2:75; end; registration let a, f; cluster JUMP (f:=<0,...,0>a) -> empty; coherence proof for l being Nat holds NIC(f:=<0,...,0>a,l) ={l + 1} by AMISTD_1:12; hence thesis by Lm1; end; end; theorem Th39: SUCC(il,SCM+FSA) = {il, il + 1} proof set X = the set of all NIC(I, il) \ JUMP I where I is Element of the InstructionsF of SCM+FSA; set N = {il, il + 1}; now let x be object; hereby assume x in union X; then consider Y being set such that A1: x in Y and A2: Y in X by TARSKI:def 4; consider i being Element of the InstructionsF of SCM+FSA such that A3: Y = NIC(i, il) \ JUMP i by A2; per cases by SCMFSA_2:93; suppose i = [0,{},{}]; then x in {il} \ JUMP halt SCM+FSA by A1,A3,AMISTD_1:2; then x = il by TARSKI:def 1; hence x in N by TARSKI:def 2; end; suppose ex a,b st i = a:=b; then consider a, b such that A4: i = a:=b; x in {il + 1} \ JUMP (a:=b) by A1,A3,A4,AMISTD_1:12; then x = il + 1 by TARSKI:def 1; hence x in N by TARSKI:def 2; end; suppose ex a,b st i = AddTo(a,b); then consider a, b such that A5: i = AddTo(a,b); x in {il + 1} \ JUMP AddTo(a,b) by A1,A3,A5,AMISTD_1:12; then x = il + 1 by TARSKI:def 1; hence x in N by TARSKI:def 2; end; suppose ex a,b st i = SubFrom(a,b); then consider a, b such that A6: i = SubFrom(a,b); x in {il + 1} \ JUMP SubFrom(a,b) by A1,A3,A6,AMISTD_1:12; then x = il + 1 by TARSKI:def 1; hence x in N by TARSKI:def 2; end; suppose ex a,b st i = MultBy(a,b); then consider a, b such that A7: i = MultBy(a,b); x in {il + 1} \ JUMP MultBy(a,b) by A1,A3,A7,AMISTD_1:12; then x = il + 1 by TARSKI:def 1; hence x in N by TARSKI:def 2; end; suppose ex a,b st i = Divide(a,b); then consider a, b such that A8: i = Divide(a,b); x in {il + 1} \ JUMP Divide(a,b) by A1,A3,A8,AMISTD_1:12; then x = il + 1 by TARSKI:def 1; hence x in N by TARSKI:def 2; end; suppose ex i1 st i = goto i1; then consider i1 such that A9: i = goto i1; x in {i1} \ JUMP i by A1,A3,A9,Th33; then x in {i1} \ {i1} by A9,Th34; hence x in N by XBOOLE_1:37; end; suppose ex i1,a st i = a=0_goto i1; then consider i1, a such that A10: i = a=0_goto i1; A11: NIC(i, il) = {i1, il + 1} by A10,Th35; x in NIC(i, il) by A1,A3,XBOOLE_0:def 5; then A12: x = i1 or x = il + 1 by A11,TARSKI:def 2; x in NIC(i, il) \ {i1} by A1,A3,A10,Th36; then not x in {i1} by XBOOLE_0:def 5; hence x in N by A12,TARSKI:def 1,def 2; end; suppose ex i1,a st i = a>0_goto i1; then consider i1, a such that A13: i = a>0_goto i1; A14: NIC(i, il) = {i1, il + 1} by A13,Th37; x in NIC(i, il) by A1,A3,XBOOLE_0:def 5; then A15: x = i1 or x = il + 1 by A14,TARSKI:def 2; x in NIC(i, il) \ {i1} by A1,A3,A13,Th38; then not x in {i1} by XBOOLE_0:def 5; hence x in N by A15,TARSKI:def 1,def 2; end; suppose ex a,b,f st i = b:=(f,a); then consider a, b, f such that A16: i = b:=(f,a); x in {il + 1} \ JUMP (b:=(f,a)) by A1,A3,A16,AMISTD_1:12; then x = il + 1 by TARSKI:def 1; hence x in N by TARSKI:def 2; end; suppose ex a,b,f st i = (f,a):=b; then consider a, b, f such that A17: i = (f,a):=b; x in {il + 1} \ JUMP ((f,a):=b) by A1,A3,A17,AMISTD_1:12; then x = il + 1 by TARSKI:def 1; hence x in N by TARSKI:def 2; end; suppose ex a,f st i = a:=len f; then consider a, f such that A18: i = a:=len f; x in {il + 1} \ JUMP (a:=len f) by A1,A3,A18,AMISTD_1:12; then x = il + 1 by TARSKI:def 1; hence x in N by TARSKI:def 2; end; suppose ex a,f st i = f:=<0,...,0>a; then consider a, f such that A19: i = f:=<0,...,0>a; x in {il + 1} \ JUMP (f:=<0,...,0>a) by A1,A3,A19,AMISTD_1:12; then x = il + 1 by TARSKI:def 1; hence x in N by TARSKI:def 2; end; end; assume A20: x in {il, il + 1}; per cases by A20,TARSKI:def 2; suppose A21: x = il; set i = halt SCM+FSA; NIC(i, il) \ JUMP i = {il} by AMISTD_1:2; then A22: {il} in X; x in {il} by A21,TARSKI:def 1; hence x in union X by A22,TARSKI:def 4; end; suppose A23: x = il + 1; set a = the Int-Location; set i = AddTo(a,a); NIC(i, il) \ JUMP i = {il + 1} by AMISTD_1:12; then A24: {il + 1} in X; x in {il + 1} by A23,TARSKI:def 1; hence x in union X by A24,TARSKI:def 4; end; end; hence thesis by TARSKI:2; end; theorem Th40: for k being Nat holds k+1 in SUCC(k,SCM+FSA) & for j being Nat st j in SUCC(k,SCM+FSA) holds k <= j proof let k be Nat; A1: SUCC(k,SCM+FSA) = {k, k+1} by Th39; hence k+1 in SUCC(k,SCM+FSA) by TARSKI:def 2; let j be Nat; assume A2: j in SUCC(k,SCM+FSA); per cases by A1,A2,TARSKI:def 2; suppose j = k; hence thesis; end; suppose j = k + 1; hence thesis by NAT_1:11; end; end; registration cluster SCM+FSA -> standard; coherence by Th40,AMISTD_1:3; end; registration cluster InsCode halt SCM+FSA -> jump-only for InsType of the InstructionsF of SCM+FSA; coherence proof now let s be State of SCM+FSA, o be Object of SCM+FSA, I be Instruction of SCM+FSA; assume that A1: InsCode I = InsCode halt SCM+FSA and o in Data-Locations SCM+FSA; I = halt SCM+FSA by A1,SCMFSA_2:95; hence Exec(I, s).o = s.o by EXTPRO_1:def 3; end; hence thesis; end; end; registration cluster halt SCM+FSA -> jump-only; coherence; end; registration let i1; cluster InsCode goto i1 -> jump-only for InsType of the InstructionsF of SCM+FSA; coherence proof set S = SCM+FSA; now let s be State of S, o be Object of S, I be Instruction of S; assume that A1: InsCode I = InsCode goto i1 and A2: o in Data-Locations S; A3: ex i2 st I = goto i2 by A1,SCMFSA_2:35; per cases by A2,Th1; suppose o is Int-Location; hence Exec(I, s).o = s.o by A3,SCMFSA_2:69; end; suppose o is FinSeq-Location; hence Exec(I, s).o = s.o by A3,SCMFSA_2:69; end; end; hence thesis; end; end; registration let i1; cluster goto i1 -> jump-only non sequential non ins-loc-free; coherence proof thus InsCode goto i1 is jump-only; JUMP goto i1 <> {}; hence goto i1 is non sequential by AMISTD_1:13; thus JumpPart goto i1 is not empty; end; end; registration let a, i1; cluster InsCode (a =0_goto i1) -> jump-only for InsType of the InstructionsF of SCM+FSA; coherence proof set S = SCM+FSA; now let s be State of S, o be Object of S, I be Instruction of S; assume that A1: InsCode I = InsCode (a =0_goto i1) and A2: o in Data-Locations S; A3: ex i2, b st I = b =0_goto i2 by A1,SCMFSA_2:24,36; per cases by A2,Th1; suppose o is Int-Location; hence Exec(I, s).o = s.o by A3,SCMFSA_2:70; end; suppose o is FinSeq-Location; hence Exec(I, s).o = s.o by A3,SCMFSA_2:70; end; end; hence thesis; end; cluster InsCode (a >0_goto i1) -> jump-only for InsType of the InstructionsF of SCM+FSA; coherence proof set S = SCM+FSA; now let s be State of S, o be Object of S, I be Instruction of S; assume that A4: InsCode I = InsCode (a >0_goto i1) and A5: o in Data-Locations S; A6: ex i2, b st I = b >0_goto i2 by A4,SCMFSA_2:25,37; per cases by A5,Th1; suppose o is Int-Location; hence Exec(I, s).o = s.o by A6,SCMFSA_2:71; end; suppose o is FinSeq-Location; hence Exec(I, s).o = s.o by A6,SCMFSA_2:71; end; end; hence thesis; end; end; registration let a, i1; cluster a =0_goto i1 -> jump-only non sequential non ins-loc-free; coherence proof thus InsCode (a =0_goto i1) is jump-only; JUMP (a =0_goto i1) <> {}; hence a =0_goto i1 is non sequential by AMISTD_1:13; dom JumpPart (a =0_goto i1) = dom <*i1*> by Th15 .= {1} by FINSEQ_1:2,38; hence JumpPart(a =0_goto i1) is not empty; end; cluster a >0_goto i1 -> jump-only non sequential non ins-loc-free; coherence proof thus InsCode (a >0_goto i1) is jump-only; JUMP (a >0_goto i1) <> {}; hence a >0_goto i1 is non sequential by AMISTD_1:13; dom JumpPart (a >0_goto i1) = dom <*i1*> by Th16 .= {1} by FINSEQ_1:2,38; hence JumpPart(a >0_goto i1) is not empty; end; end; Lm2: intloc 0 <> intloc 1 by AMI_3:10; registration let a, b; cluster InsCode (a:=b) -> non jump-only for InsType of the InstructionsF of SCM+FSA; coherence proof set w = the State of SCM+FSA; set t = w+*((intloc 0, intloc 1)-->(0,1)); A1: InsCode (a:=b) = 1 by SCMFSA_2:18 .= InsCode (intloc 0:=intloc 1) by SCMFSA_2:18; A2: dom ((intloc 0, intloc 1)-->(0,1)) = {intloc 0, intloc 1} by FUNCT_4:62; then A3: intloc 1 in dom ((intloc 0, intloc 1)-->(0,1)) by TARSKI:def 2; intloc 0 in dom ((intloc 0, intloc 1)-->(0,1)) by A2,TARSKI:def 2; then A4: t.intloc 0 = (intloc 0, intloc 1)-->(0,1).intloc 0 by FUNCT_4:13 .= 0 by AMI_3:10,FUNCT_4:63; intloc 0 in Int-Locations by AMI_2:def 16; then A5: intloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3; Exec((intloc 0:=intloc 1), t).intloc 0 = t.intloc 1 by SCMFSA_2:63 .= (intloc 0, intloc 1)-->(0,1).intloc 1 by A3,FUNCT_4:13 .= 1 by FUNCT_4:63; hence thesis by A1,A4,A5; end; cluster InsCode AddTo(a,b) -> non jump-only for InsType of the InstructionsF of SCM+FSA; coherence proof set w = the State of SCM+FSA; set t = w+*((intloc 0, intloc 1)-->(0,1)); A6: InsCode AddTo(a,b) = 2 by SCMFSA_2:19 .= InsCode AddTo(intloc 0, intloc 1) by SCMFSA_2:19; A7: dom ((intloc 0, intloc 1)-->(0,1)) = {intloc 0, intloc 1} by FUNCT_4:62; then intloc 0 in dom ((intloc 0, intloc 1)-->(0,1)) by TARSKI:def 2; then A8: t.intloc 0 = (intloc 0, intloc 1)-->(0,1).intloc 0 by FUNCT_4:13 .= 0 by AMI_3:10,FUNCT_4:63; intloc 0 in Int-Locations by AMI_2:def 16; then A9: intloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3; intloc 1 in dom ((intloc 0, intloc 1)-->(0,1)) by A7,TARSKI:def 2; then t.intloc 1 = (intloc 0, intloc 1)-->(0,1).intloc 1 by FUNCT_4:13 .= 1 by FUNCT_4:63; then Exec(AddTo(intloc 0, intloc 1), t).intloc 0 = (0 qua Nat)+1 by A8,SCMFSA_2:64; hence thesis by A6,A8,A9; end; cluster InsCode SubFrom(a,b) -> non jump-only for InsType of the InstructionsF of SCM+FSA; coherence proof set w = the State of SCM+FSA; set t = w+*((intloc 0, intloc 1)-->(0,1)); A10: InsCode SubFrom(a,b) = 3 by SCMFSA_2:20 .= InsCode SubFrom(intloc 0, intloc 1) by SCMFSA_2:20; A11: dom ((intloc 0, intloc 1)-->(0,1)) = {intloc 0, intloc 1} by FUNCT_4:62; then intloc 0 in dom ((intloc 0, intloc 1)-->(0,1)) by TARSKI:def 2; then A12: t.intloc 0 = (intloc 0, intloc 1)-->(0,1).intloc 0 by FUNCT_4:13 .= 0 by AMI_3:10,FUNCT_4:63; intloc 0 in Int-Locations by AMI_2:def 16; then A13: intloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3; intloc 1 in dom ((intloc 0, intloc 1)-->(0,1)) by A11,TARSKI:def 2; then A14: t.intloc 1 = (intloc 0, intloc 1)-->(0,1).intloc 1 by FUNCT_4:13 .= 1 by FUNCT_4:63; Exec(SubFrom(intloc 0, intloc 1), t).intloc 0 = t.intloc 0 - t.intloc 1 by SCMFSA_2:65 .= -1 by A12,A14; hence thesis by A10,A12,A13; end; cluster InsCode MultBy(a,b) -> non jump-only for InsType of the InstructionsF of SCM+FSA; coherence proof set w = the State of SCM+FSA; set t = w+*((intloc 0, intloc 1)-->(1,0)); A15: InsCode MultBy(a,b) = 4 by SCMFSA_2:21 .= InsCode MultBy(intloc 0, intloc 1) by SCMFSA_2:21; A16: dom ((intloc 0, intloc 1)-->(1,0)) = {intloc 0, intloc 1} by FUNCT_4:62; then intloc 0 in dom ((intloc 0, intloc 1)-->(1,0)) by TARSKI:def 2; then A17: t.intloc 0 = (intloc 0, intloc 1)-->(1,0).intloc 0 by FUNCT_4:13 .= 1 by AMI_3:10,FUNCT_4:63; intloc 0 in Int-Locations by AMI_2:def 16; then A18: intloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3; intloc 1 in dom ((intloc 0, intloc 1)-->(1,0)) by A16,TARSKI:def 2; then A19: t.intloc 1 = (intloc 0, intloc 1)-->(1,0).intloc 1 by FUNCT_4:13 .= 0 by FUNCT_4:63; Exec(MultBy(intloc 0, intloc 1), t).intloc 0 = t.intloc 0 * t.intloc 1 by SCMFSA_2:66 .= 0 by A19; hence thesis by A15,A17,A18; end; cluster InsCode Divide(a,b) -> non jump-only for InsType of the InstructionsF of SCM+FSA; coherence proof set w = the State of SCM+FSA; set t = w+*((intloc 0, intloc 1)-->(7,3)); A20: InsCode Divide(a,b) = 5 by SCMFSA_2:22 .= InsCode Divide(intloc 0, intloc 1) by SCMFSA_2:22; A21: dom ((intloc 0, intloc 1)-->(7,3)) = {intloc 0, intloc 1} by FUNCT_4:62; then intloc 0 in dom ((intloc 0, intloc 1)-->(7,3)) by TARSKI:def 2; then A22: t.intloc 0 = (intloc 0, intloc 1)-->(7,3).intloc 0 by FUNCT_4:13 .= 7 by AMI_3:10,FUNCT_4:63; A23: 7 = 2 * 3 + 1; intloc 0 in Int-Locations by AMI_2:def 16; then A24: intloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3; intloc 1 in dom ((intloc 0, intloc 1)-->(7,3)) by A21,TARSKI:def 2; then t.intloc 1 = (intloc 0, intloc 1)-->(7,3).intloc 1 by FUNCT_4:13 .= 3 by FUNCT_4:63; then Exec(Divide(intloc 0, intloc 1), t).intloc 0 = 7 div (3 qua Element of NAT) by A22,Lm2,SCMFSA_2:67 .= 2 by A23,NAT_D:def 1; hence thesis by A20,A22,A24; end; end; Lm3: fsloc 0 <> intloc 0 by SCMFSA_2:99; Lm4: fsloc 0 <> intloc 1 by SCMFSA_2:99; registration let a, b, f; cluster InsCode (b:=(f,a)) -> non jump-only for InsType of the InstructionsF of SCM+FSA; coherence proof Values intloc 1 = INT by SCMFSA_2:11; then reconsider E = 1 as Element of Values intloc 1 by INT_1:def 1; Values intloc 0 = INT by SCMFSA_2:11; then reconsider D = 1 as Element of Values intloc 0 by INT_1:def 1; reconsider DWA = 2 as Element of INT by INT_1:def 1; set w = the State of SCM+FSA; <*DWA*> in INT* by FINSEQ_1:def 11; then reconsider F = <*2*> as Element of Values fsloc 0 by SCMFSA_2:12; reconsider t = w+*(fsloc 0 .--> F)+*(intloc 0 .--> D)+*(intloc 1 .--> E) as State of SCM+FSA; A1: t.intloc 0 = D by AMI_3:10,BVFUNC14:12; A2: t.fsloc 0 = F by Lm3,Lm4,FUNCT_7:114; then dom (t.fsloc 0) = {1} by FINSEQ_1:2,def 8; then A3: 1 in dom (t.fsloc 0) by TARSKI:def 1; consider k being Nat such that A4: k = |. t.intloc 1 .| and A5: Exec((intloc 0):=(fsloc 0, intloc 1), t).intloc 0 = (t.fsloc 0) /. k by SCMFSA_2:72; intloc 0 in Int-Locations by AMI_2:def 16; then A6: intloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3; t.intloc 1 = E by FUNCT_7:94; then k = 1 by A4,ABSVALUE:def 1; then A7: Exec(intloc 0:=(fsloc 0, intloc 1), t).intloc 0 = (t.fsloc 0).1 by A5,A3, PARTFUN1:def 6 .= 2 by A2,FINSEQ_1:def 8; InsCode (b:=(f,a)) = 9 .= InsCode ((intloc 0):=(fsloc 0, intloc 1)); hence thesis by A1,A7,A6; end; cluster InsCode ((f,a):=b) -> non jump-only for InsType of the InstructionsF of SCM+FSA; coherence proof Values intloc 0 = INT by SCMFSA_2:11; then reconsider D = 1 as Element of Values intloc 0 by INT_1:def 1; reconsider DWA = 2 as Element of INT by INT_1:def 1; set w = the State of SCM+FSA; A8: InsCode ((f,a):=b) = 10 .= InsCode ((fsloc 0, intloc 1):=(intloc 0)); Values intloc 1 = INT by SCMFSA_2:11; then reconsider E = 1 as Element of Values intloc 1 by INT_1:def 1; <*DWA*> in INT* by FINSEQ_1:def 11; then reconsider F = <*2*> as Element of Values fsloc 0 by SCMFSA_2:12; reconsider t = w+*(fsloc 0 .--> F)+*(intloc 0 .--> D)+*(intloc 1 .--> E) as State of SCM+FSA; consider k being Nat such that A9: k = |. t.intloc 1 .| and A10: Exec((fsloc 0, intloc 1):=(intloc 0), t).fsloc 0 = (t.fsloc 0) +* (k,t.intloc 0) by SCMFSA_2:73; t.intloc 1 = E by FUNCT_7:94; then A11: k = 1 by A9,ABSVALUE:def 1; fsloc 0 in FinSeq-Locations by SCMFSA_2:def 5; then A12: fsloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3; A13: F <> <*D*> by FINSEQ_1:76; A14: t.fsloc 0 = F by Lm3,Lm4,FUNCT_7:114; t.intloc 0 = D by AMI_3:10,BVFUNC14:12; then Exec((fsloc 0, intloc 1):=intloc 0, t).fsloc 0 = <*D*> by A14,A10,A11, FUNCT_7:95; hence thesis by A8,A14,A13,A12; end; end; registration let a, b, f; cluster b:=(f,a) -> non jump-only; coherence; cluster (f,a):=b -> non jump-only; coherence; end; registration let a, f; cluster InsCode (a:=len f) -> non jump-only for InsType of the InstructionsF of SCM+FSA; coherence proof Values intloc 0 = INT by SCMFSA_2:11; then reconsider D = 3 as Element of Values intloc 0 by INT_1:def 1; reconsider DWA = 2 as Element of INT by INT_1:def 1; set w = the State of SCM+FSA; A1: InsCode (a:=len f) = 11 .= InsCode (intloc 0:=len fsloc 0); <*DWA*> in INT* by FINSEQ_1:def 11; then reconsider F = <*2*> as Element of Values fsloc 0 by SCMFSA_2:12; reconsider t = w+*(fsloc 0 .--> F)+*(intloc 0 .--> D) as State of SCM+FSA; A2: t.fsloc 0 = F by BVFUNC14:12,SCMFSA_2:99; intloc 0 in Int-Locations by AMI_2:def 16; then A3: intloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3; A4: t.intloc 0 = D by FUNCT_7:94; Exec(intloc 0 :=len fsloc 0, t).intloc 0 = len (t.fsloc 0) by SCMFSA_2:74 .= 1 by A2,FINSEQ_1:39; hence thesis by A1,A4,A3; end; cluster InsCode (f:=<0,...,0>a) -> non jump-only for InsType of the InstructionsF of SCM+FSA; coherence proof Values intloc 0 = INT by SCMFSA_2:11; then reconsider D = 1 as Element of Values intloc 0 by INT_1:def 1; reconsider DWA = 2 as Element of INT by INT_1:def 1; set w = the State of SCM+FSA; <*DWA*> in INT* by FINSEQ_1:def 11; then reconsider F = <*2*> as Element of Values fsloc 0 by SCMFSA_2:12; reconsider t = w+*(fsloc 0 .--> F)+*(intloc 0 .--> D) as State of SCM+FSA; A5: t.fsloc 0 = F by BVFUNC14:12,SCMFSA_2:99; A6: F <> <*0*> by FINSEQ_1:76; consider k being Nat such that A7: k = |. t.intloc 0 .| and A8: Exec(fsloc 0:=<0,...,0>intloc 0, t).fsloc 0 = k |-> 0 by SCMFSA_2:75; fsloc 0 in FinSeq-Locations by SCMFSA_2:def 5; then A9: fsloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3; t.intloc 0 = D by FUNCT_7:94; then k = 1 by A7,ABSVALUE:def 1; then A10: Exec(fsloc 0:=<0,...,0>intloc 0, t).fsloc 0 = <*0*> by A8,FINSEQ_2:59; InsCode (f:=<0,...,0>a) = 12 .= InsCode (fsloc 0:=<0,...,0>intloc 0); hence thesis by A5,A6,A10,A9; end; end; registration let a, f; cluster a:=len f -> non jump-only; coherence; cluster f:=<0,...,0>a -> non jump-only; coherence; end; registration cluster SCM+FSA -> with_explicit_jumps; coherence proof let I be Instruction of SCM+FSA; thus JUMP I c= rng JumpPart I proof let f be object such that A1: f in JUMP I; per cases by SCMFSA_2:93; suppose I = [0,{},{}]; hence thesis by A1,SCMFSA_2:96; end; suppose ex a,b st I = a:=b; hence thesis by A1; end; suppose ex a,b st I = AddTo(a,b); hence thesis by A1; end; suppose ex a,b st I = SubFrom(a,b); hence thesis by A1; end; suppose ex a,b st I = MultBy(a,b); hence thesis by A1; end; suppose ex a,b st I = Divide(a,b); hence thesis by A1; end; suppose A2: ex i1 st I = goto i1; consider i1 such that A3: I = goto i1 by A2; rng<*i1*> = {i1} by FINSEQ_1:39; hence thesis by A1,A3,Th34; end; suppose A4: ex i1,a st I = a=0_goto i1; consider a, i1 such that A5: I = a=0_goto i1 by A4; A6: JumpPart (a=0_goto i1) = <*i1*> by Th15; rng<*i1*> = {i1} by FINSEQ_1:39; hence thesis by A1,A5,A6,Th36; end; suppose A7: ex i1,a st I = a>0_goto i1; consider a, i1 such that A8: I = a>0_goto i1 by A7; A9: JumpPart (a>0_goto i1) = <*i1*> by Th16; rng<*i1*> = {i1} by FINSEQ_1:39; hence thesis by A1,A8,A9,Th38; end; suppose ex a,b,f st I = b:=(f,a); hence thesis by A1; end; suppose ex a,b,f st I = (f,a):=b; hence thesis by A1; end; suppose ex a,f st I = a:=len f; hence thesis by A1; end; suppose ex a,f st I = f:=<0,...,0>a; hence thesis by A1; end; end; let f being object; assume f in rng JumpPart I; then consider k being object such that A10: k in dom JumpPart I and A11: f = (JumpPart I).k by FUNCT_1:def 3; per cases by SCMFSA_2:93; suppose I = [0,{},{}]; then dom JumpPart I = dom {}; hence thesis by A10; end; suppose ex a,b st I = a:=b; then consider a, b such that A12: I = a:=b; k in dom {} by A10,A12,Th10; hence thesis; end; suppose ex a,b st I = AddTo(a,b); then consider a, b such that A13: I = AddTo(a,b); k in dom {} by A10,A13,Th11; hence thesis; end; suppose ex a,b st I = SubFrom(a,b); then consider a, b such that A14: I = SubFrom(a,b); k in dom {} by A10,A14,Th12; hence thesis; end; suppose ex a,b st I = MultBy(a,b); then consider a, b such that A15: I = MultBy(a,b); k in dom {} by A10,A15,Th13; hence thesis; end; suppose ex a,b st I = Divide(a,b); then consider a, b such that A16: I = Divide(a,b); k in dom {} by A10,A16,Th14; hence thesis; end; suppose ex i1 st I = goto i1; then consider i1 such that A17: I = goto i1; A18: JumpPart I = <*i1*> by A17; then k = 1 by A10,FINSEQ_1:90; then A19: f = i1 by A18,A11,FINSEQ_1:def 8; JUMP I = {i1} by A17,Th34; hence thesis by A19,TARSKI:def 1; end; suppose ex i1,a st I = a=0_goto i1; then consider a, i1 such that A20: I = a=0_goto i1; A21: JumpPart I = <*i1*> by A20,Th15; then k = 1 by A10,FINSEQ_1:90; then A22: f = i1 by A21,A11,FINSEQ_1:def 8; JUMP I = {i1} by A20,Th36; hence thesis by A22,TARSKI:def 1; end; suppose ex i1,a st I = a>0_goto i1; then consider a, i1 such that A23: I = a>0_goto i1; A24: JumpPart I = <*i1*> by A23,Th16; then k = 1 by A10,FINSEQ_1:90; then A25: f = i1 by A24,A11,FINSEQ_1:def 8; JUMP I = {i1} by A23,Th38; hence thesis by A25,TARSKI:def 1; end; suppose ex a,b,f st I = b:=(f,a); then consider a, b, f such that A26: I = b:=(f,a); k in dom {} by A10,A26; hence thesis; end; suppose ex a,b,f st I = (f,a):=b; then consider a, b, f such that A27: I = (f,a):=b; k in dom {} by A10,A27; hence thesis; end; suppose ex a,f st I = a:=len f; then consider a, f such that A28: I = a:=len f; k in dom {} by A10,A28; hence thesis; end; suppose ex a,f st I = f:=<0,...,0>a; then consider a, f such that A29: I = f:=<0,...,0>a; k in dom {} by A10,A29; hence thesis; end; end; end; theorem Th41: IncAddr(goto i1,k) = goto (i1+ k) proof A1: InsCode IncAddr(goto i1,k) = InsCode goto i1 by COMPOS_0:def 9 .= 6 .= InsCode goto (i1+k); A2: AddressPart IncAddr(goto i1,k) = AddressPart goto i1 by COMPOS_0:def 9 .= {} .= AddressPart goto (i1+k); A3: JumpPart IncAddr(goto i1,k) = k + JumpPart goto i1 by COMPOS_0:def 9; then A4: dom JumpPart IncAddr(goto i1,k) = dom JumpPart goto i1 by VALUED_1:def 2; A5: for x being object st x in dom JumpPart goto i1 holds (JumpPart IncAddr(goto i1,k)).x = (JumpPart goto (i1+k)).x proof let x be object; assume A6: x in dom JumpPart goto i1; then x in dom <*i1*>; then A7: x = 1 by FINSEQ_1:90; set f = (JumpPart goto i1).x; A8: (JumpPart IncAddr(goto i1,k)).x = k+f by A4,A3,A6,VALUED_1:def 2; f = <*i1*>.x .= i1 by A7,FINSEQ_1:def 8; hence (JumpPart IncAddr(goto i1,k)).x = <*(i1+k)*>. x by A7,A8,FINSEQ_1:def 8 .= (JumpPart goto (i1+k)).x; end; dom JumpPart goto (i1+k) = dom <*(i1+k)*> .= Seg 1 by FINSEQ_1:def 8 .= dom <*i1*> by FINSEQ_1:def 8 .= dom JumpPart goto i1; then JumpPart IncAddr(goto i1,k) = JumpPart goto(i1+k) by A4,A5,FUNCT_1:2; hence thesis by A1,A2,COMPOS_0:1; end; theorem Th42: IncAddr(a=0_goto i1,k) = a=0_goto (i1+k) proof A1: InsCode IncAddr(a=0_goto i1,k) = InsCode (a=0_goto i1) by COMPOS_0:def 9 .= 7 by SCMFSA_2:24 .= InsCode (a=0_goto (i1+k)) by SCMFSA_2:24; A2: a=0_goto i1 = [7, <* i1*>,<*a *>] by Th7; A3: a=0_goto(i1+k) = [7, <* i1+k*>,<*a *>] by Th7; A4: AddressPart IncAddr(a=0_goto i1,k) = AddressPart (a=0_goto i1) by COMPOS_0:def 9 .= <*a*> by A2 .= AddressPart (a=0_goto (i1+k)) by A3; A5: JumpPart IncAddr(a=0_goto i1,k) = k + JumpPart (a=0_goto i1) by COMPOS_0:def 9; then A6: dom JumpPart IncAddr(a=0_goto i1,k) = dom JumpPart (a=0_goto i1) by VALUED_1:def 2; A7: for x being object st x in dom JumpPart (a=0_goto i1) holds (JumpPart IncAddr(a=0_goto i1,k)).x = (JumpPart (a=0_goto (i1+k))).x proof let x be object; assume A8: x in dom JumpPart (a=0_goto i1); then x in dom <*i1*> by Th15; then A9: x = 1 by FINSEQ_1:90; set f = (JumpPart (a=0_goto i1)).x; A10: (JumpPart IncAddr(a=0_goto i1,k)).x = k+f by A6,A5,A8,VALUED_1:def 2; f = <*i1*>.x by Th15 .= i1 by A9,FINSEQ_1:40; hence (JumpPart IncAddr(a=0_goto i1,k)).x = <*(i1+k)*>.x by A9,A10,FINSEQ_1:40 .= (JumpPart (a=0_goto (i1+k))).x by Th15; end; dom JumpPart (a=0_goto (i1+k)) = dom <*(i1+k)*> by Th15 .= Seg 1 by FINSEQ_1:38 .= dom <*i1*> by FINSEQ_1:38 .= dom JumpPart (a=0_goto i1) by Th15; then JumpPart IncAddr(a=0_goto i1,k) = JumpPart (a=0_goto (i1+k)) by A6,A7,FUNCT_1:2; hence thesis by A1,A4,COMPOS_0:1; end; theorem Th43: IncAddr(a>0_goto i1,k) = a>0_goto (i1+k) proof A1: InsCode IncAddr(a>0_goto i1,k) = InsCode (a>0_goto i1) by COMPOS_0:def 9 .= 8 by SCMFSA_2:25 .= InsCode (a>0_goto (i1+k)) by SCMFSA_2:25; A2: a>0_goto i1 = [8, <* i1*>,<*a *>] by Th8; A3: a>0_goto(i1+k) = [8, <* i1+k*>,<*a *>] by Th8; A4: AddressPart IncAddr(a>0_goto i1,k) = AddressPart (a>0_goto i1) by COMPOS_0:def 9 .= <*a*> by A2 .= AddressPart (a>0_goto (i1+k)) by A3; A5: JumpPart IncAddr(a>0_goto i1,k) = k + JumpPart (a>0_goto i1) by COMPOS_0:def 9; then A6: dom JumpPart IncAddr(a>0_goto i1,k) = dom JumpPart (a>0_goto i1) by VALUED_1:def 2; A7: for x being object st x in dom JumpPart (a>0_goto i1) holds (JumpPart IncAddr(a>0_goto i1,k)).x = (JumpPart (a>0_goto (i1+k))).x proof let x be object; assume A8: x in dom JumpPart (a>0_goto i1); then x in dom <*i1*> by Th16; then A9: x = 1 by FINSEQ_1:90; set f = (JumpPart (a>0_goto i1)).1; A10: (JumpPart IncAddr(a>0_goto i1,k)).1 = k+f by A9,A6,A5,A8,VALUED_1:def 2; f = <*i1*>.x by Th16,A9 .= i1 by A9,FINSEQ_1:40; hence (JumpPart IncAddr(a>0_goto i1,k)).x = <*(i1+k)*>.x by A9,A10,FINSEQ_1:40 .= (JumpPart (a>0_goto (i1+k))).x by Th16; end; dom JumpPart (a>0_goto (i1+k)) = dom <*(i1+k)*> by Th16 .= Seg 1 by FINSEQ_1:38 .= dom <*i1*> by FINSEQ_1:38 .= dom JumpPart (a>0_goto i1) by Th16; then JumpPart IncAddr(a>0_goto i1,k) = JumpPart (a>0_goto (i1+k)) by A6,A7,FUNCT_1:2; hence thesis by A1,A4,COMPOS_0:1; end; registration cluster SCM+FSA -> IC-relocable; coherence proof let I be Instruction of SCM+FSA; per cases by SCMFSA_2:93; suppose I = [0,{},{}]; hence thesis by SCMFSA_2:96; end; suppose ex a,b st I = a:=b; hence thesis; end; suppose ex a,b st I = AddTo(a,b); hence thesis; end; suppose ex a,b st I = SubFrom(a,b); hence thesis; end; suppose ex a,b st I = MultBy(a,b); hence thesis; end; suppose ex a,b st I = Divide(a,b); hence thesis; end; suppose A1: ex i1 st I = goto i1; let j,k be Nat, s1 be State of SCM+FSA; set s2 = IncIC(s1,k); consider i1 such that A2: I = goto i1 by A1; thus IC Exec(IncAddr(I,j),s1) + k = IC Exec(goto(j+i1),s1) + k by A2,Th41 .= j+i1+k by SCMFSA_2:69 .= IC Exec(goto(j+k+i1),s2) by SCMFSA_2:69 .= IC Exec(IncAddr(I,j+k), s2) by A2,Th41; end; suppose ex i1,a st I = a=0_goto i1; then consider a, i1 such that A3: I = a=0_goto i1; let j,k be Nat, s1 be State of SCM+FSA; set s2 = IncIC(s1,k); a <> IC SCM+FSA & dom (IC SCM+FSA .--> (IC s1 + k)) = {IC SCM+FSA} by SCMFSA_2:56; then not a in dom (IC SCM+FSA .--> (IC s1 + k)) by TARSKI:def 1; then A4: s1.a = s2.a by FUNCT_4:11; per cases; suppose A5: s1.a = 0; thus IC Exec(IncAddr(I,j),s1) + k = IC Exec(a=0_goto(j+i1),s1) + k by A3,Th42 .= j+i1+k by A5,SCMFSA_2:70 .= IC Exec(a=0_goto(j+k+i1),s2) by A4,A5,SCMFSA_2:70 .= IC Exec(IncAddr(I,j+k), s2) by A3,Th42; end; suppose A6: s1.a <> 0; A7: IncAddr(I,j) = a=0_goto(i1+j) by A3,Th42; A8: IncAddr(I,j+k) = a=0_goto(i1+(j+k)) by A3,Th42; IC SCM+FSA in dom (IC SCM+FSA .--> (IC s1 + k)) by TARSKI:def 1; then A9: IC s2 = (IC SCM+FSA .--> (IC s1 + k)).IC SCM+FSA by FUNCT_4:13 .= (IC s1 + k) by FUNCOP_1:72; thus IC Exec(IncAddr(I,j),s1) + k = IC s1 + 1 + k by A7,A6,SCMFSA_2:70 .= IC s2 + 1 by A9 .= IC Exec(IncAddr(I,j+k), s2) by A8,A6,A4,SCMFSA_2:70; end; end; suppose ex i1,a st I = a>0_goto i1; then consider i1,a such that A10: I = a>0_goto i1; let j,k be Nat, s1 be State of SCM+FSA; set s2 = IncIC(s1,k); a <> IC SCM+FSA & dom (IC SCM+FSA .--> (IC s1 + k)) = {IC SCM+FSA} by SCMFSA_2:56; then not a in dom (IC SCM+FSA .--> (IC s1 + k)) by TARSKI:def 1; then A11: s1.a = s2.a by FUNCT_4:11; per cases; suppose A12: s1.a > 0; thus IC Exec(IncAddr(I,j),s1) + k = IC Exec(a>0_goto(j+i1),s1) + k by A10,Th43 .= j+i1+k by A12,SCMFSA_2:71 .= IC Exec(a>0_goto(j+k+i1),s2) by A11,A12,SCMFSA_2:71 .= IC Exec(IncAddr(I,j+k), s2) by A10,Th43; end; suppose A13: s1.a <= 0; A14: IncAddr(I,j) = a>0_goto(i1+j) by A10,Th43; A15: IncAddr(I,j+k) = a>0_goto(i1+(j+k)) by A10,Th43; IC SCM+FSA in dom (IC SCM+FSA .--> (IC s1 + k)) by TARSKI:def 1; then A16: IC s2 = (IC SCM+FSA .--> (IC s1 + k)).IC SCM+FSA by FUNCT_4:13 .= (IC s1 + k) by FUNCOP_1:72; thus IC Exec(IncAddr(I,j),s1) + k = IC s1 + 1 + k by A14,A13,SCMFSA_2:71 .= IC s2 + 1 by A16 .= IC Exec(IncAddr(I,j+k), s2) by A15,A13,A11,SCMFSA_2:71; end; end; suppose ex a,b,f st I = b:=(f,a); hence thesis; end; suppose ex a,b,f st I = (f,a):=b; hence thesis; end; suppose ex a,f st I = a:=len f; hence thesis; end; suppose ex a,f st I = f:=<0,...,0>a; hence thesis; end; end; end;