:: SCMFSA10 semantic presentation
begin
definition
let la, lb be Int-Location;
let a, b be Integer;
:: original: -->
redefine func(la,lb) --> (a,b) -> PartState of SCM+FSA;
coherence
(la,lb) --> (a,b) is PartState of SCM+FSA
proof
A1: Values lb = INT by SCMFSA_2:11;
b is Element of INT by INT_1:def_2;
then reconsider b = 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 = a as Element of Values la by A2;
(la,lb) --> (a,b) is PartState of SCM+FSA ;
hence (la,lb) --> (a,b) is PartState of SCM+FSA ; ::_thesis: verum
end;
end;
theorem Th1: :: SCMFSA10:1
for o being Object of SCM+FSA holds
( not o in Data-Locations or o is Int-Location or o is FinSeq-Location )
proof
let o be Object of SCM+FSA; ::_thesis: ( not o in Data-Locations or o is Int-Location or o is FinSeq-Location )
assume o in Data-Locations ; ::_thesis: ( o is Int-Location or o is FinSeq-Location )
then ( o in SCM-Data-Loc or o in SCM+FSA-Data*-Loc ) by SCMFSA_2:100, XBOOLE_0:def_3;
hence ( o is Int-Location or o is FinSeq-Location ) by AMI_2:def_16, SCMFSA_2:def_5; ::_thesis: verum
end;
theorem Th2: :: SCMFSA10:2
for a, b being Int-Location holds a := b = [1,{},<*a,b*>]
proof
let a, b be Int-Location; ::_thesis: a := b = [1,{},<*a,b*>]
ex A, B being Data-Location st
( a = A & b = B & a := b = A := B ) by SCMFSA_2:def_8;
hence a := b = [1,{},<*a,b*>] ; ::_thesis: verum
end;
theorem Th3: :: SCMFSA10:3
for a, b being Int-Location holds AddTo (a,b) = [2,{},<*a,b*>]
proof
let a, b be Int-Location; ::_thesis: AddTo (a,b) = [2,{},<*a,b*>]
ex A, B being Data-Location st
( a = A & b = B & AddTo (a,b) = AddTo (A,B) ) by SCMFSA_2:def_9;
hence AddTo (a,b) = [2,{},<*a,b*>] ; ::_thesis: verum
end;
theorem Th4: :: SCMFSA10:4
for a, b being Int-Location holds SubFrom (a,b) = [3,{},<*a,b*>]
proof
let a, b be Int-Location; ::_thesis: SubFrom (a,b) = [3,{},<*a,b*>]
ex A, B being Data-Location st
( a = A & b = B & SubFrom (a,b) = SubFrom (A,B) ) by SCMFSA_2:def_10;
hence SubFrom (a,b) = [3,{},<*a,b*>] ; ::_thesis: verum
end;
theorem Th5: :: SCMFSA10:5
for a, b being Int-Location holds MultBy (a,b) = [4,{},<*a,b*>]
proof
let a, b be Int-Location; ::_thesis: MultBy (a,b) = [4,{},<*a,b*>]
ex A, B being Data-Location st
( a = A & b = B & MultBy (a,b) = MultBy (A,B) ) by SCMFSA_2:def_11;
hence MultBy (a,b) = [4,{},<*a,b*>] ; ::_thesis: verum
end;
theorem Th6: :: SCMFSA10:6
for a, b being Int-Location holds Divide (a,b) = [5,{},<*a,b*>]
proof
let a, b be Int-Location; ::_thesis: Divide (a,b) = [5,{},<*a,b*>]
ex A, B being Data-Location st
( a = A & b = B & Divide (a,b) = Divide (A,B) ) by SCMFSA_2:def_12;
hence Divide (a,b) = [5,{},<*a,b*>] ; ::_thesis: verum
end;
theorem Th7: :: SCMFSA10:7
for a being Int-Location
for il being Element of NAT holds a =0_goto il = [7,<*il*>,<*a*>]
proof
let a be Int-Location; ::_thesis: for il being Element of NAT holds a =0_goto il = [7,<*il*>,<*a*>]
let il be Element of NAT ; ::_thesis: a =0_goto il = [7,<*il*>,<*a*>]
ex A being Data-Location st
( A = a & A =0_goto il = a =0_goto il ) by SCMFSA_2:def_14;
hence a =0_goto il = [7,<*il*>,<*a*>] ; ::_thesis: verum
end;
theorem Th8: :: SCMFSA10:8
for a being Int-Location
for il being Element of NAT holds a >0_goto il = [8,<*il*>,<*a*>]
proof
let a be Int-Location; ::_thesis: for il being Element of NAT holds a >0_goto il = [8,<*il*>,<*a*>]
let il be Element of NAT ; ::_thesis: a >0_goto il = [8,<*il*>,<*a*>]
ex A being Data-Location st
( A = a & A >0_goto il = a >0_goto il ) by SCMFSA_2:def_15;
hence a >0_goto il = [8,<*il*>,<*a*>] ; ::_thesis: verum
end;
theorem Th9: :: SCMFSA10:9
JumpPart (halt SCM+FSA) = {} ;
theorem Th10: :: SCMFSA10:10
for a, b being Int-Location holds JumpPart (a := b) = {}
proof
let a, b be Int-Location; ::_thesis: JumpPart (a := b) = {}
thus JumpPart (a := b) = [1,{},<*a,b*>] `2_3 by Th2
.= {} ; ::_thesis: verum
end;
theorem Th11: :: SCMFSA10:11
for a, b being Int-Location holds JumpPart (AddTo (a,b)) = {}
proof
let a, b be Int-Location; ::_thesis: JumpPart (AddTo (a,b)) = {}
thus JumpPart (AddTo (a,b)) = [2,{},<*a,b*>] `2_3 by Th3
.= {} ; ::_thesis: verum
end;
theorem Th12: :: SCMFSA10:12
for a, b being Int-Location holds JumpPart (SubFrom (a,b)) = {}
proof
let a, b be Int-Location; ::_thesis: JumpPart (SubFrom (a,b)) = {}
thus JumpPart (SubFrom (a,b)) = [3,{},<*a,b*>] `2_3 by Th4
.= {} ; ::_thesis: verum
end;
theorem Th13: :: SCMFSA10:13
for a, b being Int-Location holds JumpPart (MultBy (a,b)) = {}
proof
let a, b be Int-Location; ::_thesis: JumpPart (MultBy (a,b)) = {}
thus JumpPart (MultBy (a,b)) = [4,{},<*a,b*>] `2_3 by Th5
.= {} ; ::_thesis: verum
end;
theorem Th14: :: SCMFSA10:14
for a, b being Int-Location holds JumpPart (Divide (a,b)) = {}
proof
let a, b be Int-Location; ::_thesis: JumpPart (Divide (a,b)) = {}
thus JumpPart (Divide (a,b)) = [5,{},<*a,b*>] `2_3 by Th6
.= {} ; ::_thesis: verum
end;
theorem Th15: :: SCMFSA10:15
for i1 being Element of NAT
for a being Int-Location holds JumpPart (a =0_goto i1) = <*i1*>
proof
let i1 be Element of NAT ; ::_thesis: for a being Int-Location holds JumpPart (a =0_goto i1) = <*i1*>
let a be Int-Location; ::_thesis: JumpPart (a =0_goto i1) = <*i1*>
thus JumpPart (a =0_goto i1) = [7,<*i1*>,<*a*>] `2_3 by Th7
.= <*i1*> ; ::_thesis: verum
end;
theorem Th16: :: SCMFSA10:16
for i1 being Element of NAT
for a being Int-Location holds JumpPart (a >0_goto i1) = <*i1*>
proof
let i1 be Element of NAT ; ::_thesis: for a being Int-Location holds JumpPart (a >0_goto i1) = <*i1*>
let a be Int-Location; ::_thesis: JumpPart (a >0_goto i1) = <*i1*>
thus JumpPart (a >0_goto i1) = [8,<*i1*>,<*a*>] `2_3 by Th8
.= <*i1*> ; ::_thesis: verum
end;
theorem :: SCMFSA10:17
for T being InsType of the InstructionsF of SCM+FSA st T = 0 holds
JumpParts T = {0}
proof
let T be InsType of the InstructionsF of SCM+FSA; ::_thesis: ( T = 0 implies JumpParts T = {0} )
assume A1: T = 0 ; ::_thesis: JumpParts T = {0}
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {0} c= JumpParts T
let a be set ; ::_thesis: ( a in JumpParts T implies a in {0} )
assume a in JumpParts T ; ::_thesis: a in {0}
then consider I being Instruction of SCM+FSA 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, Th9, TARSKI:def_1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {0} or a in JumpParts T )
assume a in {0} ; ::_thesis: a in JumpParts T
then A4: a = 0 by TARSKI:def_1;
InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
hence a in JumpParts T by A1, Th9, A4; ::_thesis: verum
end;
theorem :: SCMFSA10:18
for T being InsType of the InstructionsF of SCM+FSA st T = 1 holds
JumpParts T = {{}}
proof
let T be InsType of the InstructionsF of SCM+FSA; ::_thesis: ( T = 1 implies JumpParts T = {{}} )
assume A1: T = 1 ; ::_thesis: JumpParts T = {{}}
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= JumpParts T
let x be set ; ::_thesis: ( x in JumpParts T implies x in {{}} )
assume x in JumpParts T ; ::_thesis: x in {{}}
then consider I being Instruction of SCM+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T ;
consider a, b being Int-Location such that
A4: I = a := b by A1, A3, SCMFSA_2:30;
x = {} by A2, Th10, A4;
hence x in {{}} by TARSKI:def_1; ::_thesis: verum
end;
set a = the Int-Location;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T )
assume x in {{}} ; ::_thesis: x in JumpParts T
then x = {} by TARSKI:def_1;
then A5: x = JumpPart ( the Int-Location := the Int-Location) by Th10;
InsCode ( the Int-Location := the Int-Location) = 1 by SCMFSA_2:18;
hence x in JumpParts T by A5, A1; ::_thesis: verum
end;
theorem :: SCMFSA10:19
for T being InsType of the InstructionsF of SCM+FSA st T = 2 holds
JumpParts T = {{}}
proof
let T be InsType of the InstructionsF of SCM+FSA; ::_thesis: ( T = 2 implies JumpParts T = {{}} )
assume A1: T = 2 ; ::_thesis: JumpParts T = {{}}
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= JumpParts T
let x be set ; ::_thesis: ( x in JumpParts T implies x in {{}} )
assume x in JumpParts T ; ::_thesis: x in {{}}
then consider I being Instruction of SCM+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T ;
consider a, b being Int-Location 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; ::_thesis: verum
end;
set a = the Int-Location;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T )
assume x in {{}} ; ::_thesis: x in JumpParts T
then x = {} by TARSKI:def_1;
then A5: x = JumpPart (AddTo ( the Int-Location, the Int-Location)) by Th11;
InsCode (AddTo ( the Int-Location, the Int-Location)) = 2 by SCMFSA_2:19;
hence x in JumpParts T by A5, A1; ::_thesis: verum
end;
theorem :: SCMFSA10:20
for T being InsType of the InstructionsF of SCM+FSA st T = 3 holds
JumpParts T = {{}}
proof
let T be InsType of the InstructionsF of SCM+FSA; ::_thesis: ( T = 3 implies JumpParts T = {{}} )
assume A1: T = 3 ; ::_thesis: JumpParts T = {{}}
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= JumpParts T
let x be set ; ::_thesis: ( x in JumpParts T implies x in {{}} )
assume x in JumpParts T ; ::_thesis: x in {{}}
then consider I being Instruction of SCM+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T ;
consider a, b being Int-Location 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; ::_thesis: verum
end;
set a = the Int-Location;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T )
assume x in {{}} ; ::_thesis: x in JumpParts T
then x = {} by TARSKI:def_1;
then A5: x = JumpPart (SubFrom ( the Int-Location, the Int-Location)) by Th12;
InsCode (SubFrom ( the Int-Location, the Int-Location)) = 3 by SCMFSA_2:20;
hence x in JumpParts T by A5, A1; ::_thesis: verum
end;
theorem :: SCMFSA10:21
for T being InsType of the InstructionsF of SCM+FSA st T = 4 holds
JumpParts T = {{}}
proof
let T be InsType of the InstructionsF of SCM+FSA; ::_thesis: ( T = 4 implies JumpParts T = {{}} )
assume A1: T = 4 ; ::_thesis: JumpParts T = {{}}
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= JumpParts T
let x be set ; ::_thesis: ( x in JumpParts T implies x in {{}} )
assume x in JumpParts T ; ::_thesis: x in {{}}
then consider I being Instruction of SCM+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T ;
consider a, b being Int-Location 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; ::_thesis: verum
end;
set a = the Int-Location;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T )
assume x in {{}} ; ::_thesis: x in JumpParts T
then x = {} by TARSKI:def_1;
then A5: x = JumpPart (MultBy ( the Int-Location, the Int-Location)) by Th13;
InsCode (MultBy ( the Int-Location, the Int-Location)) = 4 by SCMFSA_2:21;
hence x in JumpParts T by A5, A1; ::_thesis: verum
end;
theorem :: SCMFSA10:22
for T being InsType of the InstructionsF of SCM+FSA st T = 5 holds
JumpParts T = {{}}
proof
let T be InsType of the InstructionsF of SCM+FSA; ::_thesis: ( T = 5 implies JumpParts T = {{}} )
assume A1: T = 5 ; ::_thesis: JumpParts T = {{}}
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= JumpParts T
let x be set ; ::_thesis: ( x in JumpParts T implies x in {{}} )
assume x in JumpParts T ; ::_thesis: x in {{}}
then consider I being Instruction of SCM+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T ;
consider a, b being Int-Location 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; ::_thesis: verum
end;
set a = the Int-Location;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T )
assume x in {{}} ; ::_thesis: x in JumpParts T
then x = {} by TARSKI:def_1;
then A5: x = JumpPart (Divide ( the Int-Location, the Int-Location)) by Th14;
InsCode (Divide ( the Int-Location, the Int-Location)) = 5 by SCMFSA_2:22;
hence x in JumpParts T by A5, A1; ::_thesis: verum
end;
theorem Th23: :: SCMFSA10:23
for T being InsType of the InstructionsF of SCM+FSA st T = 6 holds
dom (product" (JumpParts T)) = {1}
proof
let T be InsType of the InstructionsF of SCM+FSA; ::_thesis: ( T = 6 implies dom (product" (JumpParts T)) = {1} )
set i1 = the Element of NAT ;
assume A1: T = 6 ; ::_thesis: dom (product" (JumpParts T)) = {1}
A2: JumpPart (goto the Element of NAT ) = <* the Element of NAT *> by RECDEF_2:def_2;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {1} c= dom (product" (JumpParts T))
let x be set ; ::_thesis: ( x in dom (product" (JumpParts T)) implies x in {1} )
InsCode (goto the Element of NAT ) = 6 by SCMFSA_2:23;
then A3: JumpPart (goto the Element of NAT ) in JumpParts T by A1;
assume x in dom (product" (JumpParts T)) ; ::_thesis: x in {1}
then x in DOM (JumpParts T) by CARD_3:def_12;
then x in dom (JumpPart (goto the Element of NAT )) by A3, CARD_3:108;
hence x in {1} by A2, FINSEQ_1:2, FINSEQ_1:def_8; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {1} or x in dom (product" (JumpParts T)) )
assume A4: x in {1} ; ::_thesis: x in dom (product" (JumpParts T))
for f being Function st f in JumpParts T holds
x in dom f
proof
let f be Function; ::_thesis: ( f in JumpParts T implies x in dom f )
assume f in JumpParts T ; ::_thesis: x in dom f
then consider I being Instruction of SCM+FSA such that
A5: f = JumpPart I and
A6: InsCode I = T ;
consider i1 being Element of NAT such that
A7: I = goto i1 by A1, A6, SCMFSA_2:35;
f = <*i1*> by A5, A7, RECDEF_2:def_2;
hence x in dom f by A4, FINSEQ_1:2, FINSEQ_1:def_8; ::_thesis: verum
end;
then x in DOM (JumpParts T) by CARD_3:109;
hence x in dom (product" (JumpParts T)) by CARD_3:def_12; ::_thesis: verum
end;
theorem Th24: :: SCMFSA10:24
for T being InsType of the InstructionsF of SCM+FSA st T = 7 holds
dom (product" (JumpParts T)) = {1}
proof
let T be InsType of the InstructionsF of SCM+FSA; ::_thesis: ( T = 7 implies dom (product" (JumpParts T)) = {1} )
set i1 = the Element of NAT ;
set a = the Int-Location;
assume A1: T = 7 ; ::_thesis: dom (product" (JumpParts T)) = {1}
A2: JumpPart ( the Int-Location =0_goto the Element of NAT ) = <* the Element of NAT *> by Th15;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {1} c= dom (product" (JumpParts T))
let x be set ; ::_thesis: ( x in dom (product" (JumpParts T)) implies x in {1} )
InsCode ( the Int-Location =0_goto the Element of NAT ) = 7 by SCMFSA_2:24;
then A3: JumpPart ( the Int-Location =0_goto the Element of NAT ) in JumpParts T by A1;
assume x in dom (product" (JumpParts T)) ; ::_thesis: x in {1}
then x in DOM (JumpParts T) by CARD_3:def_12;
then x in dom (JumpPart ( the Int-Location =0_goto the Element of NAT )) by A3, CARD_3:108;
hence x in {1} by A2, FINSEQ_1:2, FINSEQ_1:38; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {1} or x in dom (product" (JumpParts T)) )
assume A4: x in {1} ; ::_thesis: x in dom (product" (JumpParts T))
for f being Function st f in JumpParts T holds
x in dom f
proof
let f be Function; ::_thesis: ( f in JumpParts T implies x in dom f )
assume f in JumpParts T ; ::_thesis: x in dom f
then consider I being Instruction of SCM+FSA such that
A5: f = JumpPart I and
A6: InsCode I = T ;
consider i1 being Element of NAT , a being Int-Location such that
A7: I = a =0_goto i1 by A1, A6, SCMFSA_2:36;
f = <*i1*> by A5, A7, Th15;
hence x in dom f by A4, FINSEQ_1:2, FINSEQ_1:38; ::_thesis: verum
end;
then x in DOM (JumpParts T) by CARD_3:109;
hence x in dom (product" (JumpParts T)) by CARD_3:def_12; ::_thesis: verum
end;
theorem Th25: :: SCMFSA10:25
for T being InsType of the InstructionsF of SCM+FSA st T = 8 holds
dom (product" (JumpParts T)) = {1}
proof
let T be InsType of the InstructionsF of SCM+FSA; ::_thesis: ( T = 8 implies dom (product" (JumpParts T)) = {1} )
set i1 = the Element of NAT ;
set a = the Int-Location;
assume A1: T = 8 ; ::_thesis: dom (product" (JumpParts T)) = {1}
A2: JumpPart ( the Int-Location >0_goto the Element of NAT ) = <* the Element of NAT *> by Th16;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {1} c= dom (product" (JumpParts T))
let x be set ; ::_thesis: ( x in dom (product" (JumpParts T)) implies x in {1} )
InsCode ( the Int-Location >0_goto the Element of NAT ) = 8 by SCMFSA_2:25;
then A3: JumpPart ( the Int-Location >0_goto the Element of NAT ) in JumpParts T by A1;
assume x in dom (product" (JumpParts T)) ; ::_thesis: x in {1}
then x in DOM (JumpParts T) by CARD_3:def_12;
then x in dom (JumpPart ( the Int-Location >0_goto the Element of NAT )) by A3, CARD_3:108;
hence x in {1} by A2, FINSEQ_1:2, FINSEQ_1:38; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {1} or x in dom (product" (JumpParts T)) )
assume A4: x in {1} ; ::_thesis: x in dom (product" (JumpParts T))
for f being Function st f in JumpParts T holds
x in dom f
proof
let f be Function; ::_thesis: ( f in JumpParts T implies x in dom f )
assume f in JumpParts T ; ::_thesis: x in dom f
then consider I being Instruction of SCM+FSA such that
A5: f = JumpPart I and
A6: InsCode I = T ;
consider i1 being Element of NAT , a being Int-Location such that
A7: I = a >0_goto i1 by A1, A6, SCMFSA_2:37;
f = <*i1*> by A5, A7, Th16;
hence x in dom f by A4, FINSEQ_1:2, FINSEQ_1:38; ::_thesis: verum
end;
then x in DOM (JumpParts T) by CARD_3:109;
hence x in dom (product" (JumpParts T)) by CARD_3:def_12; ::_thesis: verum
end;
theorem :: SCMFSA10:26
for T being InsType of the InstructionsF of SCM+FSA st T = 9 holds
JumpParts T = {{}}
proof
let T be InsType of the InstructionsF of SCM+FSA; ::_thesis: ( T = 9 implies JumpParts T = {{}} )
assume A1: T = 9 ; ::_thesis: JumpParts T = {{}}
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= JumpParts T
let x be set ; ::_thesis: ( x in JumpParts T implies x in {{}} )
assume x in JumpParts T ; ::_thesis: x in {{}}
then consider I being Instruction of SCM+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T ;
consider a, b being Int-Location, f being FinSeq-Location such that
A4: I = b := (f,a) by A1, A3, SCMFSA_2:38;
x = {} by A2, A4, RECDEF_2:def_2;
hence x in {{}} by TARSKI:def_1; ::_thesis: verum
end;
set a = the Int-Location;
set f = the FinSeq-Location ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T )
assume x in {{}} ; ::_thesis: x in JumpParts T
then x = {} by TARSKI:def_1;
then A5: x = JumpPart ( the Int-Location := ( the FinSeq-Location , the Int-Location)) by RECDEF_2:def_2;
InsCode ( the Int-Location := ( the FinSeq-Location , the Int-Location)) = 9 by SCMFSA_2:26;
hence x in JumpParts T by A5, A1; ::_thesis: verum
end;
theorem :: SCMFSA10:27
for T being InsType of the InstructionsF of SCM+FSA st T = 10 holds
JumpParts T = {{}}
proof
let T be InsType of the InstructionsF of SCM+FSA; ::_thesis: ( T = 10 implies JumpParts T = {{}} )
assume A1: T = 10 ; ::_thesis: JumpParts T = {{}}
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= JumpParts T
let x be set ; ::_thesis: ( x in JumpParts T implies x in {{}} )
assume x in JumpParts T ; ::_thesis: x in {{}}
then consider I being Instruction of SCM+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T ;
consider a, b being Int-Location, f being FinSeq-Location such that
A4: I = (f,a) := b by A1, A3, SCMFSA_2:39;
x = {} by A2, A4, RECDEF_2:def_2;
hence x in {{}} by TARSKI:def_1; ::_thesis: verum
end;
set a = the Int-Location;
set f = the FinSeq-Location ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T )
assume x in {{}} ; ::_thesis: x in JumpParts T
then x = {} by TARSKI:def_1;
then A5: x = JumpPart (( the FinSeq-Location , the Int-Location) := the Int-Location) by RECDEF_2:def_2;
InsCode (( the FinSeq-Location , the Int-Location) := the Int-Location) = 10 by SCMFSA_2:27;
hence x in JumpParts T by A5, A1; ::_thesis: verum
end;
theorem :: SCMFSA10:28
for T being InsType of the InstructionsF of SCM+FSA st T = 11 holds
JumpParts T = {{}}
proof
let T be InsType of the InstructionsF of SCM+FSA; ::_thesis: ( T = 11 implies JumpParts T = {{}} )
assume A1: T = 11 ; ::_thesis: JumpParts T = {{}}
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= JumpParts T
let x be set ; ::_thesis: ( x in JumpParts T implies x in {{}} )
assume x in JumpParts T ; ::_thesis: x in {{}}
then consider I being Instruction of SCM+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T ;
consider a being Int-Location, f being FinSeq-Location such that
A4: I = a :=len f by A1, A3, SCMFSA_2:40;
x = {} by A2, A4, RECDEF_2:def_2;
hence x in {{}} by TARSKI:def_1; ::_thesis: verum
end;
set a = the Int-Location;
set f = the FinSeq-Location ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T )
assume x in {{}} ; ::_thesis: x in JumpParts T
then x = {} by TARSKI:def_1;
then A5: x = JumpPart ( the Int-Location :=len the FinSeq-Location ) by RECDEF_2:def_2;
InsCode ( the Int-Location :=len the FinSeq-Location ) = 11 by SCMFSA_2:28;
hence x in JumpParts T by A5, A1; ::_thesis: verum
end;
theorem :: SCMFSA10:29
for T being InsType of the InstructionsF of SCM+FSA st T = 12 holds
JumpParts T = {{}}
proof
let T be InsType of the InstructionsF of SCM+FSA; ::_thesis: ( T = 12 implies JumpParts T = {{}} )
assume A1: T = 12 ; ::_thesis: JumpParts T = {{}}
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= JumpParts T
let x be set ; ::_thesis: ( x in JumpParts T implies x in {{}} )
assume x in JumpParts T ; ::_thesis: x in {{}}
then consider I being Instruction of SCM+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T ;
consider a being Int-Location, f being FinSeq-Location such that
A4: I = f :=<0,...,0> a by A1, A3, SCMFSA_2:41;
x = {} by A2, A4, RECDEF_2:def_2;
hence x in {{}} by TARSKI:def_1; ::_thesis: verum
end;
set a = the Int-Location;
set f = the FinSeq-Location ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T )
assume x in {{}} ; ::_thesis: x in JumpParts T
then x = {} by TARSKI:def_1;
then A5: x = JumpPart ( the FinSeq-Location :=<0,...,0> the Int-Location) by RECDEF_2:def_2;
InsCode ( the FinSeq-Location :=<0,...,0> the Int-Location) = 12 by SCMFSA_2:29;
hence x in JumpParts T by A5, A1; ::_thesis: verum
end;
theorem :: SCMFSA10:30
for i1 being Element of NAT holds (product" (JumpParts (InsCode (goto i1)))) . 1 = NAT
proof
let i1 be Element of NAT ; ::_thesis: (product" (JumpParts (InsCode (goto i1)))) . 1 = NAT
dom (product" (JumpParts (InsCode (goto i1)))) = {1} by Th23, SCMFSA_2:23;
then A1: 1 in dom (product" (JumpParts (InsCode (goto i1)))) by TARSKI:def_1;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: NAT c= (product" (JumpParts (InsCode (goto i1)))) . 1
let x be set ; ::_thesis: ( x in (product" (JumpParts (InsCode (goto i1)))) . 1 implies x in NAT )
assume x in (product" (JumpParts (InsCode (goto i1)))) . 1 ; ::_thesis: x in NAT
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 being Element of NAT such that
A6: I = goto i2 by A5, SCMFSA_2:23, SCMFSA_2:35;
g = <*i2*> by A4, A6, RECDEF_2:def_2;
then x = i2 by A3, FINSEQ_1:def_8;
hence x in NAT ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NAT or x in (product" (JumpParts (InsCode (goto i1)))) . 1 )
assume x in NAT ; ::_thesis: x in (product" (JumpParts (InsCode (goto i1)))) . 1
then reconsider x = x as Element of NAT ;
A7: <*x*> . 1 = x by FINSEQ_1:def_8;
InsCode (goto i1) = 6 by SCMFSA_2:23;
then A8: InsCode (goto i1) = InsCode (goto x) by SCMFSA_2:23;
JumpPart (goto x) = <*x*> by RECDEF_2:def_2;
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 x in (product" (JumpParts (InsCode (goto i1)))) . 1 by A1, CARD_3:def_12; ::_thesis: verum
end;
theorem :: SCMFSA10:31
for i1 being Element of NAT
for a being Int-Location holds (product" (JumpParts (InsCode (a =0_goto i1)))) . 1 = NAT
proof
let i1 be Element of NAT ; ::_thesis: for a being Int-Location holds (product" (JumpParts (InsCode (a =0_goto i1)))) . 1 = NAT
let a be Int-Location; ::_thesis: (product" (JumpParts (InsCode (a =0_goto i1)))) . 1 = NAT
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 :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: NAT c= (product" (JumpParts (InsCode (a =0_goto i1)))) . 1
let x be set ; ::_thesis: ( x in (product" (JumpParts (InsCode (a =0_goto i1)))) . 1 implies x in NAT )
assume x in (product" (JumpParts (InsCode (a =0_goto i1)))) . 1 ; ::_thesis: x in NAT
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 being Element of NAT , b being Int-Location such that
A6: I = b =0_goto i2 by A5, SCMFSA_2:24, SCMFSA_2:36;
g = <*i2*> by A4, A6, Th15;
then x = i2 by A3, FINSEQ_1:40;
hence x in NAT ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NAT or x in (product" (JumpParts (InsCode (a =0_goto i1)))) . 1 )
assume x in NAT ; ::_thesis: x in (product" (JumpParts (InsCode (a =0_goto i1)))) . 1
then reconsider x = 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 x in (product" (JumpParts (InsCode (a =0_goto i1)))) . 1 by A1, CARD_3:def_12; ::_thesis: verum
end;
theorem :: SCMFSA10:32
for i1 being Element of NAT
for a being Int-Location holds (product" (JumpParts (InsCode (a >0_goto i1)))) . 1 = NAT
proof
let i1 be Element of NAT ; ::_thesis: for a being Int-Location holds (product" (JumpParts (InsCode (a >0_goto i1)))) . 1 = NAT
let a be Int-Location; ::_thesis: (product" (JumpParts (InsCode (a >0_goto i1)))) . 1 = NAT
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 :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: NAT c= (product" (JumpParts (InsCode (a >0_goto i1)))) . 1
let x be set ; ::_thesis: ( x in (product" (JumpParts (InsCode (a >0_goto i1)))) . 1 implies x in NAT )
assume x in (product" (JumpParts (InsCode (a >0_goto i1)))) . 1 ; ::_thesis: x in NAT
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 being Element of NAT , b being Int-Location such that
A6: I = b >0_goto i2 by A5, SCMFSA_2:25, SCMFSA_2:37;
g = <*i2*> by A4, A6, Th16;
then x = i2 by A3, FINSEQ_1:40;
hence x in NAT ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NAT or x in (product" (JumpParts (InsCode (a >0_goto i1)))) . 1 )
assume x in NAT ; ::_thesis: x in (product" (JumpParts (InsCode (a >0_goto i1)))) . 1
then reconsider x = 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 x in (product" (JumpParts (InsCode (a >0_goto i1)))) . 1 by A1, CARD_3:def_12; ::_thesis: verum
end;
Lm1: for i being Instruction of SCM+FSA st ( for l being Element of NAT holds NIC (i,l) = {(succ l)} ) holds
JUMP i is empty
proof
reconsider p = 0 , q = 1 as Element of NAT ;
let i be Instruction of SCM+FSA; ::_thesis: ( ( for l being Element of NAT holds NIC (i,l) = {(succ l)} ) implies JUMP i is empty )
assume A1: for l being Element of NAT holds NIC (i,l) = {(succ l)} ; ::_thesis: JUMP i is empty
set X = { (NIC (i,f)) where f is Element of NAT : verum } ;
reconsider p = p, q = q as Element of NAT ;
assume not JUMP i is empty ; ::_thesis: contradiction
then consider x being set such that
A2: x in meet { (NIC (i,f)) where f is Element of NAT : verum } by XBOOLE_0:def_1;
NIC (i,p) = {(succ p)} by A1;
then {(succ p)} in { (NIC (i,f)) where f is Element of NAT : verum } ;
then x in {(succ p)} by A2, SETFAM_1:def_1;
then A3: x = succ p by TARSKI:def_1;
NIC (i,q) = {(succ q)} by A1;
then {(succ q)} in { (NIC (i,f)) where f is Element of NAT : verum } ;
then x in {(succ q)} by A2, SETFAM_1:def_1;
hence contradiction by A3, TARSKI:def_1; ::_thesis: verum
end;
registration
cluster JUMP (halt SCM+FSA) -> empty ;
coherence
JUMP (halt SCM+FSA) is empty ;
end;
registration
let a, b be Int-Location;
clustera := b -> sequential ;
coherence
a := b is sequential
proof
let s be State of SCM+FSA; :: according to AMISTD_1:def_8 ::_thesis: (Exec ((a := b),s)) . (IC ) = succ (IC s)
thus (Exec ((a := b),s)) . (IC ) = succ (IC s) by SCMFSA_2:63; ::_thesis: verum
end;
cluster AddTo (a,b) -> sequential ;
coherence
AddTo (a,b) is sequential
proof
let s be State of SCM+FSA; :: according to AMISTD_1:def_8 ::_thesis: (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s)
thus (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) by SCMFSA_2:64; ::_thesis: verum
end;
cluster SubFrom (a,b) -> sequential ;
coherence
SubFrom (a,b) is sequential
proof
let s be State of SCM+FSA; :: according to AMISTD_1:def_8 ::_thesis: (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s)
thus (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) by SCMFSA_2:65; ::_thesis: verum
end;
cluster MultBy (a,b) -> sequential ;
coherence
MultBy (a,b) is sequential
proof
let s be State of SCM+FSA; :: according to AMISTD_1:def_8 ::_thesis: (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s)
thus (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) by SCMFSA_2:66; ::_thesis: verum
end;
cluster Divide (a,b) -> sequential ;
coherence
Divide (a,b) is sequential
proof
let s be State of SCM+FSA; :: according to AMISTD_1:def_8 ::_thesis: (Exec ((Divide (a,b)),s)) . (IC ) = succ (IC s)
thus (Exec ((Divide (a,b)),s)) . (IC ) = succ (IC s) by SCMFSA_2:67; ::_thesis: verum
end;
end;
registration
let a, b be Int-Location;
cluster JUMP (a := b) -> empty ;
coherence
JUMP (a := b) is empty
proof
for l being Element of NAT holds NIC ((a := b),l) = {(succ l)} by AMISTD_1:12;
hence JUMP (a := b) is empty by Lm1; ::_thesis: verum
end;
cluster JUMP (AddTo (a,b)) -> empty ;
coherence
JUMP (AddTo (a,b)) is empty
proof
for l being Element of NAT holds NIC ((AddTo (a,b)),l) = {(succ l)} by AMISTD_1:12;
hence JUMP (AddTo (a,b)) is empty by Lm1; ::_thesis: verum
end;
cluster JUMP (SubFrom (a,b)) -> empty ;
coherence
JUMP (SubFrom (a,b)) is empty
proof
for l being Element of NAT holds NIC ((SubFrom (a,b)),l) = {(succ l)} by AMISTD_1:12;
hence JUMP (SubFrom (a,b)) is empty by Lm1; ::_thesis: verum
end;
cluster JUMP (MultBy (a,b)) -> empty ;
coherence
JUMP (MultBy (a,b)) is empty
proof
for l being Element of NAT holds NIC ((MultBy (a,b)),l) = {(succ l)} by AMISTD_1:12;
hence JUMP (MultBy (a,b)) is empty by Lm1; ::_thesis: verum
end;
cluster JUMP (Divide (a,b)) -> empty ;
coherence
JUMP (Divide (a,b)) is empty
proof
for l being Element of NAT holds NIC ((Divide (a,b)),l) = {(succ l)} by AMISTD_1:12;
hence JUMP (Divide (a,b)) is empty by Lm1; ::_thesis: verum
end;
end;
theorem Th33: :: SCMFSA10:33
for i1, il being Element of NAT holds NIC ((goto i1),il) = {i1}
proof
let i1, il be Element of NAT ; ::_thesis: NIC ((goto i1),il) = {i1}
now__::_thesis:_for_x_being_set_holds_
(_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__}__)
let x be set ; ::_thesis: ( 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 } )
A1: now__::_thesis:_(_x_=_i1_implies_x_in__{__(IC_(Exec_((goto_i1),s)))_where_s_is_Element_of_product_(the_Values_of_SCM+FSA)_:_IC_s_=_il__}__)
reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def_6;
reconsider n = il1 as Element of NAT ;
set I = goto i1;
set t = the State of SCM+FSA;
set Q = the Instruction-Sequence of SCM+FSA;
assume A2: x = i1 ; ::_thesis: x in { (IC (Exec ((goto i1),s))) where s is Element of product (the_Values_of SCM+FSA) : IC s = il }
reconsider u = the State of SCM+FSA +* ((IC ),il1) as Element of product (the_Values_of SCM+FSA) by CARD_3:107;
reconsider P = the Instruction-Sequence of SCM+FSA +* (il,(goto i1)) as Instruction-Sequence of SCM+FSA ;
IC in dom the State of SCM+FSA by MEMSTR_0:2;
then A3: IC u = n by FUNCT_7:31;
A4: P /. il = P . il by PBOOLE:143;
il in NAT ;
then il in dom the Instruction-Sequence of SCM+FSA by PARTFUN1:def_2;
then A5: P . n = goto i1 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; ::_thesis: verum
end;
now__::_thesis:_(_x_in__{__(IC_(Exec_((goto_i1),s)))_where_s_is_Element_of_product_(the_Values_of_SCM+FSA)_:_IC_s_=_il__}__implies_x_=_i1_)
assume x in { (IC (Exec ((goto i1),s))) where s is Element of product (the_Values_of SCM+FSA) : IC s = il } ; ::_thesis: x = i1
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; ::_thesis: verum
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; ::_thesis: verum
end;
hence NIC ((goto i1),il) = {i1} by TARSKI:1; ::_thesis: verum
end;
theorem Th34: :: SCMFSA10:34
for i1 being Element of NAT holds JUMP (goto i1) = {i1}
proof
let i1 be Element of NAT ; ::_thesis: JUMP (goto i1) = {i1}
set X = { (NIC ((goto i1),il)) where il is Element of NAT : verum } ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_meet__{__(NIC_((goto_i1),il))_where_il_is_Element_of_NAT_:_verum__}__implies_x_in_{i1}_)_&_(_x_in_{i1}_implies_x_in_meet__{__(NIC_((goto_i1),il))_where_il_is_Element_of_NAT_:_verum__}__)_)
let x be set ; ::_thesis: ( ( x in meet { (NIC ((goto i1),il)) where il is Element of NAT : verum } implies x in {i1} ) & ( x in {i1} implies x in meet { (NIC ((goto i1),il)) where il is Element of NAT : verum } ) )
hereby ::_thesis: ( x in {i1} implies x in meet { (NIC ((goto i1),il)) where il is Element of NAT : verum } )
set il1 = 1;
A1: NIC ((goto i1),1) in { (NIC ((goto i1),il)) where il is Element of NAT : verum } ;
assume x in meet { (NIC ((goto i1),il)) where il is Element of NAT : verum } ; ::_thesis: x in {i1}
then x in NIC ((goto i1),1) by A1, SETFAM_1:def_1;
hence x in {i1} by Th33; ::_thesis: verum
end;
assume x in {i1} ; ::_thesis: x in meet { (NIC ((goto i1),il)) where il is Element of NAT : verum }
then A2: x = i1 by TARSKI:def_1;
A3: now__::_thesis:_for_Y_being_set_st_Y_in__{__(NIC_((goto_i1),il))_where_il_is_Element_of_NAT_:_verum__}__holds_
i1_in_Y
let Y be set ; ::_thesis: ( Y in { (NIC ((goto i1),il)) where il is Element of NAT : verum } implies i1 in Y )
assume Y in { (NIC ((goto i1),il)) where il is Element of NAT : verum } ; ::_thesis: i1 in Y
then consider il being Element of 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; ::_thesis: verum
end;
NIC ((goto i1),i1) in { (NIC ((goto i1),il)) where il is Element of NAT : verum } ;
hence x in meet { (NIC ((goto i1),il)) where il is Element of NAT : verum } by A2, A3, SETFAM_1:def_1; ::_thesis: verum
end;
hence JUMP (goto i1) = {i1} by TARSKI:1; ::_thesis: verum
end;
registration
let i1 be Element of NAT ;
cluster JUMP (goto i1) -> 1 -element ;
coherence
JUMP (goto i1) is 1 -element
proof
JUMP (goto i1) = {i1} by Th34;
hence JUMP (goto i1) is 1 -element ; ::_thesis: verum
end;
end;
theorem Th35: :: SCMFSA10:35
for i1, il being Element of NAT
for a being Int-Location holds NIC ((a =0_goto i1),il) = {i1,(succ il)}
proof
let i1, il be Element of NAT ; ::_thesis: for a being Int-Location holds NIC ((a =0_goto i1),il) = {i1,(succ il)}
let a be Int-Location; ::_thesis: NIC ((a =0_goto i1),il) = {i1,(succ il)}
set t = the State of SCM+FSA;
set Q = the Instruction-Sequence of SCM+FSA;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {i1,(succ il)} c= NIC ((a =0_goto i1),il)
let x be set ; ::_thesis: ( x in NIC ((a =0_goto i1),il) implies b1 in {i1,(succ il)} )
assume x in NIC ((a =0_goto i1),il) ; ::_thesis: b1 in {i1,(succ 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 ;
percases ( s . a = 0 or s . a <> 0 ) ;
suppose s . a = 0 ; ::_thesis: b1 in {i1,(succ il)}
then x = i1 by A1, SCMFSA_2:70;
hence x in {i1,(succ il)} by TARSKI:def_2; ::_thesis: verum
end;
suppose s . a <> 0 ; ::_thesis: b1 in {i1,(succ il)}
then x = succ il by A1, A2, SCMFSA_2:70;
hence x in {i1,(succ il)} by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {i1,(succ il)} or x in NIC ((a =0_goto i1),il) )
set I = a =0_goto i1;
A3: IC <> a by SCMFSA_2:56;
reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def_6;
reconsider u = the State of SCM+FSA +* ((IC ),il1) as Element of product (the_Values_of SCM+FSA) by CARD_3:107;
reconsider P = the Instruction-Sequence of SCM+FSA +* (il,(a =0_goto i1)) as Instruction-Sequence of SCM+FSA ;
reconsider n = il as Element of NAT ;
assume A4: x in {i1,(succ il)} ; ::_thesis: x in NIC ((a =0_goto i1),il)
percases ( x = i1 or x = succ il ) by A4, TARSKI:def_2;
supposeA5: x = i1 ; ::_thesis: x in NIC ((a =0_goto i1),il)
reconsider v = u +* (a .--> 0) as Element of product (the_Values_of SCM+FSA) by CARD_3:107;
A6: IC in dom the State of SCM+FSA by MEMSTR_0:2;
A7: dom (a .--> 0) = {a} by FUNCOP_1:13;
then not IC 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 ;
A9: P /. il = P . il by PBOOLE:143;
il in NAT ;
then il in dom the Instruction-Sequence of SCM+FSA by PARTFUN1:def_2;
then A10: P . il = a =0_goto i1 by FUNCT_7:31;
a in dom (a .--> 0) by A7, 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 x in NIC ((a =0_goto i1),il) by A5, A8, A10, A9; ::_thesis: verum
end;
supposeA11: x = succ il ; ::_thesis: x in NIC ((a =0_goto i1),il)
reconsider v = u +* (a .--> 1) as Element of product (the_Values_of SCM+FSA) by CARD_3:107;
A12: IC in dom the State of SCM+FSA by MEMSTR_0:2;
A13: dom (a .--> 1) = {a} by FUNCOP_1:13;
then not IC 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 ;
A15: P /. il = P . il by PBOOLE:143;
il in NAT ;
then il in dom the Instruction-Sequence of SCM+FSA by PARTFUN1:def_2;
then A16: P . il = a =0_goto i1 by FUNCT_7:31;
a in dom (a .--> 1) by A13, TARSKI:def_1;
then v . a = (a .--> 1) . a by FUNCT_4:13
.= 1 by FUNCOP_1:72 ;
then IC (Following (P,v)) = succ il by A14, A16, A15, SCMFSA_2:70;
hence x in NIC ((a =0_goto i1),il) by A11, A14, A16, A15; ::_thesis: verum
end;
end;
end;
theorem Th36: :: SCMFSA10:36
for i1 being Element of NAT
for a being Int-Location holds JUMP (a =0_goto i1) = {i1}
proof
let i1 be Element of NAT ; ::_thesis: for a being Int-Location holds JUMP (a =0_goto i1) = {i1}
let a be Int-Location; ::_thesis: JUMP (a =0_goto i1) = {i1}
set X = { (NIC ((a =0_goto i1),il)) where il is Element of NAT : verum } ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_meet__{__(NIC_((a_=0_goto_i1),il))_where_il_is_Element_of_NAT_:_verum__}__implies_x_in_{i1}_)_&_(_x_in_{i1}_implies_x_in_meet__{__(NIC_((a_=0_goto_i1),il))_where_il_is_Element_of_NAT_:_verum__}__)_)
let x be set ; ::_thesis: ( ( x in meet { (NIC ((a =0_goto i1),il)) where il is Element of NAT : verum } implies x in {i1} ) & ( x in {i1} implies x in meet { (NIC ((a =0_goto i1),il)) where il is Element of NAT : verum } ) )
A1: now__::_thesis:_for_Y_being_set_st_Y_in__{__(NIC_((a_=0_goto_i1),il))_where_il_is_Element_of_NAT_:_verum__}__holds_
i1_in_Y
let Y be set ; ::_thesis: ( Y in { (NIC ((a =0_goto i1),il)) where il is Element of NAT : verum } implies i1 in Y )
assume Y in { (NIC ((a =0_goto i1),il)) where il is Element of NAT : verum } ; ::_thesis: i1 in Y
then consider il being Element of NAT such that
A2: Y = NIC ((a =0_goto i1),il) ;
NIC ((a =0_goto i1),il) = {i1,(succ il)} by Th35;
hence i1 in Y by A2, TARSKI:def_2; ::_thesis: verum
end;
hereby ::_thesis: ( x in {i1} implies x in meet { (NIC ((a =0_goto i1),il)) where il is Element of NAT : verum } )
set il1 = 1;
set il2 = 2;
assume A3: x in meet { (NIC ((a =0_goto i1),il)) where il is Element of NAT : verum } ; ::_thesis: x in {i1}
A4: NIC ((a =0_goto i1),2) = {i1,(succ 2)} by Th35;
NIC ((a =0_goto i1),2) in { (NIC ((a =0_goto i1),il)) where il is Element of NAT : verum } ;
then x in NIC ((a =0_goto i1),2) by A3, SETFAM_1:def_1;
then A5: ( x = i1 or x = succ 2 ) by A4, TARSKI:def_2;
A6: NIC ((a =0_goto i1),1) = {i1,(succ 1)} by Th35;
NIC ((a =0_goto i1),1) in { (NIC ((a =0_goto i1),il)) where il is Element of NAT : verum } ;
then x in NIC ((a =0_goto i1),1) by A3, SETFAM_1:def_1;
then ( x = i1 or x = succ 1 ) by A6, TARSKI:def_2;
hence x in {i1} by A5, TARSKI:def_1; ::_thesis: verum
end;
assume x in {i1} ; ::_thesis: x in meet { (NIC ((a =0_goto i1),il)) where il is Element of NAT : verum }
then A7: x = i1 by TARSKI:def_1;
NIC ((a =0_goto i1),i1) in { (NIC ((a =0_goto i1),il)) where il is Element of NAT : verum } ;
hence x in meet { (NIC ((a =0_goto i1),il)) where il is Element of NAT : verum } by A7, A1, SETFAM_1:def_1; ::_thesis: verum
end;
hence JUMP (a =0_goto i1) = {i1} by TARSKI:1; ::_thesis: verum
end;
registration
let a be Int-Location;
let i1 be Element of NAT ;
cluster JUMP (a =0_goto i1) -> 1 -element ;
coherence
JUMP (a =0_goto i1) is 1 -element
proof
JUMP (a =0_goto i1) = {i1} by Th36;
hence JUMP (a =0_goto i1) is 1 -element ; ::_thesis: verum
end;
end;
theorem Th37: :: SCMFSA10:37
for i1, il being Element of NAT
for a being Int-Location holds NIC ((a >0_goto i1),il) = {i1,(succ il)}
proof
let i1, il be Element of NAT ; ::_thesis: for a being Int-Location holds NIC ((a >0_goto i1),il) = {i1,(succ il)}
let a be Int-Location; ::_thesis: NIC ((a >0_goto i1),il) = {i1,(succ il)}
set t = the State of SCM+FSA;
set Q = the Instruction-Sequence of SCM+FSA;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {i1,(succ il)} c= NIC ((a >0_goto i1),il)
let x be set ; ::_thesis: ( x in NIC ((a >0_goto i1),il) implies b1 in {i1,(succ il)} )
assume x in NIC ((a >0_goto i1),il) ; ::_thesis: b1 in {i1,(succ 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 ;
percases ( s . a > 0 or s . a <= 0 ) ;
suppose s . a > 0 ; ::_thesis: b1 in {i1,(succ il)}
then x = i1 by A1, SCMFSA_2:71;
hence x in {i1,(succ il)} by TARSKI:def_2; ::_thesis: verum
end;
suppose s . a <= 0 ; ::_thesis: b1 in {i1,(succ il)}
then x = succ il by A1, A2, SCMFSA_2:71;
hence x in {i1,(succ il)} by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {i1,(succ il)} or x in NIC ((a >0_goto i1),il) )
set I = a >0_goto i1;
A3: IC <> a by SCMFSA_2:56;
reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def_6;
reconsider n = il as Element of NAT ;
reconsider u = the State of SCM+FSA +* ((IC ),il1) as Element of product (the_Values_of SCM+FSA) by CARD_3:107;
reconsider P = the Instruction-Sequence of SCM+FSA +* (il,(a >0_goto i1)) as Instruction-Sequence of SCM+FSA ;
assume A4: x in {i1,(succ il)} ; ::_thesis: x in NIC ((a >0_goto i1),il)
percases ( x = i1 or x = succ il ) by A4, TARSKI:def_2;
supposeA5: x = i1 ; ::_thesis: x in NIC ((a >0_goto i1),il)
reconsider v = u +* (a .--> 1) as Element of product (the_Values_of SCM+FSA) by CARD_3:107;
A6: IC in dom the State of SCM+FSA by MEMSTR_0:2;
A7: dom (a .--> 1) = {a} by FUNCOP_1:13;
then not IC 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 ;
A9: P /. il = P . il by PBOOLE:143;
il in NAT ;
then il in dom the Instruction-Sequence of SCM+FSA by PARTFUN1:def_2;
then A10: P . il = a >0_goto i1 by FUNCT_7:31;
a in dom (a .--> 1) by A7, 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 x in NIC ((a >0_goto i1),il) by A5, A8, A10, A9; ::_thesis: verum
end;
supposeA11: x = succ il ; ::_thesis: x in NIC ((a >0_goto i1),il)
reconsider v = u +* (a .--> 0) as Element of product (the_Values_of SCM+FSA) by CARD_3:107;
A12: IC in dom the State of SCM+FSA by MEMSTR_0:2;
A13: dom (a .--> 0) = {a} by FUNCOP_1:13;
then not IC 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 ;
A15: P /. il = P . il by PBOOLE:143;
il in NAT ;
then il in dom the Instruction-Sequence of SCM+FSA by PARTFUN1:def_2;
then A16: P . il = a >0_goto i1 by FUNCT_7:31;
a in dom (a .--> 0) by A13, TARSKI:def_1;
then v . a = (a .--> 0) . a by FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
then IC (Following (P,v)) = succ il by A14, A16, A15, SCMFSA_2:71;
hence x in NIC ((a >0_goto i1),il) by A11, A14, A16, A15; ::_thesis: verum
end;
end;
end;
theorem Th38: :: SCMFSA10:38
for i1 being Element of NAT
for a being Int-Location holds JUMP (a >0_goto i1) = {i1}
proof
let i1 be Element of NAT ; ::_thesis: for a being Int-Location holds JUMP (a >0_goto i1) = {i1}
let a be Int-Location; ::_thesis: JUMP (a >0_goto i1) = {i1}
set X = { (NIC ((a >0_goto i1),il)) where il is Element of NAT : verum } ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_meet__{__(NIC_((a_>0_goto_i1),il))_where_il_is_Element_of_NAT_:_verum__}__implies_x_in_{i1}_)_&_(_x_in_{i1}_implies_x_in_meet__{__(NIC_((a_>0_goto_i1),il))_where_il_is_Element_of_NAT_:_verum__}__)_)
let x be set ; ::_thesis: ( ( x in meet { (NIC ((a >0_goto i1),il)) where il is Element of NAT : verum } implies x in {i1} ) & ( x in {i1} implies x in meet { (NIC ((a >0_goto i1),il)) where il is Element of NAT : verum } ) )
A1: now__::_thesis:_for_Y_being_set_st_Y_in__{__(NIC_((a_>0_goto_i1),il))_where_il_is_Element_of_NAT_:_verum__}__holds_
i1_in_Y
let Y be set ; ::_thesis: ( Y in { (NIC ((a >0_goto i1),il)) where il is Element of NAT : verum } implies i1 in Y )
assume Y in { (NIC ((a >0_goto i1),il)) where il is Element of NAT : verum } ; ::_thesis: i1 in Y
then consider il being Element of NAT such that
A2: Y = NIC ((a >0_goto i1),il) ;
NIC ((a >0_goto i1),il) = {i1,(succ il)} by Th37;
hence i1 in Y by A2, TARSKI:def_2; ::_thesis: verum
end;
hereby ::_thesis: ( x in {i1} implies x in meet { (NIC ((a >0_goto i1),il)) where il is Element of NAT : verum } )
set il1 = 1;
set il2 = 2;
assume A3: x in meet { (NIC ((a >0_goto i1),il)) where il is Element of NAT : verum } ; ::_thesis: x in {i1}
A4: NIC ((a >0_goto i1),2) = {i1,(succ 2)} by Th37;
NIC ((a >0_goto i1),2) in { (NIC ((a >0_goto i1),il)) where il is Element of NAT : verum } ;
then x in NIC ((a >0_goto i1),2) by A3, SETFAM_1:def_1;
then A5: ( x = i1 or x = succ 2 ) by A4, TARSKI:def_2;
A6: NIC ((a >0_goto i1),1) = {i1,(succ 1)} by Th37;
NIC ((a >0_goto i1),1) in { (NIC ((a >0_goto i1),il)) where il is Element of NAT : verum } ;
then x in NIC ((a >0_goto i1),1) by A3, SETFAM_1:def_1;
then ( x = i1 or x = succ 1 ) by A6, TARSKI:def_2;
hence x in {i1} by A5, TARSKI:def_1; ::_thesis: verum
end;
assume x in {i1} ; ::_thesis: x in meet { (NIC ((a >0_goto i1),il)) where il is Element of NAT : verum }
then A7: x = i1 by TARSKI:def_1;
NIC ((a >0_goto i1),i1) in { (NIC ((a >0_goto i1),il)) where il is Element of NAT : verum } ;
hence x in meet { (NIC ((a >0_goto i1),il)) where il is Element of NAT : verum } by A7, A1, SETFAM_1:def_1; ::_thesis: verum
end;
hence JUMP (a >0_goto i1) = {i1} by TARSKI:1; ::_thesis: verum
end;
registration
let a be Int-Location;
let i1 be Element of NAT ;
cluster JUMP (a >0_goto i1) -> 1 -element ;
coherence
JUMP (a >0_goto i1) is 1 -element
proof
JUMP (a >0_goto i1) = {i1} by Th38;
hence JUMP (a >0_goto i1) is 1 -element ; ::_thesis: verum
end;
end;
registration
let a, b be Int-Location;
let f be FinSeq-Location ;
clustera := (f,b) -> sequential ;
coherence
a := (f,b) is sequential
proof
let s be State of SCM+FSA; :: according to AMISTD_1:def_8 ::_thesis: (Exec ((a := (f,b)),s)) . (IC ) = succ (IC s)
thus (Exec ((a := (f,b)),s)) . (IC ) = succ (IC s) by SCMFSA_2:72; ::_thesis: verum
end;
end;
registration
let a, b be Int-Location;
let f be FinSeq-Location ;
cluster JUMP (a := (f,b)) -> empty ;
coherence
JUMP (a := (f,b)) is empty
proof
for l being Element of NAT holds NIC ((a := (f,b)),l) = {(succ l)} by AMISTD_1:12;
hence JUMP (a := (f,b)) is empty by Lm1; ::_thesis: verum
end;
end;
registration
let a, b be Int-Location;
let f be FinSeq-Location ;
cluster(f,b) := a -> sequential ;
coherence
(f,b) := a is sequential
proof
let s be State of SCM+FSA; :: according to AMISTD_1:def_8 ::_thesis: (Exec (((f,b) := a),s)) . (IC ) = succ (IC s)
thus (Exec (((f,b) := a),s)) . (IC ) = succ (IC s) by SCMFSA_2:73; ::_thesis: verum
end;
end;
registration
let a, b be Int-Location;
let f be FinSeq-Location ;
cluster JUMP ((f,b) := a) -> empty ;
coherence
JUMP ((f,b) := a) is empty
proof
for l being Element of NAT holds NIC (((f,b) := a),l) = {(succ l)} by AMISTD_1:12;
hence JUMP ((f,b) := a) is empty by Lm1; ::_thesis: verum
end;
end;
registration
let a be Int-Location;
let f be FinSeq-Location ;
clustera :=len f -> sequential ;
coherence
a :=len f is sequential
proof
let s be State of SCM+FSA; :: according to AMISTD_1:def_8 ::_thesis: (Exec ((a :=len f),s)) . (IC ) = succ (IC s)
thus (Exec ((a :=len f),s)) . (IC ) = succ (IC s) by SCMFSA_2:74; ::_thesis: verum
end;
end;
registration
let a be Int-Location;
let f be FinSeq-Location ;
cluster JUMP (a :=len f) -> empty ;
coherence
JUMP (a :=len f) is empty
proof
for l being Element of NAT holds NIC ((a :=len f),l) = {(succ l)} by AMISTD_1:12;
hence JUMP (a :=len f) is empty by Lm1; ::_thesis: verum
end;
end;
registration
let a be Int-Location;
let f be FinSeq-Location ;
clusterf :=<0,...,0> a -> sequential ;
coherence
f :=<0,...,0> a is sequential
proof
let s be State of SCM+FSA; :: according to AMISTD_1:def_8 ::_thesis: (Exec ((f :=<0,...,0> a),s)) . (IC ) = succ (IC s)
thus (Exec ((f :=<0,...,0> a),s)) . (IC ) = succ (IC s) by SCMFSA_2:75; ::_thesis: verum
end;
end;
registration
let a be Int-Location;
let f be FinSeq-Location ;
cluster JUMP (f :=<0,...,0> a) -> empty ;
coherence
JUMP (f :=<0,...,0> a) is empty
proof
for l being Element of NAT holds NIC ((f :=<0,...,0> a),l) = {(succ l)} by AMISTD_1:12;
hence JUMP (f :=<0,...,0> a) is empty by Lm1; ::_thesis: verum
end;
end;
theorem Th39: :: SCMFSA10:39
for il being Element of NAT holds SUCC (il,SCM+FSA) = {il,(succ il)}
proof
let il be Element of NAT ; ::_thesis: SUCC (il,SCM+FSA) = {il,(succ il)}
set X = { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM+FSA : verum } ;
set N = {il,(succ il)};
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_union__{__((NIC_(I,il))_\_(JUMP_I))_where_I_is_Element_of_the_InstructionsF_of_SCM+FSA_:_verum__}__implies_x_in_{il,(succ_il)}_)_&_(_x_in_{il,(succ_il)}_implies_x_in_union__{__((NIC_(I,il))_\_(JUMP_I))_where_I_is_Element_of_the_InstructionsF_of_SCM+FSA_:_verum__}__)_)
let x be set ; ::_thesis: ( ( x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM+FSA : verum } implies x in {il,(succ il)} ) & ( x in {il,(succ il)} implies b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of SCM+FSA : verum } ) )
hereby ::_thesis: ( x in {il,(succ il)} implies b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of SCM+FSA : verum } )
assume x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM+FSA : verum } ; ::_thesis: x in {il,(succ il)}
then consider Y being set such that
A1: x in Y and
A2: Y in { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM+FSA : verum } 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;
percases ( i = [0,{},{}] or ex a, b being Int-Location st i = a := b or ex a, b being Int-Location st i = AddTo (a,b) or ex a, b being Int-Location st i = SubFrom (a,b) or ex a, b being Int-Location st i = MultBy (a,b) or ex a, b being Int-Location st i = Divide (a,b) or ex i1 being Element of NAT st i = goto i1 or ex i1 being Element of NAT ex a being Int-Location st i = a =0_goto i1 or ex i1 being Element of NAT ex a being Int-Location st i = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st i = b := (f,a) or ex a, b being Int-Location ex f being FinSeq-Location st i = (f,a) := b or ex a being Int-Location ex f being FinSeq-Location st i = a :=len f or ex a being Int-Location ex f being FinSeq-Location st i = f :=<0,...,0> a ) by SCMFSA_2:93;
suppose i = [0,{},{}] ; ::_thesis: x in {il,(succ il)}
then x in {il} \ (JUMP (halt SCM+FSA)) by A1, A3, AMISTD_1:2;
then x = il by TARSKI:def_1;
hence x in {il,(succ il)} by TARSKI:def_2; ::_thesis: verum
end;
suppose ex a, b being Int-Location st i = a := b ; ::_thesis: x in {il,(succ il)}
then consider a, b being Int-Location such that
A4: i = a := b ;
x in {(succ il)} \ (JUMP (a := b)) by A1, A3, A4, AMISTD_1:12;
then x = succ il by TARSKI:def_1;
hence x in {il,(succ il)} by TARSKI:def_2; ::_thesis: verum
end;
suppose ex a, b being Int-Location st i = AddTo (a,b) ; ::_thesis: x in {il,(succ il)}
then consider a, b being Int-Location such that
A5: i = AddTo (a,b) ;
x in {(succ il)} \ (JUMP (AddTo (a,b))) by A1, A3, A5, AMISTD_1:12;
then x = succ il by TARSKI:def_1;
hence x in {il,(succ il)} by TARSKI:def_2; ::_thesis: verum
end;
suppose ex a, b being Int-Location st i = SubFrom (a,b) ; ::_thesis: x in {il,(succ il)}
then consider a, b being Int-Location such that
A6: i = SubFrom (a,b) ;
x in {(succ il)} \ (JUMP (SubFrom (a,b))) by A1, A3, A6, AMISTD_1:12;
then x = succ il by TARSKI:def_1;
hence x in {il,(succ il)} by TARSKI:def_2; ::_thesis: verum
end;
suppose ex a, b being Int-Location st i = MultBy (a,b) ; ::_thesis: x in {il,(succ il)}
then consider a, b being Int-Location such that
A7: i = MultBy (a,b) ;
x in {(succ il)} \ (JUMP (MultBy (a,b))) by A1, A3, A7, AMISTD_1:12;
then x = succ il by TARSKI:def_1;
hence x in {il,(succ il)} by TARSKI:def_2; ::_thesis: verum
end;
suppose ex a, b being Int-Location st i = Divide (a,b) ; ::_thesis: x in {il,(succ il)}
then consider a, b being Int-Location such that
A8: i = Divide (a,b) ;
x in {(succ il)} \ (JUMP (Divide (a,b))) by A1, A3, A8, AMISTD_1:12;
then x = succ il by TARSKI:def_1;
hence x in {il,(succ il)} by TARSKI:def_2; ::_thesis: verum
end;
suppose ex i1 being Element of NAT st i = goto i1 ; ::_thesis: x in {il,(succ il)}
then consider i1 being Element of NAT 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 {il,(succ il)} by XBOOLE_1:37; ::_thesis: verum
end;
suppose ex i1 being Element of NAT ex a being Int-Location st i = a =0_goto i1 ; ::_thesis: x in {il,(succ il)}
then consider i1 being Element of NAT , a being Int-Location such that
A10: i = a =0_goto i1 ;
A11: NIC (i,il) = {i1,(succ il)} by A10, Th35;
x in NIC (i,il) by A1, A3, XBOOLE_0:def_5;
then A12: ( x = i1 or x = succ il ) 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 {il,(succ il)} by A12, TARSKI:def_1, TARSKI:def_2; ::_thesis: verum
end;
suppose ex i1 being Element of NAT ex a being Int-Location st i = a >0_goto i1 ; ::_thesis: x in {il,(succ il)}
then consider i1 being Element of NAT , a being Int-Location such that
A13: i = a >0_goto i1 ;
A14: NIC (i,il) = {i1,(succ il)} by A13, Th37;
x in NIC (i,il) by A1, A3, XBOOLE_0:def_5;
then A15: ( x = i1 or x = succ il ) 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 {il,(succ il)} by A15, TARSKI:def_1, TARSKI:def_2; ::_thesis: verum
end;
suppose ex a, b being Int-Location ex f being FinSeq-Location st i = b := (f,a) ; ::_thesis: x in {il,(succ il)}
then consider a, b being Int-Location, f being FinSeq-Location such that
A16: i = b := (f,a) ;
x in {(succ il)} \ (JUMP (b := (f,a))) by A1, A3, A16, AMISTD_1:12;
then x = succ il by TARSKI:def_1;
hence x in {il,(succ il)} by TARSKI:def_2; ::_thesis: verum
end;
suppose ex a, b being Int-Location ex f being FinSeq-Location st i = (f,a) := b ; ::_thesis: x in {il,(succ il)}
then consider a, b being Int-Location, f being FinSeq-Location such that
A17: i = (f,a) := b ;
x in {(succ il)} \ (JUMP ((f,a) := b)) by A1, A3, A17, AMISTD_1:12;
then x = succ il by TARSKI:def_1;
hence x in {il,(succ il)} by TARSKI:def_2; ::_thesis: verum
end;
suppose ex a being Int-Location ex f being FinSeq-Location st i = a :=len f ; ::_thesis: x in {il,(succ il)}
then consider a being Int-Location, f being FinSeq-Location such that
A18: i = a :=len f ;
x in {(succ il)} \ (JUMP (a :=len f)) by A1, A3, A18, AMISTD_1:12;
then x = succ il by TARSKI:def_1;
hence x in {il,(succ il)} by TARSKI:def_2; ::_thesis: verum
end;
suppose ex a being Int-Location ex f being FinSeq-Location st i = f :=<0,...,0> a ; ::_thesis: x in {il,(succ il)}
then consider a being Int-Location, f being FinSeq-Location such that
A19: i = f :=<0,...,0> a ;
x in {(succ il)} \ (JUMP (f :=<0,...,0> a)) by A1, A3, A19, AMISTD_1:12;
then x = succ il by TARSKI:def_1;
hence x in {il,(succ il)} by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
assume A20: x in {il,(succ il)} ; ::_thesis: b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of SCM+FSA : verum }
percases ( x = il or x = succ il ) by A20, TARSKI:def_2;
supposeA21: x = il ; ::_thesis: b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of SCM+FSA : verum }
set i = halt SCM+FSA;
(NIC ((halt SCM+FSA),il)) \ (JUMP (halt SCM+FSA)) = {il} by AMISTD_1:2;
then A22: {il} in { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM+FSA : verum } ;
x in {il} by A21, TARSKI:def_1;
hence x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM+FSA : verum } by A22, TARSKI:def_4; ::_thesis: verum
end;
supposeA23: x = succ il ; ::_thesis: b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of SCM+FSA : verum }
set a = the Int-Location;
set i = AddTo ( the Int-Location, the Int-Location);
(NIC ((AddTo ( the Int-Location, the Int-Location)),il)) \ (JUMP (AddTo ( the Int-Location, the Int-Location))) = {(succ il)} by AMISTD_1:12;
then A24: {(succ il)} in { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM+FSA : verum } ;
x in {(succ il)} by A23, TARSKI:def_1;
hence x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM+FSA : verum } by A24, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence SUCC (il,SCM+FSA) = {il,(succ il)} by TARSKI:1; ::_thesis: verum
end;
theorem Th40: :: SCMFSA10:40
for k being Element of NAT holds
( k + 1 in SUCC (k,SCM+FSA) & ( for j being Element of NAT st j in SUCC (k,SCM+FSA) holds
k <= j ) )
proof
let k be Element of NAT ; ::_thesis: ( k + 1 in SUCC (k,SCM+FSA) & ( for j being Element of NAT st j in SUCC (k,SCM+FSA) holds
k <= j ) )
A1: SUCC (k,SCM+FSA) = {k,(succ k)} by Th39;
hence k + 1 in SUCC (k,SCM+FSA) by TARSKI:def_2; ::_thesis: for j being Element of NAT st j in SUCC (k,SCM+FSA) holds
k <= j
let j be Element of NAT ; ::_thesis: ( j in SUCC (k,SCM+FSA) implies k <= j )
assume A2: j in SUCC (k,SCM+FSA) ; ::_thesis: k <= j
percases ( j = k or j = succ k ) by A1, A2, TARSKI:def_2;
suppose j = k ; ::_thesis: k <= j
hence k <= j ; ::_thesis: verum
end;
suppose j = succ k ; ::_thesis: k <= j
hence k <= j by NAT_1:11; ::_thesis: verum
end;
end;
end;
registration
cluster SCM+FSA -> standard ;
coherence
SCM+FSA is standard by Th40, AMISTD_1:3;
end;
registration
cluster(halt SCM+FSA) `1_3 -> jump-only for InsType of the InstructionsF of SCM+FSA;
coherence
for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (halt SCM+FSA) holds
b1 is jump-only
proof
now__::_thesis:_for_s_being_State_of_SCM+FSA
for_o_being_Object_of_SCM+FSA
for_I_being_Instruction_of_SCM+FSA_st_InsCode_I_=_InsCode_(halt_SCM+FSA)_&_o_in_Data-Locations_holds_
(Exec_(I,s))_._o_=_s_._o
let s be State of SCM+FSA; ::_thesis: for o being Object of SCM+FSA
for I being Instruction of SCM+FSA st InsCode I = InsCode (halt SCM+FSA) & o in Data-Locations holds
(Exec (I,s)) . o = s . o
let o be Object of SCM+FSA; ::_thesis: for I being Instruction of SCM+FSA st InsCode I = InsCode (halt SCM+FSA) & o in Data-Locations holds
(Exec (I,s)) . o = s . o
let I be Instruction of SCM+FSA; ::_thesis: ( InsCode I = InsCode (halt SCM+FSA) & o in Data-Locations implies (Exec (I,s)) . o = s . o )
assume that
A1: InsCode I = InsCode (halt SCM+FSA) and
o in Data-Locations ; ::_thesis: (Exec (I,s)) . o = s . o
I = halt SCM+FSA by A1, SCMFSA_2:95, COMPOS_1:70;
hence (Exec (I,s)) . o = s . o by EXTPRO_1:def_3; ::_thesis: verum
end;
hence for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (halt SCM+FSA) holds
b1 is jump-only by AMISTD_1:def_1; ::_thesis: verum
end;
end;
registration
cluster halt SCM+FSA -> jump-only ;
coherence
halt SCM+FSA is jump-only
proof
thus InsCode (halt SCM+FSA) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum
end;
end;
registration
let i1 be Element of NAT ;
cluster(goto i1) `1_3 -> jump-only for InsType of the InstructionsF of SCM+FSA;
coherence
for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (goto i1) holds
b1 is jump-only
proof
set S = SCM+FSA ;
now__::_thesis:_for_s_being_State_of_SCM+FSA
for_o_being_Object_of_SCM+FSA
for_I_being_Instruction_of_SCM+FSA_st_InsCode_I_=_InsCode_(goto_i1)_&_o_in_Data-Locations_holds_
(Exec_(I,s))_._o_=_s_._o
let s be State of SCM+FSA; ::_thesis: for o being Object of SCM+FSA
for I being Instruction of SCM+FSA st InsCode I = InsCode (goto i1) & o in Data-Locations holds
(Exec (b5,b3)) . b4 = b3 . b4
let o be Object of SCM+FSA; ::_thesis: for I being Instruction of SCM+FSA st InsCode I = InsCode (goto i1) & o in Data-Locations holds
(Exec (b4,b2)) . b3 = b2 . b3
let I be Instruction of SCM+FSA; ::_thesis: ( InsCode I = InsCode (goto i1) & o in Data-Locations implies (Exec (b3,b1)) . b2 = b1 . b2 )
assume that
A1: InsCode I = InsCode (goto i1) and
A2: o in Data-Locations ; ::_thesis: (Exec (b3,b1)) . b2 = b1 . b2
A3: ex i2 being Element of NAT st I = goto i2 by A1, SCMFSA_2:23, SCMFSA_2:35;
percases ( o is Int-Location or o is FinSeq-Location ) by A2, Th1;
suppose o is Int-Location ; ::_thesis: (Exec (b3,b1)) . b2 = b1 . b2
hence (Exec (I,s)) . o = s . o by A3, SCMFSA_2:69; ::_thesis: verum
end;
suppose o is FinSeq-Location ; ::_thesis: (Exec (b3,b1)) . b2 = b1 . b2
hence (Exec (I,s)) . o = s . o by A3, SCMFSA_2:69; ::_thesis: verum
end;
end;
end;
hence for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (goto i1) holds
b1 is jump-only by AMISTD_1:def_1; ::_thesis: verum
end;
end;
registration
let i1 be Element of NAT ;
cluster goto i1 -> non ins-loc-free jump-only non sequential ;
coherence
( goto i1 is jump-only & not goto i1 is sequential & not goto i1 is ins-loc-free )
proof
thus InsCode (goto i1) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: ( not goto i1 is sequential & not goto i1 is ins-loc-free )
JUMP (goto i1) <> {} ;
hence not goto i1 is sequential by AMISTD_1:13; ::_thesis: not goto i1 is ins-loc-free
dom (JumpPart (goto i1)) = dom <*i1*> by RECDEF_2:def_2
.= {1} by FINSEQ_1:2, FINSEQ_1:def_8 ;
hence not JumpPart (goto i1) is empty ; :: according to COMPOS_0:def_8 ::_thesis: verum
end;
end;
registration
let a be Int-Location;
let i1 be Element of NAT ;
cluster(a =0_goto i1) `1_3 -> jump-only for InsType of the InstructionsF of SCM+FSA;
coherence
for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (a =0_goto i1) holds
b1 is jump-only
proof
set S = SCM+FSA ;
now__::_thesis:_for_s_being_State_of_SCM+FSA
for_o_being_Object_of_SCM+FSA
for_I_being_Instruction_of_SCM+FSA_st_InsCode_I_=_InsCode_(a_=0_goto_i1)_&_o_in_Data-Locations_holds_
(Exec_(I,s))_._o_=_s_._o
let s be State of SCM+FSA; ::_thesis: for o being Object of SCM+FSA
for I being Instruction of SCM+FSA st InsCode I = InsCode (a =0_goto i1) & o in Data-Locations holds
(Exec (b5,b3)) . b4 = b3 . b4
let o be Object of SCM+FSA; ::_thesis: for I being Instruction of SCM+FSA st InsCode I = InsCode (a =0_goto i1) & o in Data-Locations holds
(Exec (b4,b2)) . b3 = b2 . b3
let I be Instruction of SCM+FSA; ::_thesis: ( InsCode I = InsCode (a =0_goto i1) & o in Data-Locations implies (Exec (b3,b1)) . b2 = b1 . b2 )
assume that
A1: InsCode I = InsCode (a =0_goto i1) and
A2: o in Data-Locations ; ::_thesis: (Exec (b3,b1)) . b2 = b1 . b2
A3: ex i2 being Element of NAT ex b being Int-Location st I = b =0_goto i2 by A1, SCMFSA_2:24, SCMFSA_2:36;
percases ( o is Int-Location or o is FinSeq-Location ) by A2, Th1;
suppose o is Int-Location ; ::_thesis: (Exec (b3,b1)) . b2 = b1 . b2
hence (Exec (I,s)) . o = s . o by A3, SCMFSA_2:70; ::_thesis: verum
end;
suppose o is FinSeq-Location ; ::_thesis: (Exec (b3,b1)) . b2 = b1 . b2
hence (Exec (I,s)) . o = s . o by A3, SCMFSA_2:70; ::_thesis: verum
end;
end;
end;
hence for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (a =0_goto i1) holds
b1 is jump-only by AMISTD_1:def_1; ::_thesis: verum
end;
cluster(a >0_goto i1) `1_3 -> jump-only for InsType of the InstructionsF of SCM+FSA;
coherence
for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (a >0_goto i1) holds
b1 is jump-only
proof
set S = SCM+FSA ;
now__::_thesis:_for_s_being_State_of_SCM+FSA
for_o_being_Object_of_SCM+FSA
for_I_being_Instruction_of_SCM+FSA_st_InsCode_I_=_InsCode_(a_>0_goto_i1)_&_o_in_Data-Locations_holds_
(Exec_(I,s))_._o_=_s_._o
let s be State of SCM+FSA; ::_thesis: for o being Object of SCM+FSA
for I being Instruction of SCM+FSA st InsCode I = InsCode (a >0_goto i1) & o in Data-Locations holds
(Exec (b5,b3)) . b4 = b3 . b4
let o be Object of SCM+FSA; ::_thesis: for I being Instruction of SCM+FSA st InsCode I = InsCode (a >0_goto i1) & o in Data-Locations holds
(Exec (b4,b2)) . b3 = b2 . b3
let I be Instruction of SCM+FSA; ::_thesis: ( InsCode I = InsCode (a >0_goto i1) & o in Data-Locations implies (Exec (b3,b1)) . b2 = b1 . b2 )
assume that
A4: InsCode I = InsCode (a >0_goto i1) and
A5: o in Data-Locations ; ::_thesis: (Exec (b3,b1)) . b2 = b1 . b2
A6: ex i2 being Element of NAT ex b being Int-Location st I = b >0_goto i2 by A4, SCMFSA_2:25, SCMFSA_2:37;
percases ( o is Int-Location or o is FinSeq-Location ) by A5, Th1;
suppose o is Int-Location ; ::_thesis: (Exec (b3,b1)) . b2 = b1 . b2
hence (Exec (I,s)) . o = s . o by A6, SCMFSA_2:71; ::_thesis: verum
end;
suppose o is FinSeq-Location ; ::_thesis: (Exec (b3,b1)) . b2 = b1 . b2
hence (Exec (I,s)) . o = s . o by A6, SCMFSA_2:71; ::_thesis: verum
end;
end;
end;
hence for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (a >0_goto i1) holds
b1 is jump-only by AMISTD_1:def_1; ::_thesis: verum
end;
end;
registration
let a be Int-Location;
let i1 be Element of NAT ;
clustera =0_goto i1 -> non ins-loc-free jump-only non sequential ;
coherence
( a =0_goto i1 is jump-only & not a =0_goto i1 is sequential & not a =0_goto i1 is ins-loc-free )
proof
thus InsCode (a =0_goto i1) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: ( not a =0_goto i1 is sequential & not a =0_goto i1 is ins-loc-free )
JUMP (a =0_goto i1) <> {} ;
hence not a =0_goto i1 is sequential by AMISTD_1:13; ::_thesis: not a =0_goto i1 is ins-loc-free
dom (JumpPart (a =0_goto i1)) = dom <*i1*> by Th15
.= {1} by FINSEQ_1:2, FINSEQ_1:38 ;
hence not JumpPart (a =0_goto i1) is empty ; :: according to COMPOS_0:def_8 ::_thesis: verum
end;
clustera >0_goto i1 -> non ins-loc-free jump-only non sequential ;
coherence
( a >0_goto i1 is jump-only & not a >0_goto i1 is sequential & not a >0_goto i1 is ins-loc-free )
proof
thus InsCode (a >0_goto i1) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: ( not a >0_goto i1 is sequential & not a >0_goto i1 is ins-loc-free )
JUMP (a >0_goto i1) <> {} ;
hence not a >0_goto i1 is sequential by AMISTD_1:13; ::_thesis: not a >0_goto i1 is ins-loc-free
dom (JumpPart (a >0_goto i1)) = dom <*i1*> by Th16
.= {1} by FINSEQ_1:2, FINSEQ_1:38 ;
hence not JumpPart (a >0_goto i1) is empty ; :: according to COMPOS_0:def_8 ::_thesis: verum
end;
end;
Lm2: intloc 0 <> intloc 1
by AMI_3:10;
registration
let a, b be Int-Location;
cluster(a := b) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;
coherence
for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (a := b) holds
not b1 is jump-only
proof
set w = the State of SCM+FSA;
set t = the State of SCM+FSA +* (((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: ( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (0,1))) . (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 by SCMFSA_2:100, XBOOLE_0:def_3;
(Exec (((intloc 0) := (intloc 1)),( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (0,1))))) . (intloc 0) = ( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (0,1))) . (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 for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (a := b) holds
not b1 is jump-only by A1, A4, A5, AMISTD_1:def_1; ::_thesis: verum
end;
cluster(AddTo (a,b)) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;
coherence
for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (AddTo (a,b)) holds
not b1 is jump-only
proof
set w = the State of SCM+FSA;
set t = the State of SCM+FSA +* (((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: ( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (0,1))) . (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 by SCMFSA_2:100, XBOOLE_0:def_3;
intloc 1 in dom (((intloc 0),(intloc 1)) --> (0,1)) by A7, TARSKI:def_2;
then ( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (0,1))) . (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))),( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (0,1))))) . (intloc 0) = 0 + 1 by A8, SCMFSA_2:64;
hence for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (AddTo (a,b)) holds
not b1 is jump-only by A6, A8, A9, AMISTD_1:def_1; ::_thesis: verum
end;
cluster(SubFrom (a,b)) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;
coherence
for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (SubFrom (a,b)) holds
not b1 is jump-only
proof
set w = the State of SCM+FSA;
set t = the State of SCM+FSA +* (((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: ( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (0,1))) . (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 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: ( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (0,1))) . (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))),( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (0,1))))) . (intloc 0) = (( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (0,1))) . (intloc 0)) - (( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (0,1))) . (intloc 1)) by SCMFSA_2:65
.= - 1 by A12, A14 ;
hence for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (SubFrom (a,b)) holds
not b1 is jump-only by A10, A12, A13, AMISTD_1:def_1; ::_thesis: verum
end;
cluster(MultBy (a,b)) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;
coherence
for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (MultBy (a,b)) holds
not b1 is jump-only
proof
set w = the State of SCM+FSA;
set t = the State of SCM+FSA +* (((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: ( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (1,0))) . (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 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: ( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (1,0))) . (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))),( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (1,0))))) . (intloc 0) = (( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (1,0))) . (intloc 0)) * (( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (1,0))) . (intloc 1)) by SCMFSA_2:66
.= 0 by A19 ;
hence for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (MultBy (a,b)) holds
not b1 is jump-only by A15, A17, A18, AMISTD_1:def_1; ::_thesis: verum
end;
cluster(Divide (a,b)) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;
coherence
for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (Divide (a,b)) holds
not b1 is jump-only
proof
set w = the State of SCM+FSA;
set t = the State of SCM+FSA +* (((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: ( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (7,3))) . (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 by SCMFSA_2:100, XBOOLE_0:def_3;
intloc 1 in dom (((intloc 0),(intloc 1)) --> (7,3)) by A21, TARSKI:def_2;
then ( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (7,3))) . (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))),( the State of SCM+FSA +* (((intloc 0),(intloc 1)) --> (7,3))))) . (intloc 0) = 7 div 3 by A22, Lm2, SCMFSA_2:67
.= 2 by A23, NAT_D:def_1 ;
hence for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (Divide (a,b)) holds
not b1 is jump-only by A20, A22, A24, AMISTD_1:def_1; ::_thesis: verum
end;
end;
Lm3: fsloc 0 <> intloc 0
by SCMFSA_2:99;
Lm4: fsloc 0 <> intloc 1
by SCMFSA_2:99;
registration
let a, b be Int-Location;
let f be FinSeq-Location ;
cluster(b := (f,a)) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;
coherence
for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (b := (f,a)) holds
not b1 is jump-only
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 = (( the State of SCM+FSA +* ((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, FINSEQ_1:def_8;
then A3: 1 in dom (t . (fsloc 0)) by TARSKI:def_1;
consider k being Element of NAT such that
A4: k = abs (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 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 by SCMFSA_2:26
.= InsCode ((intloc 0) := ((fsloc 0),(intloc 1))) by SCMFSA_2:26 ;
hence for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (b := (f,a)) holds
not b1 is jump-only by A1, A7, A6, AMISTD_1:def_1; ::_thesis: verum
end;
cluster((f,a) := b) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;
coherence
for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode ((f,a) := b) holds
not b1 is jump-only
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 by SCMFSA_2:27
.= InsCode (((fsloc 0),(intloc 1)) := (intloc 0)) by SCMFSA_2:27 ;
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 = (( the State of SCM+FSA +* ((fsloc 0) .--> F)) +* ((intloc 0) .--> D)) +* ((intloc 1) .--> E) as State of SCM+FSA ;
consider k being Element of NAT such that
A9: k = abs (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 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 for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode ((f,a) := b) holds
not b1 is jump-only by A8, A14, A13, A12, AMISTD_1:def_1; ::_thesis: verum
end;
end;
registration
let a, b be Int-Location;
let f be FinSeq-Location ;
clusterb := (f,a) -> non jump-only ;
coherence
not b := (f,a) is jump-only
proof
thus not InsCode (b := (f,a)) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum
end;
cluster(f,a) := b -> non jump-only ;
coherence
not (f,a) := b is jump-only
proof
thus not InsCode ((f,a) := b) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum
end;
end;
registration
let a be Int-Location;
let f be FinSeq-Location ;
cluster(a :=len f) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;
coherence
for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (a :=len f) holds
not b1 is jump-only
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 by SCMFSA_2:28
.= InsCode ((intloc 0) :=len (fsloc 0)) by SCMFSA_2:28 ;
<*DWA*> in INT * by FINSEQ_1:def_11;
then reconsider F = <*2*> as Element of Values (fsloc 0) by SCMFSA_2:12;
reconsider t = ( the State of SCM+FSA +* ((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 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 for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (a :=len f) holds
not b1 is jump-only by A1, A4, A3, AMISTD_1:def_1; ::_thesis: verum
end;
cluster(f :=<0,...,0> a) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;
coherence
for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (f :=<0,...,0> a) holds
not b1 is jump-only
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 = ( the State of SCM+FSA +* ((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 Element of NAT such that
A7: k = abs (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 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 by SCMFSA_2:29
.= InsCode ((fsloc 0) :=<0,...,0> (intloc 0)) by SCMFSA_2:29 ;
hence for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (f :=<0,...,0> a) holds
not b1 is jump-only by A5, A6, A10, A9, AMISTD_1:def_1; ::_thesis: verum
end;
end;
registration
let a be Int-Location;
let f be FinSeq-Location ;
clustera :=len f -> non jump-only ;
coherence
not a :=len f is jump-only
proof
thus not InsCode (a :=len f) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum
end;
clusterf :=<0,...,0> a -> non jump-only ;
coherence
not f :=<0,...,0> a is jump-only
proof
thus not InsCode (f :=<0,...,0> a) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum
end;
end;
registration
cluster SCM+FSA -> with_explicit_jumps ;
coherence
SCM+FSA is with_explicit_jumps
proof
let I be Instruction of SCM+FSA; :: according to AMISTD_2:def_2 ::_thesis: I is with_explicit_jumps
thus JUMP I c= rng (JumpPart I) :: according to AMISTD_2:def_1,XBOOLE_0:def_10 ::_thesis: proj2 (I `2_3) c= JUMP I
proof
let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in JUMP I or f in rng (JumpPart I) )
assume A1: f in JUMP I ; ::_thesis: f in rng (JumpPart I)
percases ( I = [0,{},{}] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo (a,b) or ex a, b being Int-Location st I = SubFrom (a,b) or ex a, b being Int-Location st I = MultBy (a,b) or ex a, b being Int-Location st I = Divide (a,b) or ex i1 being Element of NAT st I = goto i1 or ex i1 being Element of NAT ex a being Int-Location st I = a =0_goto i1 or ex i1 being Element of NAT ex a being Int-Location st I = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st I = b := (f,a) or ex a, b being Int-Location ex f being FinSeq-Location st I = (f,a) := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) by SCMFSA_2:93;
suppose I = [0,{},{}] ; ::_thesis: f in rng (JumpPart I)
hence f in rng (JumpPart I) by A1, SCMFSA_2:96; ::_thesis: verum
end;
suppose ex a, b being Int-Location st I = a := b ; ::_thesis: f in rng (JumpPart I)
hence f in rng (JumpPart I) by A1; ::_thesis: verum
end;
suppose ex a, b being Int-Location st I = AddTo (a,b) ; ::_thesis: f in rng (JumpPart I)
hence f in rng (JumpPart I) by A1; ::_thesis: verum
end;
suppose ex a, b being Int-Location st I = SubFrom (a,b) ; ::_thesis: f in rng (JumpPart I)
hence f in rng (JumpPart I) by A1; ::_thesis: verum
end;
suppose ex a, b being Int-Location st I = MultBy (a,b) ; ::_thesis: f in rng (JumpPart I)
hence f in rng (JumpPart I) by A1; ::_thesis: verum
end;
suppose ex a, b being Int-Location st I = Divide (a,b) ; ::_thesis: f in rng (JumpPart I)
hence f in rng (JumpPart I) by A1; ::_thesis: verum
end;
supposeA2: ex i1 being Element of NAT st I = goto i1 ; ::_thesis: f in rng (JumpPart I)
consider i1 being Element of NAT such that
A3: I = goto i1 by A2;
A4: JumpPart (goto i1) = <*i1*> by RECDEF_2:def_2;
rng <*i1*> = {i1} by FINSEQ_1:39;
hence f in rng (JumpPart I) by A1, A3, A4, Th34; ::_thesis: verum
end;
supposeA5: ex i1 being Element of NAT ex a being Int-Location st I = a =0_goto i1 ; ::_thesis: f in rng (JumpPart I)
consider a being Int-Location, i1 being Element of NAT such that
A6: I = a =0_goto i1 by A5;
A7: JumpPart (a =0_goto i1) = <*i1*> by Th15;
rng <*i1*> = {i1} by FINSEQ_1:39;
hence f in rng (JumpPart I) by A1, A6, A7, Th36; ::_thesis: verum
end;
supposeA8: ex i1 being Element of NAT ex a being Int-Location st I = a >0_goto i1 ; ::_thesis: f in rng (JumpPart I)
consider a being Int-Location, i1 being Element of NAT such that
A9: I = a >0_goto i1 by A8;
A10: JumpPart (a >0_goto i1) = <*i1*> by Th16;
rng <*i1*> = {i1} by FINSEQ_1:39;
hence f in rng (JumpPart I) by A1, A9, A10, Th38; ::_thesis: verum
end;
suppose ex a, b being Int-Location ex f being FinSeq-Location st I = b := (f,a) ; ::_thesis: f in rng (JumpPart I)
hence f in rng (JumpPart I) by A1; ::_thesis: verum
end;
suppose ex a, b being Int-Location ex f being FinSeq-Location st I = (f,a) := b ; ::_thesis: f in rng (JumpPart I)
hence f in rng (JumpPart I) by A1; ::_thesis: verum
end;
suppose ex a being Int-Location ex f being FinSeq-Location st I = a :=len f ; ::_thesis: f in rng (JumpPart I)
hence f in rng (JumpPart I) by A1; ::_thesis: verum
end;
suppose ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ; ::_thesis: f in rng (JumpPart I)
hence f in rng (JumpPart I) by A1; ::_thesis: verum
end;
end;
end;
let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in proj2 (I `2_3) or f in JUMP I )
assume f in rng (JumpPart I) ; ::_thesis: f in JUMP I
then consider k being set such that
A11: k in dom (JumpPart I) and
A12: f = (JumpPart I) . k by FUNCT_1:def_3;
percases ( I = [0,{},{}] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo (a,b) or ex a, b being Int-Location st I = SubFrom (a,b) or ex a, b being Int-Location st I = MultBy (a,b) or ex a, b being Int-Location st I = Divide (a,b) or ex i1 being Element of NAT st I = goto i1 or ex i1 being Element of NAT ex a being Int-Location st I = a =0_goto i1 or ex i1 being Element of NAT ex a being Int-Location st I = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st I = b := (f,a) or ex a, b being Int-Location ex f being FinSeq-Location st I = (f,a) := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) by SCMFSA_2:93;
suppose I = [0,{},{}] ; ::_thesis: f in JUMP I
then dom (JumpPart I) = dom {} by RECDEF_2:def_2;
hence f in JUMP I by A11; ::_thesis: verum
end;
suppose ex a, b being Int-Location st I = a := b ; ::_thesis: f in JUMP I
then consider a, b being Int-Location such that
A13: I = a := b ;
k in dom {} by A11, A13, Th10;
hence f in JUMP I ; ::_thesis: verum
end;
suppose ex a, b being Int-Location st I = AddTo (a,b) ; ::_thesis: f in JUMP I
then consider a, b being Int-Location such that
A14: I = AddTo (a,b) ;
k in dom {} by A11, A14, Th11;
hence f in JUMP I ; ::_thesis: verum
end;
suppose ex a, b being Int-Location st I = SubFrom (a,b) ; ::_thesis: f in JUMP I
then consider a, b being Int-Location such that
A15: I = SubFrom (a,b) ;
k in dom {} by A11, A15, Th12;
hence f in JUMP I ; ::_thesis: verum
end;
suppose ex a, b being Int-Location st I = MultBy (a,b) ; ::_thesis: f in JUMP I
then consider a, b being Int-Location such that
A16: I = MultBy (a,b) ;
k in dom {} by A11, A16, Th13;
hence f in JUMP I ; ::_thesis: verum
end;
suppose ex a, b being Int-Location st I = Divide (a,b) ; ::_thesis: f in JUMP I
then consider a, b being Int-Location such that
A17: I = Divide (a,b) ;
k in dom {} by A11, A17, Th14;
hence f in JUMP I ; ::_thesis: verum
end;
suppose ex i1 being Element of NAT st I = goto i1 ; ::_thesis: f in JUMP I
then consider i1 being Element of NAT such that
A18: I = goto i1 ;
A19: JumpPart I = <*i1*> by A18, RECDEF_2:def_2;
then k = 1 by A11, FINSEQ_1:90;
then A20: f = i1 by A19, A12, FINSEQ_1:def_8;
JUMP I = {i1} by A18, Th34;
hence f in JUMP I by A20, TARSKI:def_1; ::_thesis: verum
end;
suppose ex i1 being Element of NAT ex a being Int-Location st I = a =0_goto i1 ; ::_thesis: f in JUMP I
then consider a being Int-Location, i1 being Element of NAT such that
A21: I = a =0_goto i1 ;
A22: JumpPart I = <*i1*> by A21, Th15;
then k = 1 by A11, FINSEQ_1:90;
then A23: f = i1 by A22, A12, FINSEQ_1:def_8;
JUMP I = {i1} by A21, Th36;
hence f in JUMP I by A23, TARSKI:def_1; ::_thesis: verum
end;
suppose ex i1 being Element of NAT ex a being Int-Location st I = a >0_goto i1 ; ::_thesis: f in JUMP I
then consider a being Int-Location, i1 being Element of NAT such that
A24: I = a >0_goto i1 ;
A25: JumpPart I = <*i1*> by A24, Th16;
then k = 1 by A11, FINSEQ_1:90;
then A26: f = i1 by A25, A12, FINSEQ_1:def_8;
JUMP I = {i1} by A24, Th38;
hence f in JUMP I by A26, TARSKI:def_1; ::_thesis: verum
end;
suppose ex a, b being Int-Location ex f being FinSeq-Location st I = b := (f,a) ; ::_thesis: f in JUMP I
then consider a, b being Int-Location, f being FinSeq-Location such that
A27: I = b := (f,a) ;
k in dom {} by A11, A27, RECDEF_2:def_2;
hence f in JUMP I ; ::_thesis: verum
end;
suppose ex a, b being Int-Location ex f being FinSeq-Location st I = (f,a) := b ; ::_thesis: f in JUMP I
then consider a, b being Int-Location, f being FinSeq-Location such that
A28: I = (f,a) := b ;
k in dom {} by A11, A28, RECDEF_2:def_2;
hence f in JUMP I ; ::_thesis: verum
end;
suppose ex a being Int-Location ex f being FinSeq-Location st I = a :=len f ; ::_thesis: f in JUMP I
then consider a being Int-Location, f being FinSeq-Location such that
A29: I = a :=len f ;
k in dom {} by A11, A29, RECDEF_2:def_2;
hence f in JUMP I ; ::_thesis: verum
end;
suppose ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ; ::_thesis: f in JUMP I
then consider a being Int-Location, f being FinSeq-Location such that
A30: I = f :=<0,...,0> a ;
k in dom {} by A11, A30, RECDEF_2:def_2;
hence f in JUMP I ; ::_thesis: verum
end;
end;
end;
end;
theorem Th41: :: SCMFSA10:41
for i1 being Element of NAT
for k being Nat holds IncAddr ((goto i1),k) = goto (i1 + k)
proof
let i1 be Element of NAT ; ::_thesis: for k being Nat holds IncAddr ((goto i1),k) = goto (i1 + k)
let k be Nat; ::_thesis: IncAddr ((goto i1),k) = goto (i1 + k)
A1: InsCode (IncAddr ((goto i1),k)) = InsCode (goto i1) by COMPOS_0:def_9
.= 6 by SCMFSA_2:23
.= InsCode (goto (i1 + k)) by SCMFSA_2:23 ;
A2: AddressPart (IncAddr ((goto i1),k)) = AddressPart (goto i1) by COMPOS_0:def_9
.= {} by RECDEF_2:def_3
.= AddressPart (goto (i1 + k)) by RECDEF_2:def_3 ;
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 set st x in dom (JumpPart (goto i1)) holds
(JumpPart (IncAddr ((goto i1),k))) . x = (JumpPart (goto (i1 + k))) . x
proof
let x be set ; ::_thesis: ( x in dom (JumpPart (goto i1)) implies (JumpPart (IncAddr ((goto i1),k))) . x = (JumpPart (goto (i1 + k))) . x )
assume A6: x in dom (JumpPart (goto i1)) ; ::_thesis: (JumpPart (IncAddr ((goto i1),k))) . x = (JumpPart (goto (i1 + k))) . x
then x in dom <*i1*> by RECDEF_2:def_2;
then A7: x = 1 by FINSEQ_1:90;
set f = (JumpPart (goto i1)) . x;
A8: (JumpPart (IncAddr ((goto i1),k))) . x = k + ((JumpPart (goto i1)) . x) by A4, A3, A6, VALUED_1:def_2;
(JumpPart (goto i1)) . x = <*i1*> . x by RECDEF_2:def_2
.= 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 by RECDEF_2:def_2 ;
::_thesis: verum
end;
dom (JumpPart (goto (i1 + k))) = dom <*(i1 + k)*> by RECDEF_2:def_2
.= Seg 1 by FINSEQ_1:def_8
.= dom <*i1*> by FINSEQ_1:def_8
.= dom (JumpPart (goto i1)) by RECDEF_2:def_2 ;
then JumpPart (IncAddr ((goto i1),k)) = JumpPart (goto (i1 + k)) by A4, A5, FUNCT_1:2;
hence IncAddr ((goto i1),k) = goto (i1 + k) by A1, A2, COMPOS_0:1; ::_thesis: verum
end;
theorem Th42: :: SCMFSA10:42
for i1 being Element of NAT
for k being Nat
for a being Int-Location holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)
proof
let i1 be Element of NAT ; ::_thesis: for k being Nat
for a being Int-Location holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)
let k be Nat; ::_thesis: for a being Int-Location holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)
let a be Int-Location; ::_thesis: IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)
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, RECDEF_2:def_3
.= AddressPart (a =0_goto (i1 + k)) by A3, RECDEF_2:def_3 ;
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 set 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 set ; ::_thesis: ( x in dom (JumpPart (a =0_goto i1)) implies (JumpPart (IncAddr ((a =0_goto i1),k))) . x = (JumpPart (a =0_goto (i1 + k))) . x )
assume A8: x in dom (JumpPart (a =0_goto i1)) ; ::_thesis: (JumpPart (IncAddr ((a =0_goto i1),k))) . x = (JumpPart (a =0_goto (i1 + k))) . x
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 + ((JumpPart (a =0_goto i1)) . x) by A6, A5, A8, VALUED_1:def_2;
(JumpPart (a =0_goto i1)) . x = <*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 ;
::_thesis: verum
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 IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k) by A1, A4, COMPOS_0:1; ::_thesis: verum
end;
theorem Th43: :: SCMFSA10:43
for i1 being Element of NAT
for k being Nat
for a being Int-Location holds IncAddr ((a >0_goto i1),k) = a >0_goto (i1 + k)
proof
let i1 be Element of NAT ; ::_thesis: for k being Nat
for a being Int-Location holds IncAddr ((a >0_goto i1),k) = a >0_goto (i1 + k)
let k be Nat; ::_thesis: for a being Int-Location holds IncAddr ((a >0_goto i1),k) = a >0_goto (i1 + k)
let a be Int-Location; ::_thesis: IncAddr ((a >0_goto i1),k) = a >0_goto (i1 + k)
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, RECDEF_2:def_3
.= AddressPart (a >0_goto (i1 + k)) by A3, RECDEF_2:def_3 ;
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 set 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 set ; ::_thesis: ( x in dom (JumpPart (a >0_goto i1)) implies (JumpPart (IncAddr ((a >0_goto i1),k))) . x = (JumpPart (a >0_goto (i1 + k))) . x )
assume A8: x in dom (JumpPart (a >0_goto i1)) ; ::_thesis: (JumpPart (IncAddr ((a >0_goto i1),k))) . x = (JumpPart (a >0_goto (i1 + k))) . x
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 + ((JumpPart (a >0_goto i1)) . 1) by A9, A6, A5, A8, VALUED_1:def_2;
(JumpPart (a >0_goto i1)) . 1 = <*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 ;
::_thesis: verum
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 IncAddr ((a >0_goto i1),k) = a >0_goto (i1 + k) by A1, A4, COMPOS_0:1; ::_thesis: verum
end;
registration
cluster SCM+FSA -> IC-relocable ;
coherence
SCM+FSA is IC-relocable
proof
let I be Instruction of SCM+FSA; :: according to AMISTD_2:def_4 ::_thesis: I is IC-relocable
percases ( I = [0,{},{}] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo (a,b) or ex a, b being Int-Location st I = SubFrom (a,b) or ex a, b being Int-Location st I = MultBy (a,b) or ex a, b being Int-Location st I = Divide (a,b) or ex i1 being Element of NAT st I = goto i1 or ex i1 being Element of NAT ex a being Int-Location st I = a =0_goto i1 or ex i1 being Element of NAT ex a being Int-Location st I = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st I = b := (f,a) or ex a, b being Int-Location ex f being FinSeq-Location st I = (f,a) := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) by SCMFSA_2:93;
suppose I = [0,{},{}] ; ::_thesis: I is IC-relocable
hence I is IC-relocable by SCMFSA_2:96; ::_thesis: verum
end;
suppose ex a, b being Int-Location st I = a := b ; ::_thesis: I is IC-relocable
hence I is IC-relocable ; ::_thesis: verum
end;
suppose ex a, b being Int-Location st I = AddTo (a,b) ; ::_thesis: I is IC-relocable
hence I is IC-relocable ; ::_thesis: verum
end;
suppose ex a, b being Int-Location st I = SubFrom (a,b) ; ::_thesis: I is IC-relocable
hence I is IC-relocable ; ::_thesis: verum
end;
suppose ex a, b being Int-Location st I = MultBy (a,b) ; ::_thesis: I is IC-relocable
hence I is IC-relocable ; ::_thesis: verum
end;
suppose ex a, b being Int-Location st I = Divide (a,b) ; ::_thesis: I is IC-relocable
hence I is IC-relocable ; ::_thesis: verum
end;
supposeA1: ex i1 being Element of NAT st I = goto i1 ; ::_thesis: I is IC-relocable
let j, k be Nat; :: according to AMISTD_2:def_3 ::_thesis: for b1 being set holds (IC (Exec ((IncAddr (I,j)),b1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b1,k))))
let s1 be State of SCM+FSA; ::_thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
set s2 = IncIC (s1,k);
consider i1 being Element of NAT 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)),(IncIC (s1,k)))) by SCMFSA_2:69
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A2, Th41 ; ::_thesis: verum
end;
suppose ex i1 being Element of NAT ex a being Int-Location st I = a =0_goto i1 ; ::_thesis: I is IC-relocable
then consider a being Int-Location, i1 being Element of NAT such that
A3: I = a =0_goto i1 ;
let j, k be Nat; :: according to AMISTD_2:def_3 ::_thesis: for b1 being set holds (IC (Exec ((IncAddr (I,j)),b1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b1,k))))
let s1 be State of SCM+FSA; ::_thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
set s2 = IncIC (s1,k);
( a <> IC & dom ((IC ) .--> ((IC s1) + k)) = {(IC )} ) by FUNCOP_1:13, SCMFSA_2:56;
then not a in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def_1;
then A4: s1 . a = (IncIC (s1,k)) . a by FUNCT_4:11;
percases ( s1 . a = 0 or s1 . a <> 0 ) ;
supposeA5: s1 . a = 0 ; ::_thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
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)),(IncIC (s1,k)))) by A4, A5, SCMFSA_2:70
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A3, Th42 ; ::_thesis: verum
end;
supposeA6: s1 . a <> 0 ; ::_thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
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;
dom ((IC ) .--> ((IC s1) + k)) = {(IC )} by FUNCOP_1:13;
then IC in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def_1;
then A9: IC (IncIC (s1,k)) = ((IC ) .--> ((IC s1) + k)) . (IC ) by FUNCT_4:13
.= (IC s1) + k by FUNCOP_1:72 ;
thus (IC (Exec ((IncAddr (I,j)),s1))) + k = (succ (IC s1)) + k by A7, A6, SCMFSA_2:70
.= succ (IC (IncIC (s1,k))) by A9
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A8, A6, A4, SCMFSA_2:70 ; ::_thesis: verum
end;
end;
end;
suppose ex i1 being Element of NAT ex a being Int-Location st I = a >0_goto i1 ; ::_thesis: I is IC-relocable
then consider i1 being Element of NAT , a being Int-Location such that
A10: I = a >0_goto i1 ;
let j, k be Nat; :: according to AMISTD_2:def_3 ::_thesis: for b1 being set holds (IC (Exec ((IncAddr (I,j)),b1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b1,k))))
let s1 be State of SCM+FSA; ::_thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
set s2 = IncIC (s1,k);
( a <> IC & dom ((IC ) .--> ((IC s1) + k)) = {(IC )} ) by FUNCOP_1:13, SCMFSA_2:56;
then not a in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def_1;
then A11: s1 . a = (IncIC (s1,k)) . a by FUNCT_4:11;
percases ( s1 . a > 0 or s1 . a <= 0 ) ;
supposeA12: s1 . a > 0 ; ::_thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
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)),(IncIC (s1,k)))) by A11, A12, SCMFSA_2:71
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A10, Th43 ; ::_thesis: verum
end;
supposeA13: s1 . a <= 0 ; ::_thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
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;
dom ((IC ) .--> ((IC s1) + k)) = {(IC )} by FUNCOP_1:13;
then IC in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def_1;
then A16: IC (IncIC (s1,k)) = ((IC ) .--> ((IC s1) + k)) . (IC ) by FUNCT_4:13
.= (IC s1) + k by FUNCOP_1:72 ;
thus (IC (Exec ((IncAddr (I,j)),s1))) + k = (succ (IC s1)) + k by A14, A13, SCMFSA_2:71
.= succ (IC (IncIC (s1,k))) by A16
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A15, A13, A11, SCMFSA_2:71 ; ::_thesis: verum
end;
end;
end;
suppose ex a, b being Int-Location ex f being FinSeq-Location st I = b := (f,a) ; ::_thesis: I is IC-relocable
hence I is IC-relocable ; ::_thesis: verum
end;
suppose ex a, b being Int-Location ex f being FinSeq-Location st I = (f,a) := b ; ::_thesis: I is IC-relocable
hence I is IC-relocable ; ::_thesis: verum
end;
suppose ex a being Int-Location ex f being FinSeq-Location st I = a :=len f ; ::_thesis: I is IC-relocable
hence I is IC-relocable ; ::_thesis: verum
end;
suppose ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ; ::_thesis: I is IC-relocable
hence I is IC-relocable ; ::_thesis: verum
end;
end;
end;
end;