let INS be Instruction of SCM+FSA; :: thesis: for s being State of SCM+FSA
for p being FinPartState of SCM+FSA
for i, j, k being Element of NAT st IC s = j + k holds
Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
let s be State of SCM+FSA; :: thesis: for p being FinPartState of SCM+FSA
for i, j, k being Element of NAT st IC s = j + k holds
Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
let p be FinPartState of SCM+FSA; :: thesis: for i, j, k being Element of NAT st IC s = j + k holds
Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
let i, j, k be Element of NAT ; :: thesis: ( IC s = j + k implies Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)) )
A1: now
let d be Element of NAT ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d
thus (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by AMI_1:def 13
.= s . d by COMPOS_1:20
.= (Exec ((IncAddr (INS,k)),s)) . d by AMI_1:def 13
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by COMPOS_1:20 ; :: thesis: verum
end;
A2: ( not InsCode INS <= 9 + 1 or InsCode INS <= 8 + 1 or InsCode INS = 10 ) by NAT_1:8;
A3: ( not InsCode INS <= 10 + 1 or InsCode INS <= 10 or InsCode INS = 11 ) by NAT_1:8;
A4: InsCode INS <= 11 + 1 by SCMFSA_2:35;
assume A5: IC s = j + k ; :: thesis: Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
then A6: succ ((IC s) -' k) = succ ((j + k) -' k)
.= succ j by NAT_D:34
.= j + 1 by NAT_1:39
.= ((j + 1) + k) -' k by NAT_D:34
.= ((j + 1) + k) -' k
.= ((j + k) + 1) -' k
.= (succ (IC s)) -' k by A5, NAT_1:39 ;
per cases ( InsCode INS = 0 or InsCode INS = 1 or InsCode INS = 2 or InsCode INS = 3 or InsCode INS = 4 or InsCode INS = 5 or InsCode INS = 6 or InsCode INS = 7 or InsCode INS = 8 or InsCode INS = 9 or InsCode INS = 10 or InsCode INS = 11 or InsCode INS = 12 ) by A4, A3, A2, NAT_1:8, NAT_1:33;
suppose A7: InsCode INS = 0 ; :: thesis: Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
A8: IncAddr ((halt SCM+FSA),k) = halt SCM+FSA by Th8;
A9: INS = halt SCM+FSA by A7, SCMFSA_2:122;
hence Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = s +* (Start-At (((IC s) -' k),SCM+FSA)) by EXTPRO_1:def 3
.= s +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)) by A9, EXTPRO_1:def 3
.= (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)) by A9, EXTPRO_1:def 3 ;
:: thesis: verum
end;
suppose InsCode INS = 1 ; :: thesis: Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
then consider da, db being Int-Location such that
A10: INS = da := db by SCMFSA_2:54;
A11: IncAddr (INS,k) = da := db by A10, Th9;
A12: now
let d be FinSeq-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d
thus (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A10, SCMFSA_2:89
.= s . d by SCMFSA_3:12
.= (Exec ((IncAddr (INS,k)),s)) . d by A11, SCMFSA_2:89
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:12 ; :: thesis: verum
end;
A13: now
let d be Int-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
per cases ( da = d or da <> d ) ;
suppose A14: da = d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . db by A10, SCMFSA_2:89
.= s . db by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A11, A14, SCMFSA_2:89
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ;
:: thesis: verum
end;
suppose A15: da <> d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A10, SCMFSA_2:89
.= s . d by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A11, A15, SCMFSA_2:89
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ;
:: thesis: verum
end;
end;
end;
IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = succ (IC (s +* (Start-At (((IC s) -' k),SCM+FSA)))) by A10, SCMFSA_2:89
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec ((IncAddr (INS,k)),s))) -' k by A11, SCMFSA_2:89
.= IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) by FUNCT_4:121 ;
hence Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)) by A1, A12, A13, SCMFSA_2:86; :: thesis: verum
end;
suppose InsCode INS = 2 ; :: thesis: Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
then consider da, db being Int-Location such that
A16: INS = AddTo (da,db) by SCMFSA_2:55;
A17: IncAddr (INS,k) = AddTo (da,db) by A16, Th10;
A18: now
let d be FinSeq-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d
thus (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A16, SCMFSA_2:90
.= s . d by SCMFSA_3:12
.= (Exec ((IncAddr (INS,k)),s)) . d by A17, SCMFSA_2:90
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:12 ; :: thesis: verum
end;
A19: now
let d be Int-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
per cases ( da = d or da <> d ) ;
suppose A20: da = d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . da) + ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . db) by A16, SCMFSA_2:90
.= (s . da) + ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . db) by SCMFSA_3:11
.= (s . da) + (s . db) by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A17, A20, SCMFSA_2:90
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ;
:: thesis: verum
end;
suppose A21: da <> d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A16, SCMFSA_2:90
.= s . d by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A17, A21, SCMFSA_2:90
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ;
:: thesis: verum
end;
end;
end;
IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = succ (IC (s +* (Start-At (((IC s) -' k),SCM+FSA)))) by A16, SCMFSA_2:90
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec ((IncAddr (INS,k)),s))) -' k by A17, SCMFSA_2:90
.= IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) by FUNCT_4:121 ;
hence Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)) by A1, A18, A19, SCMFSA_2:86; :: thesis: verum
end;
suppose InsCode INS = 3 ; :: thesis: Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
then consider da, db being Int-Location such that
A22: INS = SubFrom (da,db) by SCMFSA_2:56;
A23: IncAddr (INS,k) = SubFrom (da,db) by A22, Th11;
A24: now
let d be FinSeq-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d
thus (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A22, SCMFSA_2:91
.= s . d by SCMFSA_3:12
.= (Exec ((IncAddr (INS,k)),s)) . d by A23, SCMFSA_2:91
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:12 ; :: thesis: verum
end;
A25: now
let d be Int-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
per cases ( da = d or da <> d ) ;
suppose A26: da = d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . da) - ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . db) by A22, SCMFSA_2:91
.= (s . da) - ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . db) by SCMFSA_3:11
.= (s . da) - (s . db) by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A23, A26, SCMFSA_2:91
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ;
:: thesis: verum
end;
suppose A27: da <> d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A22, SCMFSA_2:91
.= s . d by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A23, A27, SCMFSA_2:91
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ;
:: thesis: verum
end;
end;
end;
IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = succ (IC (s +* (Start-At (((IC s) -' k),SCM+FSA)))) by A22, SCMFSA_2:91
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec ((IncAddr (INS,k)),s))) -' k by A23, SCMFSA_2:91
.= IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) by FUNCT_4:121 ;
hence Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)) by A1, A24, A25, SCMFSA_2:86; :: thesis: verum
end;
suppose InsCode INS = 4 ; :: thesis: Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
then consider da, db being Int-Location such that
A28: INS = MultBy (da,db) by SCMFSA_2:57;
A29: IncAddr (INS,k) = MultBy (da,db) by A28, Th12;
A30: now
let d be FinSeq-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d
thus (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A28, SCMFSA_2:92
.= s . d by SCMFSA_3:12
.= (Exec ((IncAddr (INS,k)),s)) . d by A29, SCMFSA_2:92
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:12 ; :: thesis: verum
end;
A31: now
let d be Int-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
per cases ( da = d or da <> d ) ;
suppose A32: da = d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . da) * ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . db) by A28, SCMFSA_2:92
.= (s . da) * ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . db) by SCMFSA_3:11
.= (s . da) * (s . db) by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A29, A32, SCMFSA_2:92
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ;
:: thesis: verum
end;
suppose A33: da <> d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A28, SCMFSA_2:92
.= s . d by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A29, A33, SCMFSA_2:92
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ;
:: thesis: verum
end;
end;
end;
IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = succ (IC (s +* (Start-At (((IC s) -' k),SCM+FSA)))) by A28, SCMFSA_2:92
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec ((IncAddr (INS,k)),s))) -' k by A29, SCMFSA_2:92
.= IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) by FUNCT_4:121 ;
hence Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)) by A1, A30, A31, SCMFSA_2:86; :: thesis: verum
end;
suppose InsCode INS = 5 ; :: thesis: Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
then consider da, db being Int-Location such that
A34: INS = Divide (da,db) by SCMFSA_2:58;
A35: IncAddr (INS,k) = Divide (da,db) by A34, Th13;
now
per cases ( da <> db or da = db ) ;
suppose A36: da <> db ; :: thesis: Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
A37: now
let d be Int-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
per cases ( da = d or db = d or ( da <> d & db <> d ) ) ;
suppose A38: da = d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . da) div ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . db) by A34, A36, SCMFSA_2:93
.= (s . da) div ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . db) by SCMFSA_3:11
.= (s . da) div (s . db) by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A35, A36, A38, SCMFSA_2:93
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ;
:: thesis: verum
end;
suppose A39: db = d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . da) mod ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . db) by A34, SCMFSA_2:93
.= (s . da) mod ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . db) by SCMFSA_3:11
.= (s . da) mod (s . db) by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A35, A39, SCMFSA_2:93
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ;
:: thesis: verum
end;
suppose A40: ( da <> d & db <> d ) ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A34, SCMFSA_2:93
.= s . d by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A35, A40, SCMFSA_2:93
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ;
:: thesis: verum
end;
end;
end;
A41: now
let d be FinSeq-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d
thus (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A34, SCMFSA_2:93
.= s . d by SCMFSA_3:12
.= (Exec ((IncAddr (INS,k)),s)) . d by A35, SCMFSA_2:93
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:12 ; :: thesis: verum
end;
IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = succ (IC (s +* (Start-At (((IC s) -' k),SCM+FSA)))) by A34, SCMFSA_2:93
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec ((IncAddr (INS,k)),s))) -' k by A35, SCMFSA_2:93
.= IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) by FUNCT_4:121 ;
hence Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)) by A1, A41, A37, SCMFSA_2:86; :: thesis: verum
end;
suppose A42: da = db ; :: thesis: Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
A43: now
let d be Int-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
per cases ( da = d or da <> d ) ;
suppose A44: da = d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . da) mod ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . db) by A34, A42, SCMFSA_2:94
.= (s . da) mod ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . db) by SCMFSA_3:11
.= (s . da) mod (s . db) by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A35, A42, A44, SCMFSA_2:94
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ;
:: thesis: verum
end;
suppose A45: da <> d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A34, A42, SCMFSA_2:94
.= s . d by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A35, A42, A45, SCMFSA_2:94
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ;
:: thesis: verum
end;
end;
end;
A46: now
let d be FinSeq-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d
thus (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A34, A42, SCMFSA_2:94
.= s . d by SCMFSA_3:12
.= (Exec ((IncAddr (INS,k)),s)) . d by A35, A42, SCMFSA_2:94
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:12 ; :: thesis: verum
end;
IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = succ (IC (s +* (Start-At (((IC s) -' k),SCM+FSA)))) by A34, A42, SCMFSA_2:94
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec ((IncAddr (INS,k)),s))) -' k by A35, A42, SCMFSA_2:94
.= IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) by FUNCT_4:121 ;
hence Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)) by A1, A46, A43, SCMFSA_2:86; :: thesis: verum
end;
end;
end;
hence Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)) ; :: thesis: verum
end;
suppose InsCode INS = 6 ; :: thesis: Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
then consider loc being Element of NAT such that
A47: INS = goto loc by SCMFSA_2:59;
A48: IncAddr (INS,k) = goto (loc + k) by A47, Th14;
then A49: IC (Exec ((IncAddr (INS,k)),s)) = loc + k by SCMFSA_2:95;
A50: now
let d be Int-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d
thus (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A47, SCMFSA_2:95
.= s . d by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A48, SCMFSA_2:95
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ; :: thesis: verum
end;
A51: now
let d be FinSeq-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d
thus (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A47, SCMFSA_2:95
.= s . d by SCMFSA_3:12
.= (Exec ((IncAddr (INS,k)),s)) . d by A48, SCMFSA_2:95
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:12 ; :: thesis: verum
end;
IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = loc by A47, SCMFSA_2:95
.= (IC (Exec ((IncAddr (INS,k)),s))) -' k by A49, NAT_D:34
.= IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) by FUNCT_4:121 ;
hence Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)) by A1, A51, A50, SCMFSA_2:86; :: thesis: verum
end;
suppose InsCode INS = 7 ; :: thesis: Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
then consider loc being Element of NAT , da being Int-Location such that
A52: INS = da =0_goto loc by SCMFSA_2:60;
A53: IncAddr (INS,k) = da =0_goto (loc + k) by A52, Th15;
A54: now
let d be Int-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d
thus (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A52, SCMFSA_2:96
.= s . d by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A53, SCMFSA_2:96
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ; :: thesis: verum
end;
A55: now
per cases ( s . da = 0 or s . da <> 0 ) ;
suppose A56: s . da = 0 ; :: thesis: IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)))
then A57: IC (Exec ((IncAddr (INS,k)),s)) = loc + k by A53, SCMFSA_2:96;
(s +* (Start-At (((IC s) -' k),SCM+FSA))) . da = 0 by A56, SCMFSA_3:11;
then IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = loc by A52, SCMFSA_2:96
.= (IC (Exec ((IncAddr (INS,k)),s))) -' k by A57, NAT_D:34
.= IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) by FUNCT_4:121 ;
hence IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) ; :: thesis: verum
end;
suppose A58: s . da <> 0 ; :: thesis: IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)))
then (s +* (Start-At (((IC s) -' k),SCM+FSA))) . da <> 0 by SCMFSA_3:11;
then IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = succ (IC (s +* (Start-At (((IC s) -' k),SCM+FSA)))) by A52, SCMFSA_2:96
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec ((IncAddr (INS,k)),s))) -' k by A53, A58, SCMFSA_2:96
.= IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) by FUNCT_4:121 ;
hence IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) ; :: thesis: verum
end;
end;
end;
now
let d be FinSeq-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d
thus (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A52, SCMFSA_2:96
.= s . d by SCMFSA_3:12
.= (Exec ((IncAddr (INS,k)),s)) . d by A53, SCMFSA_2:96
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:12 ; :: thesis: verum
end;
hence Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)) by A1, A55, A54, SCMFSA_2:86; :: thesis: verum
end;
suppose InsCode INS = 8 ; :: thesis: Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
then consider loc being Element of NAT , da being Int-Location such that
A59: INS = da >0_goto loc by SCMFSA_2:61;
A60: IncAddr (INS,k) = da >0_goto (loc + k) by A59, Th16;
A61: now
let d be Int-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d
thus (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A59, SCMFSA_2:97
.= s . d by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A60, SCMFSA_2:97
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ; :: thesis: verum
end;
A62: now
per cases ( s . da > 0 or s . da <= 0 ) ;
suppose A63: s . da > 0 ; :: thesis: IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)))
then A64: IC (Exec ((IncAddr (INS,k)),s)) = loc + k by A60, SCMFSA_2:97;
(s +* (Start-At (((IC s) -' k),SCM+FSA))) . da > 0 by A63, SCMFSA_3:11;
then IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = loc by A59, SCMFSA_2:97
.= (IC (Exec ((IncAddr (INS,k)),s))) -' k by A64, NAT_D:34
.= IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) by FUNCT_4:121 ;
hence IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) ; :: thesis: verum
end;
suppose A65: s . da <= 0 ; :: thesis: IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)))
then (s +* (Start-At (((IC s) -' k),SCM+FSA))) . da <= 0 by SCMFSA_3:11;
then IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = succ (IC (s +* (Start-At (((IC s) -' k),SCM+FSA)))) by A59, SCMFSA_2:97
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec ((IncAddr (INS,k)),s))) -' k by A60, A65, SCMFSA_2:97
.= IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) by FUNCT_4:121 ;
hence IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) ; :: thesis: verum
end;
end;
end;
now
let d be FinSeq-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d
thus (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A59, SCMFSA_2:97
.= s . d by SCMFSA_3:12
.= (Exec ((IncAddr (INS,k)),s)) . d by A60, SCMFSA_2:97
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:12 ; :: thesis: verum
end;
hence Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)) by A1, A62, A61, SCMFSA_2:86; :: thesis: verum
end;
suppose InsCode INS = 9 ; :: thesis: Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
then consider db, da being Int-Location , f being FinSeq-Location such that
A66: INS = da := (f,db) by SCMFSA_2:62;
A67: IncAddr (INS,k) = da := (f,db) by A66, Th17;
A68: now
let d be FinSeq-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d
thus (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A66, SCMFSA_2:98
.= s . d by SCMFSA_3:12
.= (Exec ((IncAddr (INS,k)),s)) . d by A67, SCMFSA_2:98
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:12 ; :: thesis: verum
end;
A69: now
let d be Int-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
per cases ( da = d or da <> d ) ;
suppose A70: da = d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
consider m being Element of NAT such that
A71: m = abs (s . db) and
A72: (Exec ((IncAddr (INS,k)),s)) . da = (s . f) /. m by A67, SCMFSA_2:98;
( ex m9 being Element of NAT st
( m9 = abs ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . db) & (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . da = ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . f) /. m9 ) & (s +* (Start-At (((IC s) -' k),SCM+FSA))) . db = s . db ) by A66, SCMFSA_2:98, SCMFSA_3:11;
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s . f) /. m by A70, A71, SCMFSA_3:12
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by A70, A72, SCMFSA_3:11 ;
:: thesis: verum
end;
suppose A73: da <> d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A66, SCMFSA_2:98
.= s . d by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A67, A73, SCMFSA_2:98
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ;
:: thesis: verum
end;
end;
end;
IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = succ (IC (s +* (Start-At (((IC s) -' k),SCM+FSA)))) by A66, SCMFSA_2:98
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec ((IncAddr (INS,k)),s))) -' k by A67, SCMFSA_2:98
.= IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) by FUNCT_4:121 ;
hence Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)) by A1, A68, A69, SCMFSA_2:86; :: thesis: verum
end;
suppose InsCode INS = 10 ; :: thesis: Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
then consider db, da being Int-Location , f being FinSeq-Location such that
A74: INS = (f,db) := da by SCMFSA_2:63;
A75: IncAddr (INS,k) = (f,db) := da by A74, Th18;
A76: now
let d be Int-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d
thus (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A74, SCMFSA_2:99
.= s . d by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A75, SCMFSA_2:99
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ; :: thesis: verum
end;
A77: now
let d be FinSeq-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
per cases ( f = d or f <> d ) ;
suppose A78: f = d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
A79: (s +* (Start-At (((IC s) -' k),SCM+FSA))) . db = s . db by SCMFSA_3:11;
consider m being Element of NAT such that
A80: m = abs (s . db) and
A81: (Exec ((IncAddr (INS,k)),s)) . f = (s . f) +* (m,(s . da)) by A75, SCMFSA_2:99;
( ex m9 being Element of NAT st
( m9 = abs ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . db) & (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . f = ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . f) +* (m9,((s +* (Start-At (((IC s) -' k),SCM+FSA))) . da)) ) & (s +* (Start-At (((IC s) -' k),SCM+FSA))) . da = s . da ) by A74, SCMFSA_2:99, SCMFSA_3:11;
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s . f) +* (m,(s . da)) by A78, A80, A79, SCMFSA_3:12
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by A78, A81, SCMFSA_3:12 ;
:: thesis: verum
end;
suppose A82: f <> d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A74, SCMFSA_2:99
.= s . d by SCMFSA_3:12
.= (Exec ((IncAddr (INS,k)),s)) . d by A75, A82, SCMFSA_2:99
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:12 ;
:: thesis: verum
end;
end;
end;
IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = succ (IC (s +* (Start-At (((IC s) -' k),SCM+FSA)))) by A74, SCMFSA_2:99
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec ((IncAddr (INS,k)),s))) -' k by A75, SCMFSA_2:99
.= IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) by FUNCT_4:121 ;
hence Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)) by A1, A76, A77, SCMFSA_2:86; :: thesis: verum
end;
suppose InsCode INS = 11 ; :: thesis: Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
then consider da being Int-Location , f being FinSeq-Location such that
A83: INS = da :=len f by SCMFSA_2:64;
A84: IncAddr (INS,k) = da :=len f by A83, Th19;
A85: now
let d be FinSeq-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d
thus (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A83, SCMFSA_2:100
.= s . d by SCMFSA_3:12
.= (Exec ((IncAddr (INS,k)),s)) . d by A84, SCMFSA_2:100
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:12 ; :: thesis: verum
end;
A86: now
let d be Int-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
per cases ( da = d or da <> d ) ;
suppose A87: da = d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = len ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . f) by A83, SCMFSA_2:100
.= len (s . f) by SCMFSA_3:12
.= (Exec ((IncAddr (INS,k)),s)) . d by A84, A87, SCMFSA_2:100
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ;
:: thesis: verum
end;
suppose A88: da <> d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A83, SCMFSA_2:100
.= s . d by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A84, A88, SCMFSA_2:100
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ;
:: thesis: verum
end;
end;
end;
IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = succ (IC (s +* (Start-At (((IC s) -' k),SCM+FSA)))) by A83, SCMFSA_2:100
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec ((IncAddr (INS,k)),s))) -' k by A84, SCMFSA_2:100
.= IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) by FUNCT_4:121 ;
hence Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)) by A1, A85, A86, SCMFSA_2:86; :: thesis: verum
end;
suppose InsCode INS = 12 ; :: thesis: Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))
then consider da being Int-Location , f being FinSeq-Location such that
A89: INS = f :=<0,...,0> da by SCMFSA_2:65;
A90: IncAddr (INS,k) = f :=<0,...,0> da by A89, Th20;
A91: now
let d be Int-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d
thus (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A89, SCMFSA_2:101
.= s . d by SCMFSA_3:11
.= (Exec ((IncAddr (INS,k)),s)) . d by A90, SCMFSA_2:101
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:11 ; :: thesis: verum
end;
A92: now
let d be FinSeq-Location ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
per cases ( f = d or f <> d ) ;
suppose A93: f = d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
A94: (s +* (Start-At (((IC s) -' k),SCM+FSA))) . da = s . da by SCMFSA_3:11;
( ex m being Element of NAT st
( m = abs (s . da) & (Exec ((IncAddr (INS,k)),s)) . f = m |-> 0 ) & ex m9 being Element of NAT st
( m9 = abs ((s +* (Start-At (((IC s) -' k),SCM+FSA))) . da) & (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . f = m9 |-> 0 ) ) by A89, A90, SCMFSA_2:101;
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by A93, A94, SCMFSA_3:12; :: thesis: verum
end;
suppose A95: f <> d ; :: thesis: (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . b1 = ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . b1
hence (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) . d = (s +* (Start-At (((IC s) -' k),SCM+FSA))) . d by A89, SCMFSA_2:101
.= s . d by SCMFSA_3:12
.= (Exec ((IncAddr (INS,k)),s)) . d by A90, A95, SCMFSA_2:101
.= ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) . d by SCMFSA_3:12 ;
:: thesis: verum
end;
end;
end;
IC (Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA))))) = succ (IC (s +* (Start-At (((IC s) -' k),SCM+FSA)))) by A89, SCMFSA_2:101
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec ((IncAddr (INS,k)),s))) -' k by A90, SCMFSA_2:101
.= IC ((Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))) by FUNCT_4:121 ;
hence Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA)) by A1, A91, A92, SCMFSA_2:86; :: thesis: verum
end;
end;