:: SCMRING3 semantic presentation
begin
theorem Th1: :: SCMRING3:1
for R being Ring
for a being Data-Location of R holds Values a = the carrier of R
proof
let R be Ring; ::_thesis: for a being Data-Location of R holds Values a = the carrier of R
let a be Data-Location of R; ::_thesis: Values a = the carrier of R
( a in Data-Locations & the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK ) by SCMRING2:1, SCMRING2:24;
hence Values a = the carrier of R by AMI_3:27, SCMRING1:4; ::_thesis: verum
end;
definition
let R be Ring;
let la, lb be Data-Location of R;
let a, b be Element of R;
:: original: -->
redefine func(la,lb) --> (a,b) -> FinPartState of (SCM R);
coherence
(la,lb) --> (a,b) is FinPartState of (SCM R)
proof
reconsider b9 = b as Element of Values lb by Th1;
reconsider a9 = a as Element of Values la by Th1;
(la,lb) --> (a9,b9) is FinPartState of (SCM R) ;
hence (la,lb) --> (a,b) is FinPartState of (SCM R) ; ::_thesis: verum
end;
end;
theorem Th2: :: SCMRING3:2
for R being Ring
for a being Data-Location of R holds a <> IC
proof
let R be Ring; ::_thesis: for a being Data-Location of R holds a <> IC
let a be Data-Location of R; ::_thesis: a <> IC
a in SCM-Data-Loc by AMI_2:def_16;
then a <> NAT by AMI_2:20;
hence a <> IC by SCMRING2:8; ::_thesis: verum
end;
theorem :: SCMRING3:3
for R being Ring
for o being Object of (SCM R) holds
( o = IC or o is Data-Location of R )
proof
let R be Ring; ::_thesis: for o being Object of (SCM R) holds
( o = IC or o is Data-Location of R )
let o be Object of (SCM R); ::_thesis: ( o = IC or o is Data-Location of R )
assume o <> IC ; ::_thesis: o is Data-Location of R
then not o in {(IC )} by TARSKI:def_1;
then A1: not o in {NAT} by SCMRING2:8;
not o in {NAT} by A1;
then o in the carrier of (SCM R) \ {NAT} by XBOOLE_0:def_5;
then o in SCM-Data-Loc by SCMRING2:25;
hence o is Data-Location of R by AMI_2:def_16; ::_thesis: verum
end;
theorem :: SCMRING3:4
canceled;
theorem :: SCMRING3:5
for R being Ring
for a, b being Data-Location of R holds InsCode (a := b) = 1 by RECDEF_2:def_1;
theorem :: SCMRING3:6
for R being Ring
for a, b being Data-Location of R holds InsCode (AddTo (a,b)) = 2 by RECDEF_2:def_1;
theorem :: SCMRING3:7
for R being Ring
for a, b being Data-Location of R holds InsCode (SubFrom (a,b)) = 3 by RECDEF_2:def_1;
theorem :: SCMRING3:8
for R being Ring
for a, b being Data-Location of R holds InsCode (MultBy (a,b)) = 4 by RECDEF_2:def_1;
theorem :: SCMRING3:9
for R being Ring
for r being Element of R
for a being Data-Location of R holds InsCode (a := r) = 5 by RECDEF_2:def_1;
theorem Th10: :: SCMRING3:10
for R being Ring
for i1 being Element of NAT holds InsCode (goto (i1,R)) = 6 by RECDEF_2:def_1;
theorem Th11: :: SCMRING3:11
for R being Ring
for a being Data-Location of R
for i1 being Element of NAT holds InsCode (a =0_goto i1) = 7 by RECDEF_2:def_1;
theorem Th12: :: SCMRING3:12
for R being Ring
for I being Instruction of (SCM R) st InsCode I = 0 holds
I = halt (SCM R)
proof
let R be Ring; ::_thesis: for I being Instruction of (SCM R) st InsCode I = 0 holds
I = halt (SCM R)
let I be Instruction of (SCM R); ::_thesis: ( InsCode I = 0 implies I = halt (SCM R) )
A1: ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Element of NAT st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:7;
assume InsCode I = 0 ; ::_thesis: I = halt (SCM R)
hence I = halt (SCM R) by A1, RECDEF_2:def_1; ::_thesis: verum
end;
theorem Th13: :: SCMRING3:13
for R being Ring
for I being Instruction of (SCM R) st InsCode I = 1 holds
ex a, b being Data-Location of R st I = a := b
proof
let R be Ring; ::_thesis: for I being Instruction of (SCM R) st InsCode I = 1 holds
ex a, b being Data-Location of R st I = a := b
let I be Instruction of (SCM R); ::_thesis: ( InsCode I = 1 implies ex a, b being Data-Location of R st I = a := b )
A1: ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Element of NAT st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:7;
assume InsCode I = 1 ; ::_thesis: ex a, b being Data-Location of R st I = a := b
hence ex a, b being Data-Location of R st I = a := b by A1, RECDEF_2:def_1; ::_thesis: verum
end;
theorem Th14: :: SCMRING3:14
for R being Ring
for I being Instruction of (SCM R) st InsCode I = 2 holds
ex a, b being Data-Location of R st I = AddTo (a,b)
proof
let R be Ring; ::_thesis: for I being Instruction of (SCM R) st InsCode I = 2 holds
ex a, b being Data-Location of R st I = AddTo (a,b)
let I be Instruction of (SCM R); ::_thesis: ( InsCode I = 2 implies ex a, b being Data-Location of R st I = AddTo (a,b) )
A1: ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Element of NAT st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:7;
assume InsCode I = 2 ; ::_thesis: ex a, b being Data-Location of R st I = AddTo (a,b)
hence ex a, b being Data-Location of R st I = AddTo (a,b) by A1, RECDEF_2:def_1; ::_thesis: verum
end;
theorem Th15: :: SCMRING3:15
for R being Ring
for I being Instruction of (SCM R) st InsCode I = 3 holds
ex a, b being Data-Location of R st I = SubFrom (a,b)
proof
let R be Ring; ::_thesis: for I being Instruction of (SCM R) st InsCode I = 3 holds
ex a, b being Data-Location of R st I = SubFrom (a,b)
let I be Instruction of (SCM R); ::_thesis: ( InsCode I = 3 implies ex a, b being Data-Location of R st I = SubFrom (a,b) )
A1: ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Element of NAT st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:7;
assume InsCode I = 3 ; ::_thesis: ex a, b being Data-Location of R st I = SubFrom (a,b)
hence ex a, b being Data-Location of R st I = SubFrom (a,b) by A1, RECDEF_2:def_1; ::_thesis: verum
end;
theorem Th16: :: SCMRING3:16
for R being Ring
for I being Instruction of (SCM R) st InsCode I = 4 holds
ex a, b being Data-Location of R st I = MultBy (a,b)
proof
let R be Ring; ::_thesis: for I being Instruction of (SCM R) st InsCode I = 4 holds
ex a, b being Data-Location of R st I = MultBy (a,b)
let I be Instruction of (SCM R); ::_thesis: ( InsCode I = 4 implies ex a, b being Data-Location of R st I = MultBy (a,b) )
A1: ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Element of NAT st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:7;
assume InsCode I = 4 ; ::_thesis: ex a, b being Data-Location of R st I = MultBy (a,b)
hence ex a, b being Data-Location of R st I = MultBy (a,b) by A1, RECDEF_2:def_1; ::_thesis: verum
end;
theorem Th17: :: SCMRING3:17
for R being Ring
for I being Instruction of (SCM R) st InsCode I = 5 holds
ex a being Data-Location of R ex r being Element of R st I = a := r
proof
let R be Ring; ::_thesis: for I being Instruction of (SCM R) st InsCode I = 5 holds
ex a being Data-Location of R ex r being Element of R st I = a := r
let I be Instruction of (SCM R); ::_thesis: ( InsCode I = 5 implies ex a being Data-Location of R ex r being Element of R st I = a := r )
A1: ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Element of NAT st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:7;
assume InsCode I = 5 ; ::_thesis: ex a being Data-Location of R ex r being Element of R st I = a := r
hence ex a being Data-Location of R ex r being Element of R st I = a := r by A1, RECDEF_2:def_1; ::_thesis: verum
end;
theorem Th18: :: SCMRING3:18
for R being Ring
for I being Instruction of (SCM R) st InsCode I = 6 holds
ex i2 being Element of NAT st I = goto (i2,R)
proof
let R be Ring; ::_thesis: for I being Instruction of (SCM R) st InsCode I = 6 holds
ex i2 being Element of NAT st I = goto (i2,R)
let I be Instruction of (SCM R); ::_thesis: ( InsCode I = 6 implies ex i2 being Element of NAT st I = goto (i2,R) )
A1: ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Element of NAT st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:7;
assume InsCode I = 6 ; ::_thesis: ex i2 being Element of NAT st I = goto (i2,R)
hence ex i2 being Element of NAT st I = goto (i2,R) by A1, RECDEF_2:def_1; ::_thesis: verum
end;
theorem Th19: :: SCMRING3:19
for R being Ring
for I being Instruction of (SCM R) st InsCode I = 7 holds
ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1
proof
let R be Ring; ::_thesis: for I being Instruction of (SCM R) st InsCode I = 7 holds
ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1
let I be Instruction of (SCM R); ::_thesis: ( InsCode I = 7 implies ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 )
A1: ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Element of NAT st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:7;
assume InsCode I = 7 ; ::_thesis: ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1
hence ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 by A1, RECDEF_2:def_1; ::_thesis: verum
end;
Lm1: for x, y being set st x in dom <*y*> holds
x = 1
proof
let x, y be set ; ::_thesis: ( x in dom <*y*> implies x = 1 )
assume x in dom <*y*> ; ::_thesis: x = 1
then x in Seg 1 by FINSEQ_1:def_8;
hence x = 1 by FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum
end;
Lm2: for R being Ring
for T being InsType of the InstructionsF of (SCM R) holds
( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )
proof
let R be Ring; ::_thesis: for T being InsType of the InstructionsF of (SCM R) holds
( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )
let T be InsType of the InstructionsF of (SCM R); ::_thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )
consider y being set such that
A1: [T,y] in proj1 the InstructionsF of (SCM R) by XTUPLE_0:def_12;
consider x being set such that
A2: [[T,y],x] in the InstructionsF of (SCM R) by A1, XTUPLE_0:def_12;
[T,y,x] in SCM-Instr R by A2, SCMRING2:def_1;
then ( [T,y,x] in (({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of Data-Locations : verum } or [T,y,x] in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } ) by AMI_3:27, XBOOLE_0:def_3;
then ( [T,y,x] in ({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } or [T,y,x] in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of Data-Locations : verum } or [T,y,x] in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } ) by XBOOLE_0:def_3;
then A3: ( [T,y,x] in {[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : I in {1,2,3,4} } or [T,y,x] in { [6,<*i*>,{}] where i is Element of NAT : verum } or [T,y,x] in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of Data-Locations : verum } or [T,y,x] in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } ) by XBOOLE_0:def_3;
percases ( [T,y,x] in {[0,{},{}]} or [T,y,x] in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : I in {1,2,3,4} } or [T,y,x] in { [6,<*i*>,{}] where i is Element of NAT : verum } or [T,y,x] in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of Data-Locations : verum } or [T,y,x] in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } ) by A3, XBOOLE_0:def_3;
suppose [T,y,x] in {[0,{},{}]} ; ::_thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )
then [T,y,x] = [0,{},{}] by TARSKI:def_1;
hence ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 ) by XTUPLE_0:3; ::_thesis: verum
end;
suppose [T,y,x] in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : I in {1,2,3,4} } ; ::_thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )
then ex I being Element of Segm 8 ex a, b being Element of Data-Locations st
( [T,y,x] = [I,{},<*a,b*>] & I in {1,2,3,4} ) ;
then T in {1,2,3,4} by XTUPLE_0:3;
hence ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 ) by ENUMSET1:def_2; ::_thesis: verum
end;
suppose [T,y,x] in { [6,<*i*>,{}] where i is Element of NAT : verum } ; ::_thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )
then ex i being Element of NAT st [T,y,x] = [6,<*i*>,{}] ;
hence ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 ) by XTUPLE_0:3; ::_thesis: verum
end;
suppose [T,y,x] in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of Data-Locations : verum } ; ::_thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )
then ex i being Element of NAT ex a being Element of Data-Locations st [T,y,x] = [7,<*i*>,<*a*>] ;
hence ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 ) by XTUPLE_0:3; ::_thesis: verum
end;
suppose [T,y,x] in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } ; ::_thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )
then ex a being Element of Data-Locations ex r being Element of R st [T,y,x] = [5,{},<*a,r*>] ;
hence ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 ) by XTUPLE_0:3; ::_thesis: verum
end;
end;
end;
theorem :: SCMRING3:20
for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 0 holds
JumpParts T = {0}
proof
let R be Ring; ::_thesis: for T being InsType of the InstructionsF of (SCM R) st T = 0 holds
JumpParts T = {0}
let T be InsType of the InstructionsF of (SCM R); ::_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 R) such that
A2: a = JumpPart I and
A3: InsCode I = T ;
I = halt (SCM R) by A1, A3, Th12;
then a = {} by A2;
hence a in {0} by 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 R)) = 0 & JumpPart (halt (SCM R)) = 0 ) by COMPOS_1:70;
hence a in JumpParts T by A1, A4; ::_thesis: verum
end;
theorem :: SCMRING3:21
for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 1 holds
JumpParts T = {{}}
proof
let R be Ring; ::_thesis: for T being InsType of the InstructionsF of (SCM R) st T = 1 holds
JumpParts T = {{}}
let T be InsType of the InstructionsF of (SCM R); ::_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 R) such that
A2: x = JumpPart I and
A3: InsCode I = T ;
consider a, b being Data-Location of R such that
A4: I = a := b by A1, A3, Th13;
x = {} by A2, A4, RECDEF_2:def_2;
hence x in {{}} by TARSKI:def_1; ::_thesis: verum
end;
set a = the Data-Location of R;
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 Data-Location of R := the Data-Location of R) by RECDEF_2:def_2;
InsCode ( the Data-Location of R := the Data-Location of R) = 1 by RECDEF_2:def_1;
hence x in JumpParts T by A5, A1; ::_thesis: verum
end;
theorem :: SCMRING3:22
for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 2 holds
JumpParts T = {{}}
proof
let R be Ring; ::_thesis: for T being InsType of the InstructionsF of (SCM R) st T = 2 holds
JumpParts T = {{}}
let T be InsType of the InstructionsF of (SCM R); ::_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 R) such that
A2: x = JumpPart I and
A3: InsCode I = T ;
consider a, b being Data-Location of R such that
A4: I = AddTo (a,b) by A1, A3, Th14;
x = {} by A2, A4, RECDEF_2:def_2;
hence x in {{}} by TARSKI:def_1; ::_thesis: verum
end;
set a = the Data-Location of R;
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 Data-Location of R, the Data-Location of R)) by RECDEF_2:def_2;
InsCode (AddTo ( the Data-Location of R, the Data-Location of R)) = 2 by RECDEF_2:def_1;
hence x in JumpParts T by A5, A1; ::_thesis: verum
end;
theorem :: SCMRING3:23
for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 3 holds
JumpParts T = {{}}
proof
let R be Ring; ::_thesis: for T being InsType of the InstructionsF of (SCM R) st T = 3 holds
JumpParts T = {{}}
let T be InsType of the InstructionsF of (SCM R); ::_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 R) such that
A2: x = JumpPart I and
A3: InsCode I = T ;
consider a, b being Data-Location of R such that
A4: I = SubFrom (a,b) by A1, A3, Th15;
x = {} by A2, A4, RECDEF_2:def_2;
hence x in {{}} by TARSKI:def_1; ::_thesis: verum
end;
set a = the Data-Location of R;
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 Data-Location of R, the Data-Location of R)) by RECDEF_2:def_2;
InsCode (SubFrom ( the Data-Location of R, the Data-Location of R)) = 3 by RECDEF_2:def_1;
hence x in JumpParts T by A5, A1; ::_thesis: verum
end;
theorem :: SCMRING3:24
for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 4 holds
JumpParts T = {{}}
proof
let R be Ring; ::_thesis: for T being InsType of the InstructionsF of (SCM R) st T = 4 holds
JumpParts T = {{}}
let T be InsType of the InstructionsF of (SCM R); ::_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 R) such that
A2: x = JumpPart I and
A3: InsCode I = T ;
consider a, b being Data-Location of R such that
A4: I = MultBy (a,b) by A1, A3, Th16;
x = {} by A2, A4, RECDEF_2:def_2;
hence x in {{}} by TARSKI:def_1; ::_thesis: verum
end;
set a = the Data-Location of R;
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 Data-Location of R, the Data-Location of R)) by RECDEF_2:def_2;
InsCode (MultBy ( the Data-Location of R, the Data-Location of R)) = 4 by RECDEF_2:def_1;
hence x in JumpParts T by A5, A1; ::_thesis: verum
end;
theorem :: SCMRING3:25
for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 5 holds
JumpParts T = {{}}
proof
let R be Ring; ::_thesis: for T being InsType of the InstructionsF of (SCM R) st T = 5 holds
JumpParts T = {{}}
let T be InsType of the InstructionsF of (SCM R); ::_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 R) such that
A2: x = JumpPart I and
A3: InsCode I = T ;
consider a being Data-Location of R, r being Element of R such that
A4: I = a := r by A1, A3, Th17;
x = {} by A2, A4, RECDEF_2:def_2;
hence x in {{}} by TARSKI:def_1; ::_thesis: verum
end;
set a = the Data-Location of R;
set r = the Element of R;
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 Data-Location of R := the Element of R) by RECDEF_2:def_2;
InsCode ( the Data-Location of R := the Element of R) = 5 by RECDEF_2:def_1;
hence x in JumpParts T by A5, A1; ::_thesis: verum
end;
theorem Th26: :: SCMRING3:26
for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 6 holds
dom (product" (JumpParts T)) = {1}
proof
let R be Ring; ::_thesis: for T being InsType of the InstructionsF of (SCM R) st T = 6 holds
dom (product" (JumpParts T)) = {1}
let T be InsType of the InstructionsF of (SCM R); ::_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 ,R)) = <* 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 ,R)) = 6 by RECDEF_2:def_1;
then A3: JumpPart (goto ( the Element of NAT ,R)) 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 ,R))) 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 R) such that
A5: f = JumpPart I and
A6: InsCode I = T ;
consider i1 being Element of NAT such that
A7: I = goto (i1,R) by A1, A6, Th18;
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 Th27: :: SCMRING3:27
for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 7 holds
dom (product" (JumpParts T)) = {1}
proof
let R be Ring; ::_thesis: for T being InsType of the InstructionsF of (SCM R) st T = 7 holds
dom (product" (JumpParts T)) = {1}
let T be InsType of the InstructionsF of (SCM R); ::_thesis: ( T = 7 implies dom (product" (JumpParts T)) = {1} )
set i1 = the Element of NAT ;
set a = the Data-Location of R;
assume A1: T = 7 ; ::_thesis: dom (product" (JumpParts T)) = {1}
A2: JumpPart ( the Data-Location of R =0_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 ( the Data-Location of R =0_goto the Element of NAT ) = 7 by RECDEF_2:def_1;
then A3: JumpPart ( the Data-Location of R =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 Data-Location of R =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 R) such that
A5: f = JumpPart I and
A6: InsCode I = T ;
consider a being Data-Location of R, i1 being Element of NAT such that
A7: I = a =0_goto i1 by A1, A6, Th19;
f = <*i1*> by A5, A7, RECDEF_2:def_2;
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 :: SCMRING3:28
for R being Ring
for i1 being Element of NAT holds (product" (JumpParts (InsCode (goto (i1,R))))) . 1 = NAT
proof
let R be Ring; ::_thesis: for i1 being Element of NAT holds (product" (JumpParts (InsCode (goto (i1,R))))) . 1 = NAT
let i1 be Element of NAT ; ::_thesis: (product" (JumpParts (InsCode (goto (i1,R))))) . 1 = NAT
dom (product" (JumpParts (InsCode (goto (i1,R))))) = {1} by Th10, Th26;
then A1: 1 in dom (product" (JumpParts (InsCode (goto (i1,R))))) by TARSKI:def_1;
A2: InsCode (goto (i1,R)) = 6 by RECDEF_2:def_1;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: NAT c= (product" (JumpParts (InsCode (goto (i1,R))))) . 1
let x be set ; ::_thesis: ( x in (product" (JumpParts (InsCode (goto (i1,R))))) . 1 implies x in NAT )
assume x in (product" (JumpParts (InsCode (goto (i1,R))))) . 1 ; ::_thesis: x in NAT
then x in pi ((JumpParts (InsCode (goto (i1,R)))),1) by A1, CARD_3:def_12;
then consider g being Function such that
A3: g in JumpParts (InsCode (goto (i1,R))) and
A4: x = g . 1 by CARD_3:def_6;
consider I being Instruction of (SCM R) such that
A5: g = JumpPart I and
A6: InsCode I = InsCode (goto (i1,R)) by A3;
consider i2 being Element of NAT such that
A7: I = goto (i2,R) by A2, A6, Th18;
g = <*i2*> by A5, A7, RECDEF_2:def_2;
then x = i2 by A4, 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,R))))) . 1 )
assume x in NAT ; ::_thesis: x in (product" (JumpParts (InsCode (goto (i1,R))))) . 1
then reconsider x = x as Element of NAT ;
( JumpPart (goto (x,R)) = <*x*> & InsCode (goto (i1,R)) = InsCode (goto (x,R)) ) by A2, RECDEF_2:def_1, RECDEF_2:def_2;
then A8: <*x*> in JumpParts (InsCode (goto (i1,R))) ;
<*x*> . 1 = x by FINSEQ_1:def_8;
then x in pi ((JumpParts (InsCode (goto (i1,R)))),1) by A8, CARD_3:def_6;
hence x in (product" (JumpParts (InsCode (goto (i1,R))))) . 1 by A1, CARD_3:def_12; ::_thesis: verum
end;
theorem :: SCMRING3:29
for R being Ring
for a being Data-Location of R
for i1 being Element of NAT holds (product" (JumpParts (InsCode (a =0_goto i1)))) . 1 = NAT
proof
let R be Ring; ::_thesis: for a being Data-Location of R
for i1 being Element of NAT holds (product" (JumpParts (InsCode (a =0_goto i1)))) . 1 = NAT
let a be Data-Location of R; ::_thesis: for i1 being Element of NAT holds (product" (JumpParts (InsCode (a =0_goto i1)))) . 1 = NAT
let i1 be Element of NAT ; ::_thesis: (product" (JumpParts (InsCode (a =0_goto i1)))) . 1 = NAT
dom (product" (JumpParts (InsCode (a =0_goto i1)))) = {1} by Th11, Th27;
then A1: 1 in dom (product" (JumpParts (InsCode (a =0_goto i1)))) by TARSKI:def_1;
A2: InsCode (a =0_goto i1) = 7 by RECDEF_2: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
A3: g in JumpParts (InsCode (a =0_goto i1)) and
A4: x = g . 1 by CARD_3:def_6;
consider I being Instruction of (SCM R) such that
A5: g = JumpPart I and
A6: InsCode I = InsCode (a =0_goto i1) by A3;
consider b being Data-Location of R, i2 being Element of NAT such that
A7: I = b =0_goto i2 by A2, A6, Th19;
g = <*i2*> by A5, A7, RECDEF_2:def_2;
then x = i2 by A4, 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 ;
( JumpPart (a =0_goto x) = <*x*> & InsCode (a =0_goto i1) = InsCode (a =0_goto x) ) by A2, RECDEF_2:def_1, RECDEF_2:def_2;
then A8: <*x*> in JumpParts (InsCode (a =0_goto i1)) ;
<*x*> . 1 = x by FINSEQ_1:40;
then x in pi ((JumpParts (InsCode (a =0_goto i1))),1) by A8, CARD_3:def_6;
hence x in (product" (JumpParts (InsCode (a =0_goto i1)))) . 1 by A1, CARD_3:def_12; ::_thesis: verum
end;
Lm3: for R being Ring
for i being Instruction of (SCM R) st ( for l being Element of NAT holds NIC (i,l) = {(succ l)} ) holds
JUMP i is empty
proof
let R be Ring; ::_thesis: for i being Instruction of (SCM R) st ( for l being Element of NAT holds NIC (i,l) = {(succ l)} ) holds
JUMP i is empty
set p = 1;
set q = 2;
let i be Instruction of (SCM R); ::_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 = 1, q = 2 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
let R be Ring;
cluster JUMP (halt (SCM R)) -> empty ;
coherence
JUMP (halt (SCM R)) is empty ;
end;
registration
let R be Ring;
let a, b be Data-Location of R;
clustera := b -> sequential ;
coherence
a := b is sequential
proof
let s be State of (SCM R); :: according to AMISTD_1:def_8 ::_thesis: (Exec ((a := b),s)) . (0. (SCM R)) = succ (IC s)
thus (Exec ((a := b),s)) . (0. (SCM R)) = succ (IC s) by SCMRING2:11; ::_thesis: verum
end;
cluster AddTo (a,b) -> sequential ;
coherence
AddTo (a,b) is sequential
proof
let s be State of (SCM R); :: according to AMISTD_1:def_8 ::_thesis: (Exec ((AddTo (a,b)),s)) . (0. (SCM R)) = succ (IC s)
thus (Exec ((AddTo (a,b)),s)) . (0. (SCM R)) = succ (IC s) by SCMRING2:12; ::_thesis: verum
end;
cluster SubFrom (a,b) -> sequential ;
coherence
SubFrom (a,b) is sequential
proof
let s be State of (SCM R); :: according to AMISTD_1:def_8 ::_thesis: (Exec ((SubFrom (a,b)),s)) . (0. (SCM R)) = succ (IC s)
thus (Exec ((SubFrom (a,b)),s)) . (0. (SCM R)) = succ (IC s) by SCMRING2:13; ::_thesis: verum
end;
cluster MultBy (a,b) -> sequential ;
coherence
MultBy (a,b) is sequential
proof
let s be State of (SCM R); :: according to AMISTD_1:def_8 ::_thesis: (Exec ((MultBy (a,b)),s)) . (0. (SCM R)) = succ (IC s)
thus (Exec ((MultBy (a,b)),s)) . (0. (SCM R)) = succ (IC s) by SCMRING2:14; ::_thesis: verum
end;
end;
registration
let R be Ring;
let a be Data-Location of R;
let r be Element of R;
clustera := r -> sequential ;
coherence
a := r is sequential
proof
let s be State of (SCM R); :: according to AMISTD_1:def_8 ::_thesis: (Exec ((a := r),s)) . (0. (SCM R)) = succ (IC s)
thus (Exec ((a := r),s)) . (0. (SCM R)) = succ (IC s) by SCMRING2:17; ::_thesis: verum
end;
end;
registration
let R be Ring;
let a, b be Data-Location of R;
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 Lm3; ::_thesis: verum
end;
end;
registration
let R be Ring;
let a, b be Data-Location of R;
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 Lm3; ::_thesis: verum
end;
end;
registration
let R be Ring;
let a, b be Data-Location of R;
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 Lm3; ::_thesis: verum
end;
end;
registration
let R be Ring;
let a, b be Data-Location of R;
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 Lm3; ::_thesis: verum
end;
end;
registration
let R be Ring;
let a be Data-Location of R;
let r be Element of R;
cluster JUMP (a := r) -> empty ;
coherence
JUMP (a := r) is empty
proof
for l being Element of NAT holds NIC ((a := r),l) = {(succ l)} by AMISTD_1:12;
hence JUMP (a := r) is empty by Lm3; ::_thesis: verum
end;
end;
theorem Th30: :: SCMRING3:30
for R being Ring
for i1, il being Element of NAT holds NIC ((goto (i1,R)),il) = {i1}
proof
let R be Ring; ::_thesis: for i1, il being Element of NAT holds NIC ((goto (i1,R)),il) = {i1}
let i1, il be Element of NAT ; ::_thesis: NIC ((goto (i1,R)),il) = {i1}
now__::_thesis:_for_x_being_set_holds_
(_x_in_{i1}_iff_x_in__{__(IC_(Exec_((goto_(i1,R)),s)))_where_s_is_Element_of_product_(the_Values_of_(SCM_R))_:_IC_s_=_il__}__)
let x be set ; ::_thesis: ( x in {i1} iff x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il } )
A1: now__::_thesis:_(_x_=_i1_implies_x_in__{__(IC_(Exec_((goto_(i1,R)),s)))_where_s_is_Element_of_product_(the_Values_of_(SCM_R))_:_IC_s_=_il__}__)
reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def_6;
set I = goto (i1,R);
set t = the State of (SCM R);
set Q = the Instruction-Sequence of (SCM R);
assume A2: x = i1 ; ::_thesis: x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il }
reconsider u = the State of (SCM R) +* ((IC ),il1) as Element of product (the_Values_of (SCM R)) by CARD_3:107;
reconsider P = the Instruction-Sequence of (SCM R) +* (il,(goto (i1,R))) as Instruction-Sequence of (SCM R) ;
A3: P /. il = P . il by PBOOLE:143;
IC in dom the State of (SCM R) by MEMSTR_0:2;
then A4: IC u = il by FUNCT_7:31;
il in NAT ;
then il in dom the Instruction-Sequence of (SCM R) by PARTFUN1:def_2;
then A5: P . il = goto (i1,R) by FUNCT_7:31;
then IC (Following (P,u)) = i1 by A4, A3, SCMRING2:15;
hence x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il } by A2, A3, A4, A5; ::_thesis: verum
end;
now__::_thesis:_(_x_in__{__(IC_(Exec_((goto_(i1,R)),s)))_where_s_is_Element_of_product_(the_Values_of_(SCM_R))_:_IC_s_=_il__}__implies_x_=_i1_)
assume x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il } ; ::_thesis: x = i1
then ex s being Element of product (the_Values_of (SCM R)) st
( x = IC (Exec ((goto (i1,R)),s)) & IC s = il ) ;
hence x = i1 by SCMRING2:15; ::_thesis: verum
end;
hence ( x in {i1} iff x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il } ) by A1, TARSKI:def_1; ::_thesis: verum
end;
hence NIC ((goto (i1,R)),il) = {i1} by TARSKI:1; ::_thesis: verum
end;
theorem Th31: :: SCMRING3:31
for R being Ring
for i1 being Element of NAT holds JUMP (goto (i1,R)) = {i1}
proof
let R be Ring; ::_thesis: for i1 being Element of NAT holds JUMP (goto (i1,R)) = {i1}
let i1 be Element of NAT ; ::_thesis: JUMP (goto (i1,R)) = {i1}
set X = { (NIC ((goto (i1,R)),il)) where il is Element of NAT : verum } ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_meet__{__(NIC_((goto_(i1,R)),il))_where_il_is_Element_of_NAT_:_verum__}__implies_x_in_{i1}_)_&_(_x_in_{i1}_implies_x_in_meet__{__(NIC_((goto_(i1,R)),il))_where_il_is_Element_of_NAT_:_verum__}__)_)
let x be set ; ::_thesis: ( ( x in meet { (NIC ((goto (i1,R)),il)) where il is Element of NAT : verum } implies x in {i1} ) & ( x in {i1} implies x in meet { (NIC ((goto (i1,R)),il)) where il is Element of NAT : verum } ) )
hereby ::_thesis: ( x in {i1} implies x in meet { (NIC ((goto (i1,R)),il)) where il is Element of NAT : verum } )
reconsider il1 = 1 as Element of NAT ;
A1: NIC ((goto (i1,R)),il1) in { (NIC ((goto (i1,R)),il)) where il is Element of NAT : verum } ;
assume x in meet { (NIC ((goto (i1,R)),il)) where il is Element of NAT : verum } ; ::_thesis: x in {i1}
then x in NIC ((goto (i1,R)),il1) by A1, SETFAM_1:def_1;
hence x in {i1} by Th30; ::_thesis: verum
end;
assume x in {i1} ; ::_thesis: x in meet { (NIC ((goto (i1,R)),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,R)),il))_where_il_is_Element_of_NAT_:_verum__}__holds_
i1_in_Y
let Y be set ; ::_thesis: ( Y in { (NIC ((goto (i1,R)),il)) where il is Element of NAT : verum } implies i1 in Y )
assume Y in { (NIC ((goto (i1,R)),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,R)),il) ;
NIC ((goto (i1,R)),il) = {i1} by Th30;
hence i1 in Y by A4, TARSKI:def_1; ::_thesis: verum
end;
NIC ((goto (i1,R)),i1) in { (NIC ((goto (i1,R)),il)) where il is Element of NAT : verum } ;
hence x in meet { (NIC ((goto (i1,R)),il)) where il is Element of NAT : verum } by A2, A3, SETFAM_1:def_1; ::_thesis: verum
end;
hence JUMP (goto (i1,R)) = {i1} by TARSKI:1; ::_thesis: verum
end;
registration
let R be Ring;
let i1 be Element of NAT ;
cluster JUMP (goto (i1,R)) -> 1 -element ;
coherence
JUMP (goto (i1,R)) is 1 -element
proof
JUMP (goto (i1,R)) = {i1} by Th31;
hence JUMP (goto (i1,R)) is 1 -element ; ::_thesis: verum
end;
end;
theorem Th32: :: SCMRING3:32
for R being Ring
for a being Data-Location of R
for i1, il being Element of NAT holds
( i1 in NIC ((a =0_goto i1),il) & NIC ((a =0_goto i1),il) c= {i1,(succ il)} )
proof
let R be Ring; ::_thesis: for a being Data-Location of R
for i1, il being Element of NAT holds
( i1 in NIC ((a =0_goto i1),il) & NIC ((a =0_goto i1),il) c= {i1,(succ il)} )
let a be Data-Location of R; ::_thesis: for i1, il being Element of NAT holds
( i1 in NIC ((a =0_goto i1),il) & NIC ((a =0_goto i1),il) c= {i1,(succ il)} )
let i1, il be Element of NAT ; ::_thesis: ( i1 in NIC ((a =0_goto i1),il) & NIC ((a =0_goto i1),il) c= {i1,(succ il)} )
set t = the State of (SCM R);
set Q = the Instruction-Sequence of (SCM R);
set I = a =0_goto i1;
reconsider a9 = a as Element of Data-Locations by SCMRING2:1;
reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def_6;
Values a = ((SCM-VAL R) * SCM-OK) . a9 by SCMRING2:24
.= the carrier of R by AMI_3:27, SCMRING1:4 ;
then reconsider 0R = 0. R as Element of Values a ;
reconsider u = the State of (SCM R) +* ((IC ),il1) as Element of product (the_Values_of (SCM R)) by CARD_3:107;
reconsider P = the Instruction-Sequence of (SCM R) +* (il,(a =0_goto i1)) as Instruction-Sequence of (SCM R) ;
reconsider v = u +* (a .--> 0R) as Element of product (the_Values_of (SCM R)) by CARD_3:107;
A1: IC in dom the State of (SCM R) by MEMSTR_0:2;
A2: dom (a .--> 0R) = {a} by FUNCOP_1:13;
IC <> a by Th2;
then not IC in dom (a .--> 0R) by A2, TARSKI:def_1;
then A3: IC v = IC u by FUNCT_4:11
.= il by A1, FUNCT_7:31 ;
A4: P /. il = P . il by PBOOLE:143;
il in NAT ;
then il in dom the Instruction-Sequence of (SCM R) by PARTFUN1:def_2;
then A5: P . il = a =0_goto i1 by FUNCT_7:31;
a in dom (a .--> 0R) by A2, TARSKI:def_1;
then v . a = (a .--> 0R) . a by FUNCT_4:13
.= 0. R by FUNCOP_1:72 ;
then IC (Following (P,v)) = i1 by A3, A5, A4, SCMRING2:16;
hence i1 in NIC ((a =0_goto i1),il) by A3, A5, A4; ::_thesis: NIC ((a =0_goto i1),il) c= {i1,(succ il)}
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NIC ((a =0_goto i1),il) or x in {i1,(succ il)} )
assume x in NIC ((a =0_goto i1),il) ; ::_thesis: x in {i1,(succ il)}
then consider s being Element of product (the_Values_of (SCM R)) such that
A6: ( x = IC (Exec ((a =0_goto i1),s)) & IC s = il ) ;
percases ( s . a = 0. R or s . a <> 0. R ) ;
suppose s . a = 0. R ; ::_thesis: x in {i1,(succ il)}
then x = i1 by A6, SCMRING2:16;
hence x in {i1,(succ il)} by TARSKI:def_2; ::_thesis: verum
end;
suppose s . a <> 0. R ; ::_thesis: x in {i1,(succ il)}
then x = succ il by A6, SCMRING2:16;
hence x in {i1,(succ il)} by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
theorem :: SCMRING3:33
for R being non trivial Ring
for a being Data-Location of R
for il, i1 being Element of NAT holds NIC ((a =0_goto i1),il) = {i1,(succ il)}
proof
let R be non trivial Ring; ::_thesis: for a being Data-Location of R
for il, i1 being Element of NAT holds NIC ((a =0_goto i1),il) = {i1,(succ il)}
let a be Data-Location of R; ::_thesis: for il, i1 being Element of NAT holds NIC ((a =0_goto i1),il) = {i1,(succ il)}
let il, i1 be Element of NAT ; ::_thesis: NIC ((a =0_goto i1),il) = {i1,(succ il)}
set t = the State of (SCM R);
set Q = the Instruction-Sequence of (SCM R);
set I = a =0_goto i1;
reconsider a9 = a as Element of Data-Locations by SCMRING2:1;
A1: Values a = ((SCM-VAL R) * SCM-OK) . a9 by SCMRING2:24
.= the carrier of R by AMI_3:27, SCMRING1:4 ;
reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def_6;
thus NIC ((a =0_goto i1),il) c= {i1,(succ il)} by Th32; :: according to XBOOLE_0:def_10 ::_thesis: {i1,(succ il)} c= NIC ((a =0_goto i1),il)
reconsider u = the State of (SCM R) +* ((IC ),il1) as Element of product (the_Values_of (SCM R)) by CARD_3:107;
reconsider P = the Instruction-Sequence of (SCM R) +* (il,(a =0_goto i1)) as Instruction-Sequence of (SCM R) ;
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) )
A2: IC <> a by Th2;
A3: IC in dom the State of (SCM R) by MEMSTR_0:2;
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 0R = 0. R as Element of Values a by A1;
reconsider v = u +* (a .--> 0R) as Element of product (the_Values_of (SCM R)) by CARD_3:107;
A6: dom (a .--> 0R) = {a} by FUNCOP_1:13;
then not IC in dom (a .--> 0R) by A2, TARSKI:def_1;
then A7: IC v = IC u by FUNCT_4:11
.= il by A3, FUNCT_7:31 ;
A8: P /. il = P . il by PBOOLE:143;
il in NAT ;
then il in dom the Instruction-Sequence of (SCM R) by PARTFUN1:def_2;
then A9: P . il = a =0_goto i1 by FUNCT_7:31;
a in dom (a .--> 0R) by A6, TARSKI:def_1;
then v . a = (a .--> 0R) . a by FUNCT_4:13
.= 0. R by FUNCOP_1:72 ;
then IC (Following (P,v)) = i1 by A7, A8, A9, SCMRING2:16;
hence x in NIC ((a =0_goto i1),il) by A5, A7, A8, A9; ::_thesis: verum
end;
supposeA10: x = succ il ; ::_thesis: x in NIC ((a =0_goto i1),il)
consider e being Element of R such that
A11: e <> 0. R by STRUCT_0:def_18;
reconsider E = e as Element of Values a by A1;
reconsider v = u +* (a .--> E) as Element of product (the_Values_of (SCM R)) by CARD_3:107;
A12: dom (a .--> E) = {a} by FUNCOP_1:13;
then not IC in dom (a .--> E) by A2, TARSKI:def_1;
then A13: IC v = IC u by FUNCT_4:11
.= il by A3, FUNCT_7:31 ;
A14: P /. il = P . il by PBOOLE:143;
il in NAT ;
then il in dom the Instruction-Sequence of (SCM R) by PARTFUN1:def_2;
then A15: P . il = a =0_goto i1 by FUNCT_7:31;
a in dom (a .--> E) by A12, TARSKI:def_1;
then v . a = (a .--> E) . a by FUNCT_4:13
.= E by FUNCOP_1:72 ;
then IC (Following (P,v)) = succ il by A11, A13, A14, A15, SCMRING2:16;
hence x in NIC ((a =0_goto i1),il) by A10, A13, A14, A15; ::_thesis: verum
end;
end;
end;
theorem Th34: :: SCMRING3:34
for R being Ring
for a being Data-Location of R
for i1 being Element of NAT holds JUMP (a =0_goto i1) = {i1}
proof
let R be Ring; ::_thesis: for a being Data-Location of R
for i1 being Element of NAT holds JUMP (a =0_goto i1) = {i1}
let a be Data-Location of R; ::_thesis: for i1 being Element of NAT holds JUMP (a =0_goto i1) = {i1}
let i1 be Element of NAT ; ::_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 ex il being Element of NAT st Y = NIC ((a =0_goto i1),il) ;
hence i1 in Y by Th32; ::_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 } )
reconsider il1 = 1, il2 = 2 as Element of NAT ;
assume A2: x in meet { (NIC ((a =0_goto i1),il)) where il is Element of NAT : verum } ; ::_thesis: x in {i1}
A3: NIC ((a =0_goto i1),il2) c= {i1,(succ il2)} by Th32;
NIC ((a =0_goto i1),il2) in { (NIC ((a =0_goto i1),il)) where il is Element of NAT : verum } ;
then x in NIC ((a =0_goto i1),il2) by A2, SETFAM_1:def_1;
then A4: ( x = i1 or x = succ il2 ) by A3, TARSKI:def_2;
A5: NIC ((a =0_goto i1),il1) c= {i1,(succ il1)} by Th32;
NIC ((a =0_goto i1),il1) in { (NIC ((a =0_goto i1),il)) where il is Element of NAT : verum } ;
then x in NIC ((a =0_goto i1),il1) by A2, SETFAM_1:def_1;
then ( x = i1 or x = succ il1 ) by A5, TARSKI:def_2;
hence x in {i1} by A4, 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 A6: 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 A6, A1, SETFAM_1:def_1; ::_thesis: verum
end;
hence JUMP (a =0_goto i1) = {i1} by TARSKI:1; ::_thesis: verum
end;
registration
let R be Ring;
let a be Data-Location of R;
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 Th34;
hence JUMP (a =0_goto i1) is 1 -element ; ::_thesis: verum
end;
end;
theorem Th35: :: SCMRING3:35
for R being Ring
for il being Element of NAT holds SUCC (il,(SCM R)) = {il,(succ il)}
proof
let R be Ring; ::_thesis: for il being Element of NAT holds SUCC (il,(SCM R)) = {il,(succ il)}
let il be Element of NAT ; ::_thesis: SUCC (il,(SCM R)) = {il,(succ il)}
set X = { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of (SCM R) : 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_R)_:_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_R)_:_verum__}__)_)
let x be set ; ::_thesis: ( ( x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of (SCM R) : 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 R) : 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 R) : verum } )
assume x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of (SCM R) : 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 R) : verum } by TARSKI:def_4;
consider i being Element of the InstructionsF of (SCM R) such that
A3: Y = (NIC (i,il)) \ (JUMP i) by A2;
percases ( i = [0,{},{}] or ex a, b being Data-Location of R st i = a := b or ex a, b being Data-Location of R st i = AddTo (a,b) or ex a, b being Data-Location of R st i = SubFrom (a,b) or ex a, b being Data-Location of R st i = MultBy (a,b) or ex i1 being Element of NAT st i = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st i = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st i = a := r ) by SCMRING2:7;
suppose i = [0,{},{}] ; ::_thesis: x in {il,(succ il)}
then i = halt (SCM R) ;
then x in {il} \ (JUMP (halt (SCM R))) 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 Data-Location of R st i = a := b ; ::_thesis: x in {il,(succ il)}
then consider a, b being Data-Location of R 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 Data-Location of R st i = AddTo (a,b) ; ::_thesis: x in {il,(succ il)}
then consider a, b being Data-Location of R 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 Data-Location of R st i = SubFrom (a,b) ; ::_thesis: x in {il,(succ il)}
then consider a, b being Data-Location of R 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 Data-Location of R st i = MultBy (a,b) ; ::_thesis: x in {il,(succ il)}
then consider a, b being Data-Location of R 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 i1 being Element of NAT st i = goto (i1,R) ; ::_thesis: x in {il,(succ il)}
then consider i1 being Element of NAT such that
A8: i = goto (i1,R) ;
x in {i1} \ (JUMP i) by A1, A3, A8, Th30;
then x in {i1} \ {i1} by A8, Th31;
hence x in {il,(succ il)} by XBOOLE_1:37; ::_thesis: verum
end;
suppose ex a being Data-Location of R ex i1 being Element of NAT st i = a =0_goto i1 ; ::_thesis: x in {il,(succ il)}
then consider a being Data-Location of R, i1 being Element of NAT such that
A9: i = a =0_goto i1 ;
A10: NIC (i,il) c= {i1,(succ il)} by A9, Th32;
x in NIC (i,il) by A1, A3, XBOOLE_0:def_5;
then A11: ( x = i1 or x = succ il ) by A10, TARSKI:def_2;
x in (NIC (i,il)) \ {i1} by A1, A3, A9, Th34;
then not x in {i1} by XBOOLE_0:def_5;
hence x in {il,(succ il)} by A11, TARSKI:def_1, TARSKI:def_2; ::_thesis: verum
end;
suppose ex a being Data-Location of R ex r being Element of R st i = a := r ; ::_thesis: x in {il,(succ il)}
then consider a being Data-Location of R, r being Element of R such that
A12: i = a := r ;
x in {(succ il)} \ (JUMP (a := r)) by A1, A3, A12, 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 A13: x in {il,(succ il)} ; ::_thesis: b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of (SCM R) : verum }
percases ( x = il or x = succ il ) by A13, TARSKI:def_2;
supposeA14: x = il ; ::_thesis: b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of (SCM R) : verum }
set i = halt (SCM R);
(NIC ((halt (SCM R)),il)) \ (JUMP (halt (SCM R))) = {il} by AMISTD_1:2;
then A15: {il} in { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of (SCM R) : verum } ;
x in {il} by A14, TARSKI:def_1;
hence x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of (SCM R) : verum } by A15, TARSKI:def_4; ::_thesis: verum
end;
supposeA16: x = succ il ; ::_thesis: b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of (SCM R) : verum }
set a = the Data-Location of R;
set i = AddTo ( the Data-Location of R, the Data-Location of R);
(NIC ((AddTo ( the Data-Location of R, the Data-Location of R)),il)) \ (JUMP (AddTo ( the Data-Location of R, the Data-Location of R))) = {(succ il)} by AMISTD_1:12;
then A17: {(succ il)} in { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of (SCM R) : verum } ;
x in {(succ il)} by A16, TARSKI:def_1;
hence x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of (SCM R) : verum } by A17, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence SUCC (il,(SCM R)) = {il,(succ il)} by TARSKI:1; ::_thesis: verum
end;
theorem Th36: :: SCMRING3:36
for R being Ring
for k being Element of NAT holds
( k + 1 in SUCC (k,(SCM R)) & ( for j being Element of NAT st j in SUCC (k,(SCM R)) holds
k <= j ) )
proof
let R be Ring; ::_thesis: for k being Element of NAT holds
( k + 1 in SUCC (k,(SCM R)) & ( for j being Element of NAT st j in SUCC (k,(SCM R)) holds
k <= j ) )
let k be Element of NAT ; ::_thesis: ( k + 1 in SUCC (k,(SCM R)) & ( for j being Element of NAT st j in SUCC (k,(SCM R)) holds
k <= j ) )
reconsider fk = k as Element of NAT ;
A1: SUCC (k,(SCM R)) = {k,(succ fk)} by Th35;
hence k + 1 in SUCC (k,(SCM R)) by TARSKI:def_2; ::_thesis: for j being Element of NAT st j in SUCC (k,(SCM R)) holds
k <= j
let j be Element of NAT ; ::_thesis: ( j in SUCC (k,(SCM R)) implies k <= j )
assume A2: j in SUCC (k,(SCM R)) ; ::_thesis: k <= j
reconsider fk = k as Element of NAT ;
percases ( j = k or j = succ fk ) by A1, A2, TARSKI:def_2;
suppose j = k ; ::_thesis: k <= j
hence k <= j ; ::_thesis: verum
end;
suppose j = succ fk ; ::_thesis: k <= j
hence k <= j by NAT_1:11; ::_thesis: verum
end;
end;
end;
registration
let R be Ring;
cluster SCM R -> standard ;
coherence
SCM R is standard
proof
deffunc H1( Element of NAT ) -> Element of NAT = R;
for k being Element of NAT holds
( k + 1 in SUCC (k,(SCM R)) & ( for j being Element of NAT st j in SUCC (k,(SCM R)) holds
k <= j ) ) by Th36;
hence SCM R is standard by AMISTD_1:3; ::_thesis: verum
end;
end;
definition
let R be Ring;
let k be Element of NAT ;
func dl. (R,k) -> Data-Location of R equals :: SCMRING3:def 1
dl. k;
coherence
dl. k is Data-Location of R
proof
dl. k in Data-Locations by AMI_2:def_16, AMI_3:27;
hence dl. k is Data-Location of R by SCMRING2:1; ::_thesis: verum
end;
end;
:: deftheorem defines dl. SCMRING3:def_1_:_
for R being Ring
for k being Element of NAT holds dl. (R,k) = dl. k;
registration
let R be Ring;
cluster InsCode (halt (SCM R)) -> jump-only for InsType of the InstructionsF of (SCM R);
coherence
for b1 being InsType of the InstructionsF of (SCM R) st b1 = InsCode (halt (SCM R)) holds
b1 is jump-only
proof
now__::_thesis:_for_s_being_State_of_(SCM_R)
for_o_being_Object_of_(SCM_R)
for_I_being_Instruction_of_(SCM_R)_st_InsCode_I_=_InsCode_(halt_(SCM_R))_&_o_in_Data-Locations_holds_
(Exec_(I,s))_._o_=_s_._o
let s be State of (SCM R); ::_thesis: for o being Object of (SCM R)
for I being Instruction of (SCM R) st InsCode I = InsCode (halt (SCM R)) & o in Data-Locations holds
(Exec (I,s)) . o = s . o
let o be Object of (SCM R); ::_thesis: for I being Instruction of (SCM R) st InsCode I = InsCode (halt (SCM R)) & o in Data-Locations holds
(Exec (I,s)) . o = s . o
let I be Instruction of (SCM R); ::_thesis: ( InsCode I = InsCode (halt (SCM R)) & o in Data-Locations implies (Exec (I,s)) . o = s . o )
assume that
A1: InsCode I = InsCode (halt (SCM R)) and
o in Data-Locations ; ::_thesis: (Exec (I,s)) . o = s . o
I = halt (SCM R) by A1, Th12, 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 R) st b1 = InsCode (halt (SCM R)) holds
b1 is jump-only by AMISTD_1:def_1; ::_thesis: verum
end;
end;
registration
let R be Ring;
cluster halt (SCM R) -> jump-only ;
coherence
halt (SCM R) is jump-only
proof
thus InsCode (halt (SCM R)) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum
end;
end;
registration
let R be Ring;
let i1 be Element of NAT ;
cluster InsCode (goto (i1,R)) -> jump-only for InsType of the InstructionsF of (SCM R);
coherence
for b1 being InsType of the InstructionsF of (SCM R) st b1 = InsCode (goto (i1,R)) holds
b1 is jump-only
proof
set S = SCM R;
now__::_thesis:_for_s_being_State_of_(SCM_R)
for_o_being_Object_of_(SCM_R)
for_I_being_Instruction_of_(SCM_R)_st_InsCode_I_=_InsCode_(goto_(i1,R))_&_o_in_Data-Locations_holds_
(Exec_(I,s))_._o_=_s_._o
let s be State of (SCM R); ::_thesis: for o being Object of (SCM R)
for I being Instruction of (SCM R) st InsCode I = InsCode (goto (i1,R)) & o in Data-Locations holds
(Exec (I,s)) . o = s . o
let o be Object of (SCM R); ::_thesis: for I being Instruction of (SCM R) st InsCode I = InsCode (goto (i1,R)) & o in Data-Locations holds
(Exec (I,s)) . o = s . o
let I be Instruction of (SCM R); ::_thesis: ( InsCode I = InsCode (goto (i1,R)) & o in Data-Locations implies (Exec (I,s)) . o = s . o )
assume that
A1: InsCode I = InsCode (goto (i1,R)) and
A2: o in Data-Locations ; ::_thesis: (Exec (I,s)) . o = s . o
InsCode (goto (i1,R)) = 6 by RECDEF_2:def_1;
then A3: ex i2 being Element of NAT st I = goto (i2,R) by A1, Th18;
o in Data-Locations by A2, SCMRING2:22;
then o is Data-Location of R by SCMRING2:1;
hence (Exec (I,s)) . o = s . o by A3, SCMRING2:15; ::_thesis: verum
end;
hence for b1 being InsType of the InstructionsF of (SCM R) st b1 = InsCode (goto (i1,R)) holds
b1 is jump-only by AMISTD_1:def_1; ::_thesis: verum
end;
end;
registration
let R be Ring;
let i1 be Element of NAT ;
cluster goto (i1,R) -> jump-only ;
coherence
goto (i1,R) is jump-only
proof
thus InsCode (goto (i1,R)) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum
end;
end;
registration
let R be Ring;
let a be Data-Location of R;
let i1 be Element of NAT ;
cluster InsCode (a =0_goto i1) -> jump-only for InsType of the InstructionsF of (SCM R);
coherence
for b1 being InsType of the InstructionsF of (SCM R) st b1 = InsCode (a =0_goto i1) holds
b1 is jump-only
proof
set S = SCM R;
now__::_thesis:_for_s_being_State_of_(SCM_R)
for_o_being_Object_of_(SCM_R)
for_I_being_Instruction_of_(SCM_R)_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 R); ::_thesis: for o being Object of (SCM R)
for I being Instruction of (SCM R) st InsCode I = InsCode (a =0_goto i1) & o in Data-Locations holds
(Exec (I,s)) . o = s . o
let o be Object of (SCM R); ::_thesis: for I being Instruction of (SCM R) st InsCode I = InsCode (a =0_goto i1) & o in Data-Locations holds
(Exec (I,s)) . o = s . o
let I be Instruction of (SCM R); ::_thesis: ( InsCode I = InsCode (a =0_goto i1) & o in Data-Locations implies (Exec (I,s)) . o = s . o )
assume that
A1: InsCode I = InsCode (a =0_goto i1) and
A2: o in Data-Locations ; ::_thesis: (Exec (I,s)) . o = s . o
InsCode (a =0_goto i1) = 7 by RECDEF_2:def_1;
then A3: ex b being Data-Location of R ex i2 being Element of NAT st I = b =0_goto i2 by A1, Th19;
o in Data-Locations by A2, SCMRING2:22;
then o is Data-Location of R by SCMRING2:1;
hence (Exec (I,s)) . o = s . o by A3, SCMRING2:16; ::_thesis: verum
end;
hence for b1 being InsType of the InstructionsF of (SCM R) st b1 = InsCode (a =0_goto i1) holds
b1 is jump-only by AMISTD_1:def_1; ::_thesis: verum
end;
end;
registration
let R be Ring;
let a be Data-Location of R;
let i1 be Element of NAT ;
clustera =0_goto i1 -> jump-only ;
coherence
a =0_goto i1 is jump-only
proof
thus InsCode (a =0_goto i1) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum
end;
end;
registration
let S be non trivial Ring;
let p, q be Data-Location of S;
cluster InsCode (p := q) -> non jump-only for InsType of the InstructionsF of (SCM S);
coherence
for b1 being InsType of the InstructionsF of (SCM S) st b1 = InsCode (p := q) holds
not b1 is jump-only
proof
set w = the State of (SCM S);
consider e being Element of S such that
A1: e <> 0. S by STRUCT_0:def_18;
reconsider e = e as Element of S ;
set t = the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e));
A2: dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) = {(dl. (S,0)),(dl. (S,1))} by FUNCT_4:62;
then A3: dl. (S,1) in dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) by TARSKI:def_2;
A4: InsCode (p := q) = 1 by RECDEF_2:def_1
.= InsCode ((dl. (S,0)) := (dl. (S,1))) by RECDEF_2:def_1 ;
dl. (S,0) in Data-Locations by SCMRING2:1;
then A5: dl. (S,0) in Data-Locations by SCMRING2:22;
dl. (S,0) in dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) by A2, TARSKI:def_2;
then A6: ( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,0)) = (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) . (dl. (S,0)) by FUNCT_4:13
.= 0. S by AMI_3:10, FUNCT_4:63 ;
(Exec (((dl. (S,0)) := (dl. (S,1))),( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))))) . (dl. (S,0)) = ( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,1)) by SCMRING2:11
.= (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) . (dl. (S,1)) by A3, FUNCT_4:13
.= e by FUNCT_4:63 ;
hence for b1 being InsType of the InstructionsF of (SCM S) st b1 = InsCode (p := q) holds
not b1 is jump-only by A1, A4, A6, A5, AMISTD_1:def_1; ::_thesis: verum
end;
end;
registration
let S be non trivial Ring;
let p, q be Data-Location of S;
clusterp := q -> non jump-only ;
coherence
not p := q is jump-only
proof
thus not InsCode (p := q) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum
end;
end;
registration
let S be non trivial Ring;
let p, q be Data-Location of S;
cluster InsCode (AddTo (p,q)) -> non jump-only for InsType of the InstructionsF of (SCM S);
coherence
for b1 being InsType of the InstructionsF of (SCM S) st b1 = InsCode (AddTo (p,q)) holds
not b1 is jump-only
proof
set w = the State of (SCM S);
consider e being Element of S such that
A1: e <> 0. S by STRUCT_0:def_18;
reconsider e = e as Element of S ;
set t = the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e));
A2: dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) = {(dl. (S,0)),(dl. (S,1))} by FUNCT_4:62;
then dl. (S,0) in dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) by TARSKI:def_2;
then A3: ( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,0)) = (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) . (dl. (S,0)) by FUNCT_4:13
.= 0. S by AMI_3:10, FUNCT_4:63 ;
A4: InsCode (AddTo (p,q)) = 2 by RECDEF_2:def_1
.= InsCode (AddTo ((dl. (S,0)),(dl. (S,1)))) by RECDEF_2:def_1 ;
dl. (S,1) in dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) by A2, TARSKI:def_2;
then A5: ( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,1)) = (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) . (dl. (S,1)) by FUNCT_4:13
.= e by FUNCT_4:63 ;
dl. (S,0) in Data-Locations by SCMRING2:1;
then A6: dl. (S,0) in Data-Locations by SCMRING2:22;
(Exec ((AddTo ((dl. (S,0)),(dl. (S,1)))),( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))))) . (dl. (S,0)) = (( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,0))) + (( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,1))) by SCMRING2:12
.= e by A3, A5, RLVECT_1:4 ;
hence for b1 being InsType of the InstructionsF of (SCM S) st b1 = InsCode (AddTo (p,q)) holds
not b1 is jump-only by A1, A4, A3, A6, AMISTD_1:def_1; ::_thesis: verum
end;
end;
registration
let S be non trivial Ring;
let p, q be Data-Location of S;
cluster AddTo (p,q) -> non jump-only ;
coherence
not AddTo (p,q) is jump-only
proof
thus not InsCode (AddTo (p,q)) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum
end;
end;
registration
let S be non trivial Ring;
let p, q be Data-Location of S;
cluster InsCode (SubFrom (p,q)) -> non jump-only for InsType of the InstructionsF of (SCM S);
coherence
for b1 being InsType of the InstructionsF of (SCM S) st b1 = InsCode (SubFrom (p,q)) holds
not b1 is jump-only
proof
set w = the State of (SCM S);
consider e being Element of S such that
A1: e <> 0. S by STRUCT_0:def_18;
reconsider e = e as Element of S ;
A2: now__::_thesis:_not_-_e_=_0._S
assume - e = 0. S ; ::_thesis: contradiction
then e = - (0. S) by RLVECT_1:17;
hence contradiction by A1, RLVECT_1:12; ::_thesis: verum
end;
set t = the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e));
A3: InsCode (SubFrom (p,q)) = 3 by RECDEF_2:def_1
.= InsCode (SubFrom ((dl. (S,0)),(dl. (S,1)))) by RECDEF_2:def_1 ;
A4: dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) = {(dl. (S,0)),(dl. (S,1))} by FUNCT_4:62;
then dl. (S,0) in dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) by TARSKI:def_2;
then A5: ( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,0)) = (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) . (dl. (S,0)) by FUNCT_4:13
.= 0. S by AMI_3:10, FUNCT_4:63 ;
dl. (S,1) in dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) by A4, TARSKI:def_2;
then A6: ( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,1)) = (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) . (dl. (S,1)) by FUNCT_4:13
.= e by FUNCT_4:63 ;
dl. (S,0) in Data-Locations by SCMRING2:1;
then A7: dl. (S,0) in Data-Locations by SCMRING2:22;
(Exec ((SubFrom ((dl. (S,0)),(dl. (S,1)))),( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))))) . (dl. (S,0)) = (( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,0))) - (( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,1))) by SCMRING2:13
.= - e by A5, A6, RLVECT_1:14 ;
hence for b1 being InsType of the InstructionsF of (SCM S) st b1 = InsCode (SubFrom (p,q)) holds
not b1 is jump-only by A3, A5, A2, A7, AMISTD_1:def_1; ::_thesis: verum
end;
end;
registration
let S be non trivial Ring;
let p, q be Data-Location of S;
cluster SubFrom (p,q) -> non jump-only ;
coherence
not SubFrom (p,q) is jump-only
proof
thus not InsCode (SubFrom (p,q)) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum
end;
end;
registration
let S be non trivial Ring;
let p, q be Data-Location of S;
cluster InsCode (MultBy (p,q)) -> non jump-only for InsType of the InstructionsF of (SCM S);
coherence
for b1 being InsType of the InstructionsF of (SCM S) st b1 = InsCode (MultBy (p,q)) holds
not b1 is jump-only
proof
IC = IC by AMI_3:1, SCMRING2:8;
then A1: ( 0. S <> 1_ S & dl. (S,0) <> IC ) by AMI_3:13, LMOD_6:def_1;
set w = the State of (SCM S);
set t = the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S)));
A2: InsCode (MultBy (p,q)) = 4 by RECDEF_2:def_1
.= InsCode (MultBy ((dl. (S,0)),(dl. (S,1)))) by RECDEF_2:def_1 ;
A3: dom (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S))) = {(dl. (S,0)),(dl. (S,1))} by FUNCT_4:62;
then dl. (S,0) in dom (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S))) by TARSKI:def_2;
then A4: ( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S)))) . (dl. (S,0)) = (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S))) . (dl. (S,0)) by FUNCT_4:13
.= 1_ S by AMI_3:10, FUNCT_4:63 ;
dl. (S,1) in dom (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S))) by A3, TARSKI:def_2;
then A5: ( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S)))) . (dl. (S,1)) = (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S))) . (dl. (S,1)) by FUNCT_4:13
.= 0. S by FUNCT_4:63 ;
dl. (S,0) in Data-Locations by SCMRING2:1;
then A6: dl. (S,0) in Data-Locations by SCMRING2:22;
(Exec ((MultBy ((dl. (S,0)),(dl. (S,1)))),( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S)))))) . (dl. (S,0)) = (( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S)))) . (dl. (S,0))) * (( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S)))) . (dl. (S,1))) by SCMRING2:14
.= 0. S by A5, VECTSP_1:6 ;
hence for b1 being InsType of the InstructionsF of (SCM S) st b1 = InsCode (MultBy (p,q)) holds
not b1 is jump-only by A2, A1, A4, A6, AMISTD_1:def_1; ::_thesis: verum
end;
end;
registration
let S be non trivial Ring;
let p, q be Data-Location of S;
cluster MultBy (p,q) -> non jump-only ;
coherence
not MultBy (p,q) is jump-only
proof
thus not InsCode (MultBy (p,q)) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum
end;
end;
registration
let S be non trivial Ring;
let p be Data-Location of S;
let w be Element of S;
cluster InsCode (p := w) -> non jump-only for InsType of the InstructionsF of (SCM S);
coherence
for b1 being InsType of the InstructionsF of (SCM S) st b1 = InsCode (p := w) holds
not b1 is jump-only
proof
set j = the State of (SCM S);
A1: InsCode (p := w) = 5 by RECDEF_2:def_1
.= InsCode ((dl. (S,0)) := w) by RECDEF_2:def_1 ;
the carrier of S <> {w} ;
then consider e being set such that
A2: e in the carrier of S and
A3: e <> w by ZFMISC_1:35;
Values (dl. (S,0)) = the carrier of S by Th1;
then reconsider e = e as Element of Values (dl. (S,0)) by A2;
reconsider v = (dl. (S,0)) .--> e as PartState of (SCM S) ;
set t = the State of (SCM S) +* v;
dom ((dl. (S,0)) .--> e) = {(dl. (S,0))} by FUNCOP_1:13;
then dl. (S,0) in dom ((dl. (S,0)) .--> e) by TARSKI:def_1;
then A4: ( the State of (SCM S) +* v) . (dl. (S,0)) = ((dl. (S,0)) .--> e) . (dl. (S,0)) by FUNCT_4:13
.= e by FUNCOP_1:72 ;
dl. (S,0) in Data-Locations by SCMRING2:1;
then A5: dl. (S,0) in Data-Locations by SCMRING2:22;
(Exec (((dl. (S,0)) := w),( the State of (SCM S) +* v))) . (dl. (S,0)) = w by SCMRING2:17;
hence for b1 being InsType of the InstructionsF of (SCM S) st b1 = InsCode (p := w) holds
not b1 is jump-only by A3, A1, A4, A5, AMISTD_1:def_1; ::_thesis: verum
end;
end;
registration
let S be non trivial Ring;
let p be Data-Location of S;
let w be Element of S;
clusterp := w -> non jump-only ;
coherence
not p := w is jump-only
proof
thus not InsCode (p := w) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum
end;
end;
registration
let R be Ring;
let i1 be Element of NAT ;
cluster goto (i1,R) -> non sequential ;
coherence
not goto (i1,R) is sequential
proof
JUMP (goto (i1,R)) <> {} ;
hence not goto (i1,R) is sequential by AMISTD_1:13; ::_thesis: verum
end;
end;
registration
let R be Ring;
let a be Data-Location of R;
let i1 be Element of NAT ;
clustera =0_goto i1 -> non sequential ;
coherence
not a =0_goto i1 is sequential
proof
JUMP (a =0_goto i1) <> {} ;
hence not a =0_goto i1 is sequential by AMISTD_1:13; ::_thesis: verum
end;
end;
registration
let R be Ring;
let i1 be Element of NAT ;
cluster goto (i1,R) -> non ins-loc-free ;
coherence
not goto (i1,R) is ins-loc-free
proof
dom (JumpPart (goto (i1,R))) = dom <*i1*> by RECDEF_2:def_2
.= {1} by FINSEQ_1:2, FINSEQ_1:def_8 ;
hence not JumpPart (goto (i1,R)) is empty ; :: according to COMPOS_0:def_8 ::_thesis: verum
end;
end;
registration
let R be Ring;
let a be Data-Location of R;
let i1 be Element of NAT ;
clustera =0_goto i1 -> non ins-loc-free ;
coherence
not a =0_goto i1 is ins-loc-free
proof
dom (JumpPart (a =0_goto i1)) = dom <*i1*> by RECDEF_2:def_2
.= {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;
registration
let R be Ring;
cluster SCM R -> with_explicit_jumps ;
coherence
SCM R is with_explicit_jumps
proof
let I be Instruction of (SCM R); :: 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 (JumpPart I) 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 Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Element of NAT st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:7;
supposeA2: I = [0,{},{}] ; ::_thesis: f in rng (JumpPart I)
JUMP (halt (SCM R)) is empty ;
hence f in rng (JumpPart I) by A1, A2; ::_thesis: verum
end;
suppose ex a, b being Data-Location of R 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 Data-Location of R 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 Data-Location of R 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 Data-Location of R st I = MultBy (a,b) ; ::_thesis: f in rng (JumpPart I)
hence f in rng (JumpPart I) by A1; ::_thesis: verum
end;
supposeA3: ex i1 being Element of NAT st I = goto (i1,R) ; ::_thesis: f in rng (JumpPart I)
consider i1 being Element of NAT such that
A4: I = goto (i1,R) by A3;
A5: JumpPart (goto (i1,R)) = <*i1*> by RECDEF_2:def_2;
rng <*i1*> = {i1} by FINSEQ_1:39;
hence f in rng (JumpPart I) by A1, A4, A5, Th31; ::_thesis: verum
end;
supposeA6: ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 ; ::_thesis: f in rng (JumpPart I)
consider a being Data-Location of R, i1 being Element of NAT such that
A7: I = a =0_goto i1 by A6;
A8: JumpPart (a =0_goto i1) = <*i1*> by RECDEF_2:def_2;
rng <*i1*> = {i1} by FINSEQ_1:39;
hence f in rng (JumpPart I) by A1, A7, A8, Th34; ::_thesis: verum
end;
suppose ex a being Data-Location of R ex r being Element of R st I = a := r ; ::_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 (JumpPart I) or f in JUMP I )
assume f in rng (JumpPart I) ; ::_thesis: f in JUMP I
then consider k being set such that
A9: k in dom (JumpPart I) and
A10: f = (JumpPart I) . k by FUNCT_1:def_3;
percases ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Element of NAT st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:7;
suppose I = [0,{},{}] ; ::_thesis: f in JUMP I
then I = halt (SCM R) ;
hence f in JUMP I by A9; ::_thesis: verum
end;
suppose ex a, b being Data-Location of R st I = a := b ; ::_thesis: f in JUMP I
then consider a, b being Data-Location of R such that
A11: I = a := b ;
k in dom {} by A9, A11, RECDEF_2:def_2;
hence f in JUMP I ; ::_thesis: verum
end;
suppose ex a, b being Data-Location of R st I = AddTo (a,b) ; ::_thesis: f in JUMP I
then consider a, b being Data-Location of R such that
A12: I = AddTo (a,b) ;
k in dom {} by A9, A12, RECDEF_2:def_2;
hence f in JUMP I ; ::_thesis: verum
end;
suppose ex a, b being Data-Location of R st I = SubFrom (a,b) ; ::_thesis: f in JUMP I
then consider a, b being Data-Location of R such that
A13: I = SubFrom (a,b) ;
k in dom {} by A9, A13, RECDEF_2:def_2;
hence f in JUMP I ; ::_thesis: verum
end;
suppose ex a, b being Data-Location of R st I = MultBy (a,b) ; ::_thesis: f in JUMP I
then consider a, b being Data-Location of R such that
A14: I = MultBy (a,b) ;
k in dom {} by A9, A14, RECDEF_2:def_2;
hence f in JUMP I ; ::_thesis: verum
end;
suppose ex i1 being Element of NAT st I = goto (i1,R) ; ::_thesis: f in JUMP I
then consider i1 being Element of NAT such that
A15: I = goto (i1,R) ;
A16: JumpPart I = <*i1*> by A15, RECDEF_2:def_2;
then k = 1 by A9, Lm1;
then A17: f = i1 by A16, A10, FINSEQ_1:def_8;
JUMP I = {i1} by A15, Th31;
hence f in JUMP I by A17, TARSKI:def_1; ::_thesis: verum
end;
suppose ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 ; ::_thesis: f in JUMP I
then consider a being Data-Location of R, i1 being Element of NAT such that
A18: I = a =0_goto i1 ;
A19: JumpPart I = <*i1*> by A18, RECDEF_2:def_2;
then k = 1 by A9, Lm1;
then A20: f = i1 by A19, A10, FINSEQ_1:40;
JUMP I = {i1} by A18, Th34;
hence f in JUMP I by A20, TARSKI:def_1; ::_thesis: verum
end;
suppose ex a being Data-Location of R ex r being Element of R st I = a := r ; ::_thesis: f in JUMP I
then consider a being Data-Location of R, r being Element of R such that
A21: I = a := r ;
k in dom {} by A9, A21, RECDEF_2:def_2;
hence f in JUMP I ; ::_thesis: verum
end;
end;
end;
end;
theorem Th37: :: SCMRING3:37
for R being Ring
for i1 being Element of NAT
for k being Nat holds IncAddr ((goto (i1,R)),k) = goto ((i1 + k),R)
proof
let R be Ring; ::_thesis: for i1 being Element of NAT
for k being Nat holds IncAddr ((goto (i1,R)),k) = goto ((i1 + k),R)
let i1 be Element of NAT ; ::_thesis: for k being Nat holds IncAddr ((goto (i1,R)),k) = goto ((i1 + k),R)
let k be Nat; ::_thesis: IncAddr ((goto (i1,R)),k) = goto ((i1 + k),R)
A1: JumpPart (IncAddr ((goto (i1,R)),k)) = k + (JumpPart (goto (i1,R))) by COMPOS_0:def_9;
then A2: dom (JumpPart (IncAddr ((goto (i1,R)),k))) = dom (JumpPart (goto (i1,R))) by VALUED_1:def_2;
A3: dom (JumpPart (goto ((i1 + k),R))) = 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,R))) by RECDEF_2:def_2 ;
A4: for x being set st x in dom (JumpPart (goto (i1,R))) holds
(JumpPart (IncAddr ((goto (i1,R)),k))) . x = (JumpPart (goto ((i1 + k),R))) . x
proof
let x be set ; ::_thesis: ( x in dom (JumpPart (goto (i1,R))) implies (JumpPart (IncAddr ((goto (i1,R)),k))) . x = (JumpPart (goto ((i1 + k),R))) . x )
assume A5: x in dom (JumpPart (goto (i1,R))) ; ::_thesis: (JumpPart (IncAddr ((goto (i1,R)),k))) . x = (JumpPart (goto ((i1 + k),R))) . x
then x in dom <*i1*> by RECDEF_2:def_2;
then A6: x = 1 by Lm1;
reconsider f = (JumpPart (goto (i1,R))) . x as Element of NAT by ORDINAL1:def_12;
A7: (JumpPart (IncAddr ((goto (i1,R)),k))) . x = k + f by A5, A1, A2, VALUED_1:def_2;
f = <*i1*> . x by RECDEF_2:def_2
.= i1 by A6, FINSEQ_1:def_8 ;
hence (JumpPart (IncAddr ((goto (i1,R)),k))) . x = <*(i1 + k)*> . x by A6, A7, FINSEQ_1:def_8
.= (JumpPart (goto ((i1 + k),R))) . x by RECDEF_2:def_2 ;
::_thesis: verum
end;
A8: InsCode (IncAddr ((goto (i1,R)),k)) = InsCode (goto (i1,R)) by COMPOS_0:def_9
.= 6 by RECDEF_2:def_1
.= InsCode (goto ((i1 + k),R)) by RECDEF_2:def_1 ;
A9: AddressPart (IncAddr ((goto (i1,R)),k)) = AddressPart (goto (i1,R)) by COMPOS_0:def_9
.= {} by RECDEF_2:def_3
.= AddressPart (goto ((i1 + k),R)) by RECDEF_2:def_3 ;
JumpPart (IncAddr ((goto (i1,R)),k)) = JumpPart (goto ((i1 + k),R)) by A2, A3, A4, FUNCT_1:2;
hence IncAddr ((goto (i1,R)),k) = goto ((i1 + k),R) by A8, A9, COMPOS_0:1; ::_thesis: verum
end;
theorem Th38: :: SCMRING3:38
for R being Ring
for a being Data-Location of R
for i1 being Element of NAT
for k being Nat holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)
proof
let R be Ring; ::_thesis: for a being Data-Location of R
for i1 being Element of NAT
for k being Nat holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)
let a be Data-Location of R; ::_thesis: for i1 being Element of NAT
for k being Nat holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)
let i1 be Element of NAT ; ::_thesis: for k being Nat holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)
let k be Nat; ::_thesis: IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)
A1: JumpPart (IncAddr ((a =0_goto i1),k)) = k + (JumpPart (a =0_goto i1)) by COMPOS_0:def_9;
then A2: dom (JumpPart (IncAddr ((a =0_goto i1),k))) = dom (JumpPart (a =0_goto i1)) by VALUED_1:def_2;
A3: dom (JumpPart (a =0_goto (i1 + k))) = dom <*(i1 + k)*> by RECDEF_2:def_2
.= Seg 1 by FINSEQ_1:38
.= dom <*i1*> by FINSEQ_1:38
.= dom (JumpPart (a =0_goto i1)) by RECDEF_2:def_2 ;
A4: 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 A5: 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 RECDEF_2:def_2;
then A6: x = 1 by FINSEQ_1:90;
reconsider f = (JumpPart (a =0_goto i1)) . x as Element of NAT by ORDINAL1:def_12;
A7: (JumpPart (IncAddr ((a =0_goto i1),k))) . x = k + f by A5, A1, A2, VALUED_1:def_2;
f = <*i1*> . x by RECDEF_2:def_2
.= i1 by A6, FINSEQ_1:40 ;
hence (JumpPart (IncAddr ((a =0_goto i1),k))) . x = <*(i1 + k)*> . x by A6, A7, FINSEQ_1:40
.= (JumpPart (a =0_goto (i1 + k))) . x by RECDEF_2:def_2 ;
::_thesis: verum
end;
A8: InsCode (IncAddr ((a =0_goto i1),k)) = InsCode (a =0_goto i1) by COMPOS_0:def_9
.= 7 by RECDEF_2:def_1
.= InsCode (a =0_goto (i1 + k)) by RECDEF_2:def_1 ;
A9: AddressPart (IncAddr ((a =0_goto i1),k)) = AddressPart (a =0_goto i1) by COMPOS_0:def_9
.= <*a*> by RECDEF_2:def_3
.= AddressPart (a =0_goto (i1 + k)) by RECDEF_2:def_3 ;
JumpPart (IncAddr ((a =0_goto i1),k)) = JumpPart (a =0_goto (i1 + k)) by A2, A3, A4, FUNCT_1:2;
hence IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k) by A8, A9, COMPOS_0:1; ::_thesis: verum
end;
registration
let R be Ring;
cluster SCM R -> IC-relocable ;
coherence
SCM R is IC-relocable
proof
thus SCM R is IC-relocable ::_thesis: verum
proof
let I be Instruction of (SCM R); :: according to AMISTD_2:def_4 ::_thesis: I is IC-relocable
percases ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Element of NAT st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:7;
suppose I = [0,{},{}] ; ::_thesis: I is IC-relocable
then I = halt (SCM R) ;
hence I is IC-relocable ; ::_thesis: verum
end;
suppose ex a, b being Data-Location of R st I = a := b ; ::_thesis: I is IC-relocable
hence I is IC-relocable ; ::_thesis: verum
end;
suppose ex a, b being Data-Location of R st I = AddTo (a,b) ; ::_thesis: I is IC-relocable
hence I is IC-relocable ; ::_thesis: verum
end;
suppose ex a, b being Data-Location of R st I = SubFrom (a,b) ; ::_thesis: I is IC-relocable
hence I is IC-relocable ; ::_thesis: verum
end;
suppose ex a, b being Data-Location of R st I = MultBy (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,R) ; ::_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 R); ::_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,R) by A1;
thus (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC (Exec ((goto ((j + i1),R)),s1))) + k by A2, Th37
.= (j + i1) + k by SCMRING2:15
.= IC (Exec ((goto (((j + i1) + k),R)),(IncIC (s1,k)))) by SCMRING2:15
.= IC (Exec ((goto (((j + k) + i1),R)),(IncIC (s1,k))))
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A2, Th37 ; ::_thesis: verum
end;
suppose ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 ; ::_thesis: I is IC-relocable
then consider a being Data-Location of R, 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 R); ::_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 Th2, FUNCOP_1:13;
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. R or s1 . a <> 0. R ) ;
supposeA5: s1 . a = 0. R ; ::_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, Th38
.= (j + i1) + k by A5, SCMRING2:16
.= IC (Exec ((a =0_goto ((j + i1) + k)),(IncIC (s1,k)))) by A4, A5, SCMRING2:16
.= IC (Exec ((a =0_goto ((j + k) + i1)),(IncIC (s1,k))))
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A3, Th38 ; ::_thesis: verum
end;
supposeA6: s1 . a <> 0. R ; ::_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, Th38;
A8: IncAddr (I,(j + k)) = a =0_goto (i1 + (j + k)) by A3, Th38;
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, SCMRING2:16
.= ((IC s1) + 1) + k
.= succ (IC (IncIC (s1,k))) by A9
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A8, A6, A4, SCMRING2:16 ; ::_thesis: verum
end;
end;
end;
suppose ex a being Data-Location of R ex r being Element of R st I = a := r ; ::_thesis: I is IC-relocable
hence I is IC-relocable ; ::_thesis: verum
end;
end;
end;
end;
end;
theorem :: SCMRING3:39
for R being Ring
for I being Instruction of (SCM R) holds InsCode I <= 7
proof
let R be Ring; ::_thesis: for I being Instruction of (SCM R) holds InsCode I <= 7
let I be Instruction of (SCM R); ::_thesis: InsCode I <= 7
set T = InsCode I;
( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 or InsCode I = 6 or InsCode I = 7 ) by Lm2;
hence InsCode I <= 7 ; ::_thesis: verum
end;