Copyright (c) 1997 Association of Mizar Users
environ
vocabulary SCMFSA6A, SCMFSA_2, CARD_1, SCMFSA8B, SCMFSA8A, SCMFSA_4, FUNCT_4,
CAT_1, AMI_3, RELAT_1, BOOLE, AMI_1, AMI_5, FUNCT_1, ARYTM_1, RELOC,
SF_MASTR, SCMFSA7B, UNIALG_2, AMI_2, SCM_1, CARD_3, SCMFSA6B, FUNCOP_1,
SCMFSA_9;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1,
RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, CARD_1, CARD_3, AMI_1, AMI_3, SCM_1,
AMI_5, SCMFSA_2, SCMFSA_4, SCMFSA_5, SCMFSA6A, SF_MASTR, SCMFSA6B,
SCMFSA7B, SCMFSA8A, SCMFSA8B;
constructors NAT_1, AMI_5, SCMFSA_5, SCM_1, SCMFSA6A, SCMFSA6B, SCMFSA8A,
SF_MASTR, SCMFSA8B;
clusters FUNCT_1, PRELAMB, AMI_1, SCMFSA_2, SCMFSA_4, SF_MASTR, SCMFSA6B,
SCMFSA7B, SCMFSA8A, INT_1, RELSET_1, NAT_1, FRAENKEL, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions SCMFSA_4;
theorems TARSKI, NAT_1, FUNCT_1, FUNCT_4, REAL_1, CQC_THE1, AMI_1, SCMFSA_2,
SCMFSA_4, AMI_5, SCM_1, SCMFSA_5, SCMFSA6A, AXIOMS, GRFUNC_1, SF_MASTR,
SCMFSA6B, SCMFSA7B, SCMFSA8A, SCMFSA8B, ZFMISC_1, CQC_LANG, PRE_CIRC,
RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1;
schemes NAT_1, RECDEF_1;
begin
theorem Th1:
for I being Macro-Instruction, a being Int-Location holds
card if=0(a, I ';' Goto insloc 0, SCM+FSA-Stop) = card I + 6
proof
let I be Macro-Instruction, a be Int-Location;
thus
card if=0(a, I ';' Goto insloc 0, SCM+FSA-Stop)
= card (I ';' Goto insloc 0) + 1 +4 by SCMFSA8A:17,SCMFSA8B:14
.= card I + card Goto insloc 0 + 1+4 by SCMFSA6A:61
.= card I + 1+1+4 by SCMFSA8A:29
.= card I + 1+(1+4) by XCMPLX_1:1
.= card I + (1+5) by XCMPLX_1:1
.= card I + 6;
end;
theorem Th2:
for I being Macro-Instruction, a being Int-Location holds
card if>0(a, I ';' Goto insloc 0, SCM+FSA-Stop) = card I + 6
proof
let I be Macro-Instruction, a be Int-Location;
thus
card if>0(a, I ';' Goto insloc 0, SCM+FSA-Stop)
= card (I ';' Goto insloc 0) + 1 +4 by SCMFSA8A:17,SCMFSA8B:15
.= card I + card Goto insloc 0 + 1+4 by SCMFSA6A:61
.= card I + 1+1+4 by SCMFSA8A:29
.= card I + 1+(1+4) by XCMPLX_1:1
.= card I + (1+5) by XCMPLX_1:1
.= card I + 6;
end;
:: WHILE Statement
reserve m, n for Nat;
definition
let a be Int-Location;
let I be Macro-Instruction;
func while=0(a,I) -> Macro-Instruction equals
:Def1:
if=0(a, I ';' Goto insloc 0, SCM+FSA-Stop) +*
( insloc (card I +4) .--> goto insloc 0 );
correctness
proof
set i = insloc (card I +4) .--> goto insloc 0;
set C = if=0(a, I ';' Goto insloc 0, SCM+FSA-Stop);
set P = C +* i;
A1: card C = card I + 6 by Th1;
card I + 4 < card I + 6 by REAL_1:53;
then insloc (card I + 4) in dom C by A1,SCMFSA6A:15;
then A2: {insloc (card I + 4)} c= dom C by ZFMISC_1:37;
A3: dom(P) = dom C \/ dom i by FUNCT_4:def 1
.= dom C \/ {insloc (card I + 4)} by CQC_LANG:5
.= dom C by A2,XBOOLE_1:12;
P is initial
proof let m,n; thus thesis by A3,SCMFSA_4:def 4;
end;
hence thesis;
end;
func while>0(a,I) -> Macro-Instruction equals
:Def2:
if>0(a, I ';' Goto insloc 0, SCM+FSA-Stop) +*
( insloc (card I +4) .--> goto insloc 0 );
correctness
proof
set i = insloc (card I +4) .--> goto insloc 0;
set C = if>0(a, I ';' Goto insloc 0, SCM+FSA-Stop);
set P = C +* i;
A4: card C = card I + 6 by Th2;
card I + 4 < card I + 6 by REAL_1:53;
then insloc (card I + 4) in dom C by A4,SCMFSA6A:15;
then A5: {insloc (card I + 4)} c= dom C by ZFMISC_1:37;
A6: dom(P) = dom C \/ dom i by FUNCT_4:def 1
.= dom C \/ {insloc (card I + 4)} by CQC_LANG:5
.= dom C by A5,XBOOLE_1:12;
P is initial
proof let m,n; thus thesis by A6,SCMFSA_4:def 4;
end;
hence thesis;
end;
end;
theorem Th3:
for I being Macro-Instruction, a being Int-Location holds
card if=0(a,SCM+FSA-Stop,if>0(a,SCM+FSA-Stop,I ';' Goto insloc 0))
= card I + 11
proof
let I be Macro-Instruction, a be Int-Location;
thus
card if=0(a,SCM+FSA-Stop,if>0(a,SCM+FSA-Stop,I ';' Goto insloc 0))
= 1 + card if>0(a,SCM+FSA-Stop,I ';' Goto insloc 0) +4 by SCMFSA8A:17,
SCMFSA8B:14
.= card (I ';' Goto insloc 0) + 1+ 4 + 1+4 by SCMFSA8A:17,SCMFSA8B:15
.= card I + card Goto insloc 0 +1+ 4 + 1+4 by SCMFSA6A:61
.= card I + 1 + 1 +4 + 1 + 4 by SCMFSA8A:29
.= card I + (1 + 1)+4 +1 + 4 by XCMPLX_1:1
.= card I + (2+ 4) +1+ 4 by XCMPLX_1:1
.= card I + (6 + 1) + 4 by XCMPLX_1:1
.= card I + (7 + 4) by XCMPLX_1:1
.= card I + 11;
end;
definition
let a be Int-Location;
let I be Macro-Instruction;
func while<0(a,I) -> Macro-Instruction equals
:Def3:
if=0(a,SCM+FSA-Stop,if>0(a,SCM+FSA-Stop,I ';' Goto insloc 0)) +*
( insloc (card I +4) .--> goto insloc 0 );
correctness
proof
set i = insloc (card I +4) .--> goto insloc 0;
set C = if=0(a,SCM+FSA-Stop,if>0(a,SCM+FSA-Stop,I ';' Goto insloc 0));
set P = C +* i;
A1: card C = card I + 11 by Th3;
card I + 4 < card I + 11 by REAL_1:53;
then insloc (card I + 4) in dom C by A1,SCMFSA6A:15;
then A2: {insloc (card I + 4)} c= dom C by ZFMISC_1:37;
A3: dom(P) = dom C \/ dom i by FUNCT_4:def 1
.= dom C \/ {insloc (card I + 4)} by CQC_LANG:5
.= dom C by A2,XBOOLE_1:12;
P is initial
proof let m,n; thus thesis by A3,SCMFSA_4:def 4;
end;
hence thesis;
end;
end;
theorem Th4:
for I being Macro-Instruction, a being Int-Location holds
card while=0(a,I) = card I + 6
proof
let I be Macro-Instruction, a be Int-Location;
set i = insloc (card I +4) .--> goto insloc 0;
set C = if=0(a, I ';' Goto insloc 0, SCM+FSA-Stop);
set P = C +* i;
A1: card C = card I + 6 by Th1;
card I + 4 < card I + 6 by REAL_1:53;
then insloc (card I + 4) in dom C by A1,SCMFSA6A:15;
then A2: {insloc (card I + 4)} c= dom C by ZFMISC_1:37;
A3: dom(P) = dom C \/ dom i by FUNCT_4:def 1
.= dom C \/ {insloc (card I + 4)} by CQC_LANG:5
.= dom C by A2,XBOOLE_1:12;
thus
card while=0(a,I) = card P by Def1
.= card dom C by A3,PRE_CIRC:21
.= card I + 6 by A1,PRE_CIRC:21;
end;
theorem Th5:
for I being Macro-Instruction, a being Int-Location holds
card while>0(a,I) = card I + 6
proof
let I be Macro-Instruction, a be Int-Location;
set i = insloc (card I +4) .--> goto insloc 0;
set C = if>0(a, I ';' Goto insloc 0, SCM+FSA-Stop);
set P = C +* i;
A1: card C = card I + 6 by Th2;
card I + 4 < card I + 6 by REAL_1:53;
then insloc (card I + 4) in dom C by A1,SCMFSA6A:15;
then A2: {insloc (card I + 4)} c= dom C by ZFMISC_1:37;
A3: dom(P) = dom C \/ dom i by FUNCT_4:def 1
.= dom C \/ {insloc (card I + 4)} by CQC_LANG:5
.= dom C by A2,XBOOLE_1:12;
thus
card while>0(a,I) = card P by Def2
.= card dom C by A3,PRE_CIRC:21
.= card I + 6 by A1,PRE_CIRC:21;
end;
theorem
for I being Macro-Instruction, a being Int-Location holds
card while<0(a,I) = card I + 11
proof
let I be Macro-Instruction, a be Int-Location;
set i = insloc (card I +4) .--> goto insloc 0;
set C = if=0(a,SCM+FSA-Stop,if>0(a,SCM+FSA-Stop,I ';' Goto insloc 0));
set P = C +* i;
A1: card C = card I + 11 by Th3;
card I + 4 < card I + 11 by REAL_1:53;
then insloc (card I + 4) in dom C by A1,SCMFSA6A:15;
then A2: {insloc (card I + 4)} c= dom C by ZFMISC_1:37;
A3: dom(P) = dom C \/ dom i by FUNCT_4:def 1
.= dom C \/ {insloc (card I + 4)} by CQC_LANG:5
.= dom C by A2,XBOOLE_1:12;
thus
card while<0(a,I) = card P by Def3
.= card dom C by A3,PRE_CIRC:21
.= card I + 11 by A1,PRE_CIRC:21;
end;
theorem Th7:
for a being Int-Location, l being Instruction-Location of SCM+FSA holds
a =0_goto l <> halt SCM+FSA
proof
let a be Int-Location;
let l be Instruction-Location of SCM+FSA;
thus thesis by SCMFSA_2:48,124;
end;
theorem Th8:
for a being Int-Location, l being Instruction-Location of SCM+FSA holds
a >0_goto l <> halt SCM+FSA
proof
let a be Int-Location;
let l be Instruction-Location of SCM+FSA;
thus thesis by SCMFSA_2:49,124;
end;
theorem Th9:
for l being Instruction-Location of SCM+FSA holds
goto l <> halt SCM+FSA
proof
let l be Instruction-Location of SCM+FSA;
thus thesis by SCMFSA_2:47,124;
end;
theorem Th10:
for a being Int-Location, I being Macro-Instruction holds
insloc 0 in dom while=0(a,I) &
insloc 1 in dom while=0(a,I) &
insloc 0 in dom while>0(a,I) &
insloc 1 in dom while>0(a,I)
proof
let a be Int-Location;
let I be Macro-Instruction;
set I1= I ';' Goto insloc 0;
set J = SCM+FSA-Stop;
set f = insloc (card I +4) .--> goto insloc 0;
set i = a =0_goto insloc (card J + 3);
while=0(a,I)= if=0(a, I1, J) +* f by Def1;
then dom while=0(a,I) = dom if=0(a,I1,J) \/ dom f by FUNCT_4:def 1;
then A1: dom if=0(a,I1,J) c= dom while=0(a,I) by XBOOLE_1:7;
if=0(a, I1, J)
= i ';' J ';' Goto insloc (card I1 + 1) ';' I1 ';' SCM+FSA-Stop
by SCMFSA8B:def 1
.= i ';' J ';' Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop)
by SCMFSA6A:62
.= i ';' J ';' (Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop))
by SCMFSA6A:62
.= i ';' (J ';' (Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop)))
by SCMFSA6A:66
.= Macro i ';' (J ';' (Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop)))
by SCMFSA6A:def 5;
then dom Macro i c= dom if=0(a,I1,J) by SCMFSA6A:56;
then A2:dom Macro i c= dom while=0(a,I) by A1,XBOOLE_1:1;
dom Macro i = {insloc 0, insloc 1} by SCMFSA7B:4;
then insloc 0 in dom Macro i & insloc 1 in dom Macro i by TARSKI:def 2;
hence insloc 0 in dom while=0(a,I) & insloc 1 in dom while=0(a,I) by A2;
set i = a >0_goto insloc (card J + 3);
while>0(a,I)= if>0(a, I1, J) +* f by Def2;
then dom while>0(a,I) = dom if>0(a,I1,J) \/ dom f by FUNCT_4:def 1;
then A3: dom if>0(a,I1,J) c= dom while>0(a,I) by XBOOLE_1:7;
if>0(a, I1, J)
= i ';' J ';' Goto insloc (card I1 + 1) ';' I1 ';' SCM+FSA-Stop
by SCMFSA8B:def 2
.= i ';' J ';' Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop)
by SCMFSA6A:62
.= i ';' J ';' (Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop))
by SCMFSA6A:62
.= i ';' (J ';' (Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop)))
by SCMFSA6A:66
.= Macro i ';' (J ';' (Goto insloc (card I1 + 1) ';' (I1 ';'
SCM+FSA-Stop))) by SCMFSA6A:def 5;
then dom Macro i c= dom if>0(a,I1,J) by SCMFSA6A:56;
then A4:dom Macro i c= dom while>0(a,I) by A3,XBOOLE_1:1;
dom Macro i = {insloc 0, insloc 1} by SCMFSA7B:4;
then insloc 0 in dom Macro i & insloc 1 in dom Macro i by TARSKI:def 2;
hence thesis by A4;
end;
theorem Th11:
for a being Int-Location, I being Macro-Instruction holds
while=0(a,I).insloc 0 = a =0_goto insloc 4 &
while=0(a,I).insloc 1 = goto insloc 2 &
while>0(a,I).insloc 0 = a >0_goto insloc 4 &
while>0(a,I).insloc 1 = goto insloc 2
proof
let a be Int-Location;
let I be Macro-Instruction;
set I1= I ';' Goto insloc 0;
set J = SCM+FSA-Stop;
set f = insloc (card I +4) .--> goto insloc 0;
set i = a =0_goto insloc (card J + 3);
A1: i <> halt SCM+FSA by Th7;
A2: dom f = {insloc (card I + 4)} by CQC_LANG:5;
insloc 0 <> insloc (card I + 4) by SCMFSA_2:18;
then A3: not insloc 0 in dom f by A2,TARSKI:def 1;
A4: insloc 0 in dom while=0(a,I) by Th10;
while=0(a,I) = if=0(a, I1, J) +* f by Def1;
then A5: dom while=0(a,I) = dom if=0(a,I1,J) \/ dom f by FUNCT_4:def 1;
1 <> card I + 4 by NAT_1:29;
then insloc 1 <> insloc (card I + 4) by SCMFSA_2:18;
then A6: not insloc 1 in dom f by A2,TARSKI:def 1;
A7: insloc 1 in dom while=0(a,I) by Th10;
A8: if=0(a, I1, J)
= i ';' J ';' Goto insloc (card I1 + 1) ';' I1 ';' SCM+FSA-Stop
by SCMFSA8B:def 1
.= i ';' J ';' Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop)
by SCMFSA6A:62
.= i ';' J ';' (Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop))
by SCMFSA6A:62
.= i ';' (J ';' (Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop)))
by SCMFSA6A:66
.= Macro i ';' (J ';' (Goto insloc (card I1 + 1) ';' (I1 ';'
SCM+FSA-Stop))) by SCMFSA6A:def 5;
dom Macro i = {insloc 0, insloc 1} by SCMFSA7B:4;
then A9: insloc 0 in dom Macro i & insloc 1 in dom Macro i by TARSKI:def 2;
thus while=0(a,I).insloc 0 = (if=0(a, I1, J) +* f).insloc 0 by Def1
.=if=0(a,I1,J).insloc 0 by A3,A4,A5,FUNCT_4:def 1
.= (Directed Macro i).insloc 0 by A8,A9,SCMFSA8A:28
.= a =0_goto insloc 4 by A1,SCMFSA7B:7,SCMFSA8A:17;
thus while=0(a,I).insloc 1 = (if=0(a, I1, J) +* f).insloc 1 by Def1
.=if=0(a,I1,J).insloc 1 by A5,A6,A7,FUNCT_4:def 1
.= (Directed Macro i).insloc 1 by A8,A9,SCMFSA8A:28
.= goto insloc 2 by SCMFSA7B:8;
set i = a >0_goto insloc (card J + 3);
A10: i <> halt SCM+FSA by Th8;
A11: insloc 0 in dom while>0(a,I) by Th10;
while>0(a,I) = if>0(a, I1, J) +* f by Def2;
then A12: dom while>0(a,I) = dom if>0(a,I1,J) \/ dom f by FUNCT_4:def 1;
A13: insloc 1 in dom while>0(a,I) by Th10;
A14: if>0(a, I1, J)
= i ';' J ';' Goto insloc (card I1 + 1) ';' I1 ';' SCM+FSA-Stop
by SCMFSA8B:def 2
.= i ';' J ';' Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop)
by SCMFSA6A:62
.= i ';' J ';' (Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop))
by SCMFSA6A:62
.= i ';' (J ';' (Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop)))
by SCMFSA6A:66
.= Macro i ';' (J ';' (Goto insloc (card I1 + 1) ';' (I1 ';'
SCM+FSA-Stop))) by SCMFSA6A:def 5;
dom Macro i = {insloc 0, insloc 1} by SCMFSA7B:4;
then A15: insloc 0 in dom Macro i & insloc 1 in dom Macro i by TARSKI:def 2;
thus while>0(a,I).insloc 0 = (if>0(a, I1, J) +* f).insloc 0 by Def2
.=if>0(a,I1,J).insloc 0 by A3,A11,A12,FUNCT_4:def 1
.= (Directed Macro i).insloc 0 by A14,A15,SCMFSA8A:28
.= a >0_goto insloc 4 by A10,SCMFSA7B:7,SCMFSA8A:17;
thus while>0(a,I).insloc 1 = (if>0(a, I1, J) +* f).insloc 1 by Def2
.=if>0(a,I1,J).insloc 1 by A6,A12,A13,FUNCT_4:def 1
.= (Directed Macro i).insloc 1 by A14,A15,SCMFSA8A:28
.= goto insloc 2 by SCMFSA7B:8;
end;
theorem Th12:
for a being Int-Location, I being Macro-Instruction,k being Nat st
k < 6 holds insloc k in dom while=0(a,I)
proof
let a be Int-Location, I be Macro-Instruction,k be Nat;
assume A1: k < 6;
6 <= card I + 6 by NAT_1:29;
then A2: k < card I + 6 by A1,AXIOMS:22;
card while=0(a,I) = card I + 6 by Th4;
hence thesis by A2,SCMFSA6A:15;
end;
theorem Th13:
for a being Int-Location, I being Macro-Instruction,k being Nat st
k < 6 holds insloc (card I +k) in dom while=0(a,I)
proof
let a be Int-Location, I be Macro-Instruction,k be Nat;
assume k < 6;
then A1: card I + k < card I + 6 by REAL_1:53;
card while=0(a,I) = card I + 6 by Th4;
hence thesis by A1,SCMFSA6A:15;
end;
theorem Th14:
for a being Int-Location, I being Macro-Instruction holds
while=0(a,I).insloc (card I +5) = halt SCM+FSA
proof
let a be Int-Location;
let I be Macro-Instruction;
set I1= I ';' Goto insloc 0;
set J = SCM+FSA-Stop;
set f = insloc (card I +4) .--> goto insloc 0;
set i = a =0_goto insloc (card J + 3);
set c5 = card I + 5;
set Lc5=insloc c5;
A1: dom f = {insloc (card I + 4)} by CQC_LANG:5;
c5 <> card I + 4 by XCMPLX_1:2;
then Lc5 <> insloc (card I + 4) by SCMFSA_2:18;
then A2: not Lc5 in dom f by A1,TARSKI:def 1;
A3: Lc5 in dom while=0(a,I) by Th13;
while=0(a,I) = if=0(a, I1, J) +* f by Def1;
then A4: dom while=0(a,I) = dom if=0(a,I1,J) \/ dom f by FUNCT_4:def 1;
then A5: Lc5 in dom if=0(a,I1,J) by A2,A3,XBOOLE_0:def 2;
set Mi= Macro i ';' J ';' Goto insloc (card I1 + 1) ';' I1;
set J1= SCM+FSA-Stop;
A6: if=0(a, I1, J)
= i ';' J ';' Goto insloc (card I1 + 1) ';' I1 ';' SCM+FSA-Stop
by SCMFSA8B:def 1
.= Mi ';' J1 by SCMFSA6A:def 5;
then card if=0(a, I1,J) = card Mi + card J1 by SCMFSA6A:61;
then A7: card Mi = card if=0(a,I1,J)-card J1 by XCMPLX_1:26
.= card I + 6 - 1 by Th1,SCMFSA8A:17
.= card I + (5+1-1) by XCMPLX_1:29
.= c5;
then A8: not Lc5 in dom Mi by SCMFSA6A:15;
A9: if=0(a, I1, J) = Directed Mi +* ProgramPart Relocated(J1, c5) by A6,A7,
SCMFSA6A:def 4;
then A10: dom if=0(a,I1,J) = dom Directed Mi \/ dom ProgramPart Relocated(J1,
c5)
by FUNCT_4:def 1;
then dom if=0(a,I1,J)
= dom Mi \/ dom ProgramPart Relocated(J1, c5) by SCMFSA6A:14;
then A11: Lc5 in dom ProgramPart Relocated(J1, c5) by A5,A8,XBOOLE_0:def 2;
A12: insloc 0 + c5 = insloc ( 0 + c5) by SCMFSA_4:def 1;
insloc 0 + c5 in { il+c5 where il is Instruction-Location of SCM+FSA:
il in dom J1} by SCMFSA8A:16;
then A13: insloc c5 in dom Shift(J1,c5) by A12,SCMFSA_4:31;
then A14: pi(Shift(J1,c5),Lc5) = Shift(J1,c5).(insloc 0 +c5) by A12,AMI_5:def 5
.= halt SCM+FSA by SCMFSA8A:16,SCMFSA_4:30;
thus while=0(a,I).Lc5 = (if=0(a, I1, J) +* f).Lc5 by Def1
.= (Directed Mi +* ProgramPart Relocated(J1, c5)).Lc5 by A2,A3,A4,A9,FUNCT_4
:def 1
.= (ProgramPart Relocated(J1,c5)).Lc5 by A5,A10,A11,FUNCT_4:def 1
.= IncAddr(Shift(ProgramPart(J1),c5),c5).Lc5 by SCMFSA_5:2
.= IncAddr(Shift(J1,c5),c5).Lc5 by AMI_5:72
.= IncAddr( halt SCM+FSA, c5 ) by A13,A14,SCMFSA_4:24
.= halt SCM+FSA by SCMFSA_4:8;
end;
theorem Th15:
for a being Int-Location, I being Macro-Instruction holds
while=0(a,I).insloc 3 = goto insloc (card I +5)
proof
let a be Int-Location;
let I be Macro-Instruction;
set I1= I ';' Goto insloc 0;
set J = SCM+FSA-Stop;
set f = insloc (card I +4) .--> goto insloc 0;
set i = a =0_goto insloc (card J + 3);
A1: dom f = {insloc (card I + 4)} by CQC_LANG:5;
3 <> card I + 4 by NAT_1:29;
then insloc 3 <> insloc (card I + 4) by SCMFSA_2:18;
then A2: not insloc 3 in dom f by A1,TARSKI:def 1;
A3: insloc 3 in dom while=0(a,I) by Th12;
while=0(a,I) = if=0(a, I1, J) +* f by Def1;
then A4: dom while=0(a,I) = dom if=0(a,I1,J) \/ dom f by FUNCT_4:def 1;
then A5: insloc 3 in dom if=0(a,I1,J) by A2,A3,XBOOLE_0:def 2;
set Mi=Macro i ';' J;
set G=Goto insloc (card I1 + 1);
set J2= (I1 ';' SCM+FSA-Stop);
set J1=G ';' J2;
A6: card Mi = card Macro i + card J by SCMFSA6A:61
.= 2 + 1 by SCMFSA7B:6,SCMFSA8A:17;
then A7: not insloc 3 in dom Mi by SCMFSA6A:15;
A8: if=0(a, I1, J)
= i ';' J ';' Goto insloc (card I1 + 1) ';' I1 ';' SCM+FSA-Stop
by SCMFSA8B:def 1
.= i ';' J ';' Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop)
by SCMFSA6A:62
.= i ';' J ';' J1 by SCMFSA6A:62
.= Mi ';' J1 by SCMFSA6A:def 5
.= Directed Mi +* ProgramPart Relocated(J1, 3) by A6,SCMFSA6A:def 4;
then A9: dom if=0(a,I1,J) = dom Directed Mi \/ dom ProgramPart Relocated(J1, 3)
by FUNCT_4:def 1;
then dom if=0(a,I1,J)
= dom Mi \/ dom ProgramPart Relocated(J1, 3) by SCMFSA6A:14;
then A10: insloc 3 in dom ProgramPart Relocated(J1, 3) by A5,A7,XBOOLE_0:def 2;
A11: insloc 0 in dom G by SCMFSA8A:47;
A12: G.insloc 0 = goto insloc (card I1 + 1) by SCMFSA8A:47
.= goto insloc (card I + card Goto insloc 0 + 1) by SCMFSA6A:61
.= goto insloc (card I + 1 + 1) by SCMFSA8A:29
.= goto insloc (card I +(1+1)) by XCMPLX_1:1;
then A13: G.insloc 0 <> halt SCM+FSA by Th9;
A14: insloc 0 + 3 = insloc ( 0 + 3) by SCMFSA_4:def 1;
J1= Directed G +* ProgramPart Relocated(J2, card G) by SCMFSA6A:def 4;
then dom J1 = dom Directed G \/ dom ProgramPart Relocated(J2, card G)
by FUNCT_4:def 1
.= dom G \/ dom ProgramPart Relocated(J2, card G) by SCMFSA6A:14;
then A15: insloc 0 in dom J1 by A11,XBOOLE_0:def 2;
then insloc 0 + 3 in { il+3 where il is Instruction-Location of SCM+FSA:
il in dom J1};
then A16: insloc 3 in dom Shift(J1,3) by A14,SCMFSA_4:31;
then A17: pi(Shift(J1,3),insloc 3) =Shift(J1,3).(insloc 0 +3) by A14,AMI_5:def
5
.=J1.insloc 0 by A15,SCMFSA_4:30
.=(Directed G).insloc 0 by A11,SCMFSA8A:28
.=goto insloc (card I + 2) by A11,A12,A13,SCMFSA8A:30;
thus while=0(a,I).insloc 3 = (if=0(a, I1, J) +* f).insloc 3 by Def1
.= (Directed Mi +* ProgramPart Relocated(J1, 3)).insloc 3 by A2,A3,A4,A8,
FUNCT_4:def 1
.= (ProgramPart Relocated(J1,3)).insloc 3 by A5,A9,A10,FUNCT_4:def 1
.= IncAddr(Shift(ProgramPart(J1),3),3).insloc 3 by SCMFSA_5:2
.= IncAddr(Shift(J1,3),3).insloc 3 by AMI_5:72
.= IncAddr(goto insloc (card I +2),3) by A16,A17,SCMFSA_4:24
.= goto (insloc (card I +2) + 3) by SCMFSA_4:14
.= goto insloc (card I+ 2 +3) by SCMFSA_4:def 1
.= goto insloc (card I+ (2 +3)) by XCMPLX_1:1
.= goto insloc (card I+ 5);
end;
theorem Th16:
for a being Int-Location, I being Macro-Instruction holds
while=0(a,I).insloc 2 = goto insloc 3
proof
let a be Int-Location;
let I be Macro-Instruction;
set I1= I ';' Goto insloc 0;
set J = SCM+FSA-Stop;
set f = insloc (card I +4) .--> goto insloc 0;
set i = a =0_goto insloc (card J + 3);
A1: dom f = {insloc (card I + 4)} by CQC_LANG:5;
2 <> card I + 4 by NAT_1:29;
then insloc 2 <> insloc (card I + 4) by SCMFSA_2:18;
then A2: not insloc 2 in dom f by A1,TARSKI:def 1;
A3: insloc 2 in dom while=0(a,I) by Th12;
while=0(a,I) = if=0(a, I1, J) +* f by Def1;
then A4: dom while=0(a,I) = dom if=0(a,I1,J) \/ dom f by FUNCT_4:def 1;
then A5: insloc 2 in dom if=0(a,I1,J) by A2,A3,XBOOLE_0:def 2;
set Mi=Macro i;
set J2=Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop);
set J1=J ';' J2;
A6: card Mi = 2 by SCMFSA7B:6;
then A7: not insloc 2 in dom Mi by SCMFSA6A:15;
A8: if=0(a, I1, J)
= i ';' J ';' Goto insloc (card I1 + 1) ';' I1 ';' SCM+FSA-Stop
by SCMFSA8B:def 1
.= i ';' J ';' Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop)
by SCMFSA6A:62
.= i ';' J ';' (Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop))
by SCMFSA6A:62
.= i ';' J1 by SCMFSA6A:66
.= Mi ';' J1 by SCMFSA6A:def 5
.= Directed Mi +* ProgramPart Relocated(J1, 2) by A6,SCMFSA6A:def 4;
then A9: dom if=0(a,I1,J) = dom Directed Mi \/ dom ProgramPart Relocated(J1, 2)
by FUNCT_4:def 1;
then dom if=0(a,I1,J)
= dom Mi \/ dom ProgramPart Relocated(J1, 2) by SCMFSA6A:14;
then A10: insloc 2 in dom ProgramPart Relocated(J1, 2) by A5,A7,XBOOLE_0:def 2;
A11: insloc 0 + 2 = insloc ( 0 + 2) by SCMFSA_4:def 1;
J1= Directed J +* ProgramPart Relocated(J2, card J) by SCMFSA6A:def 4;
then dom J1 = dom Directed J \/ dom ProgramPart Relocated(J2, card J)
by FUNCT_4:def 1
.= dom J \/ dom ProgramPart Relocated(J2, card J) by SCMFSA6A:14;
then A12: insloc 0 in dom J1 by SCMFSA8A:16,XBOOLE_0:def 2;
then insloc 0 + 2 in { il+2 where il is Instruction-Location of SCM+FSA:
il in dom J1};
then A13: insloc 2 in dom Shift(J1,2) by A11,SCMFSA_4:31;
then A14: pi(Shift(J1,2),insloc 2) =Shift(J1,2).(insloc 0 +2) by A11,AMI_5:def
5
.=J1.insloc 0 by A12,SCMFSA_4:30
.=(Directed J).insloc 0 by SCMFSA8A:16,28
.=goto insloc card J by SCMFSA8A:16,30;
thus while=0(a,I).insloc 2 = (if=0(a, I1, J) +* f).insloc 2 by Def1
.= (Directed Mi +* ProgramPart Relocated(J1, 2)).insloc 2 by A2,A3,A4,A8,
FUNCT_4:def 1
.= (ProgramPart Relocated(J1,2)).insloc 2 by A5,A9,A10,FUNCT_4:def 1
.= IncAddr(Shift(ProgramPart(J1),2),2).insloc 2 by SCMFSA_5:2
.= IncAddr(Shift(J1,2),2).insloc 2 by AMI_5:72
.= IncAddr(goto insloc card J,2) by A13,A14,SCMFSA_4:24
.= goto (insloc 1 + 2) by SCMFSA8A:17,SCMFSA_4:14
.= goto insloc (1+2) by SCMFSA_4:def 1
.= goto insloc 3;
end;
theorem
for a being Int-Location, I being Macro-Instruction,k being Nat st
k < card I +6 holds insloc k in dom while=0(a,I)
proof
let a be Int-Location, I be Macro-Instruction,k be Nat;
assume A1: k < card I +6;
card while=0(a,I) = card I + 6 by Th4;
hence thesis by A1,SCMFSA6A:15;
end;
theorem Th18:
for s being State of SCM+FSA, I being Macro-Instruction,
a being read-write Int-Location st s.a <> 0 holds
while=0(a,I) is_halting_on s & while=0(a,I) is_closed_on s
proof
let s be State of SCM+FSA;
let I be Macro-Instruction;
let a be read-write Int-Location;
assume A1: s.a <> 0;
set s1 = s +* (while=0(a,I) +* Start-At insloc 0);
set s2 = (Computation s1).1;
set s3 = (Computation s1).2;
set s4 = (Computation s1).3;
set s5 = (Computation s1).4;
set C1 = Computation s1;
set i = a =0_goto insloc 4;
A2: insloc 0 in dom while=0(a,I) by Th10;
while=0(a,I) c= while=0(a,I) +* Start-At insloc 0 by SCMFSA8A:9;
then A3: dom while=0(a,I) c= dom (while=0(a,I) +* Start-At insloc 0)
by GRFUNC_1:8;
A4: IC SCM+FSA in dom (while=0(a,I) +* Start-At insloc 0) by SF_MASTR:65;
A5: IC s1 = s1.IC SCM+FSA by AMI_1:def 15
.= (while=0(a,I) +* Start-At insloc 0).IC SCM+FSA by A4,FUNCT_4:14
.= insloc 0 by SF_MASTR:66;
s1.insloc 0 = (while=0(a,I) +* Start-At insloc 0).insloc 0
by A2,A3,FUNCT_4:14
.= while=0(a,I).insloc 0 by A2,SCMFSA6B:7
.= i by Th11;
then A6: CurInstr s1 = i by A5,AMI_1:def 17;
A7: (Computation s1).(0 + 1) = Following (Computation s1).0 by AMI_1:def 19
.= Following s1 by AMI_1:def 19
.= Exec(i,s1) by A6,AMI_1:def 18;
not a in dom (while=0(a,I) +* Start-At insloc 0) & a in dom s
by SCMFSA6B:12,SCMFSA_2:66;
then A8: s1.a = s.a by FUNCT_4:12;
A9: IC C1.1 = C1.1.IC SCM+FSA by AMI_1:def 15
.= Next insloc 0 by A1,A5,A7,A8,SCMFSA_2:96
.= insloc (0 + 1) by SCMFSA_2:32;
A10: insloc 1 in dom while=0(a,I) by Th10;
C1.1.insloc 1 = s1.insloc 1 by AMI_1:54
.= (while=0(a,I) +* Start-At insloc 0).insloc 1 by A3,A10,FUNCT_4:14
.= while=0(a,I).insloc 1 by A10,SCMFSA6B:7
.= goto insloc 2 by Th11;
then A11: CurInstr C1.1 = goto insloc 2 by A9,AMI_1:def 17;
A12: (Computation s1).(1 + 1) = Following s2 by AMI_1:def 19
.= Exec(goto insloc 2,s2) by A11,AMI_1:def 18;
A13: insloc 2 in dom while=0(a,I) by Th12;
A14: IC s3 = s3.IC SCM+FSA by AMI_1:def 15
.= insloc 2 by A12,SCMFSA_2:95;
s3.insloc 2 = s1.insloc 2 by AMI_1:54
.= (while=0(a,I) +* Start-At insloc 0).insloc 2 by A3,A13,FUNCT_4:14
.= while=0(a,I).insloc 2 by A13,SCMFSA6B:7
.= goto insloc 3 by Th16;
then A15: CurInstr s3 = goto insloc 3 by A14,AMI_1:def 17;
A16: (Computation s1).(2 + 1) = Following s3 by AMI_1:def 19
.= Exec(goto insloc 3,s3) by A15,AMI_1:def 18;
A17: insloc 3 in dom while=0(a,I) by Th12;
set loc5= insloc (card I +5);
A18: IC s4 = s4.IC SCM+FSA by AMI_1:def 15
.= insloc 3 by A16,SCMFSA_2:95;
s4.insloc 3 = s1.insloc 3 by AMI_1:54
.= (while=0(a,I) +* Start-At insloc 0).insloc 3 by A3,A17,FUNCT_4:14
.= while=0(a,I).insloc 3 by A17,SCMFSA6B:7
.= goto loc5 by Th15;
then A19: CurInstr s4 = goto loc5 by A18,AMI_1:def 17;
A20: (Computation s1).(3 + 1) = Following s4 by AMI_1:def 19
.= Exec(goto loc5,s4) by A19,AMI_1:def 18;
A21: loc5 in dom while=0(a,I) by Th13;
A22: IC s5 = s5.IC SCM+FSA by AMI_1:def 15
.= loc5 by A20,SCMFSA_2:95;
s5.loc5 = s1.loc5 by AMI_1:54
.= (while=0(a,I) +* Start-At insloc 0).loc5 by A3,A21,FUNCT_4:14
.= while=0(a,I).loc5 by A21,SCMFSA6B:7
.= halt SCM+FSA by Th14;
then A23: CurInstr s5 = halt SCM+FSA by A22,AMI_1:def 17;
then s1 is halting by AMI_1:def 20;
hence while=0(a,I) is_halting_on s by SCMFSA7B:def 8;
now let k be Nat;
A24: k<=3 or k >= 3+1 by NAT_1:38;
per cases by A24,CQC_THE1:4;
suppose k = 0;
hence IC C1.k in dom while=0(a,I) by A2,A5,AMI_1:def 19;
suppose k = 1;
hence IC C1.k in dom while=0(a,I) by A9,Th10;
suppose k = 2;
hence IC C1.k in dom while=0(a,I) by A14,Th12;
suppose k = 3;
hence IC C1.k in dom while=0(a,I) by A18,Th12;
suppose k >= 4;
hence IC C1.k in dom while=0(a,I) by A21,A22,A23,AMI_1:52;
end;
hence while=0(a,I) is_closed_on s by SCMFSA7B:def 7;
end;
theorem Th19:
for a being Int-Location, I being Macro-Instruction,
s being State of SCM+FSA,k being Nat st
I is_closed_on s & I is_halting_on s &
k < LifeSpan (s +* (I +* Start-At insloc 0)) &
IC (Computation (s +* (while=0(a,I) +* Start-At insloc 0))).(1 + k) =
IC (Computation (s +* ( I +* Start-At insloc 0))).k + 4 &
(Computation (s +* (while=0(a,I) +* Start-At insloc 0))).(1 + k) |
(Int-Locations \/ FinSeq-Locations) =
(Computation (s +* ( I +* Start-At insloc 0))).k |
(Int-Locations \/ FinSeq-Locations) holds
IC (Computation (s +* (while=0(a,I) +* Start-At insloc 0))).(1 + k+1) =
IC (Computation (s +* (I +* Start-At insloc 0))).(k+1) + 4 &
(Computation (s +* (while=0(a,I) +* Start-At insloc 0))).(1 + k+1) |
(Int-Locations \/ FinSeq-Locations) =
(Computation (s +* (I +* Start-At insloc 0))).(k+1) |
(Int-Locations \/ FinSeq-Locations)
proof
set D = Int-Locations \/ FinSeq-Locations;
let a be Int-Location;
let I be Macro-Instruction;
let s be State of SCM+FSA;
let k be Nat;
set s1 = s +* (while=0(a,I) +* Start-At insloc 0);
set sI = s +* ( I +* Start-At insloc 0);
set sK1=(Computation s1).(1 + k);
set sK2= (Computation sI).k;
set l3=IC (Computation sI).k;
assume A1: I is_closed_on s;
assume A2: I is_halting_on s;
assume A3: k < LifeSpan sI;
assume A4: IC (Computation s1).(1 + k)=l3 + 4;
assume A5:sK1 | D = sK2 | D;
set I1= I ';' Goto insloc 0;
set J = SCM+FSA-Stop;
set f = insloc (card I +4) .--> goto insloc 0;
set i = a =0_goto insloc (card J + 3);
A6: dom f = {insloc (card I + 4)} by CQC_LANG:5;
consider n being Nat such that A7: l3 = insloc n by SCMFSA_2:21;
A8: insloc n in dom I by A1,A7,SCMFSA7B:def 7;
then A9: n < card I by SCMFSA6A:15;
then n + 4 <> card I + 4 by XCMPLX_1:2;
then insloc (n + 4) <> insloc (card I + 4) by SCMFSA_2:18;
then A10: not insloc (n+4) in dom f by A6,TARSKI:def 1;
A11: n+4 < card I+ 6 by A9,REAL_1:67;
card while=0(a,I) = card I + 6 by Th4;
then A12: insloc (n+4) in dom while=0(a,I) by A11,SCMFSA6A:15;
while=0(a,I) = if=0(a, I1, J) +* f by Def1;
then A13: dom while=0(a,I) = dom if=0(a,I1,J) \/ dom f by FUNCT_4:def 1;
then A14: insloc (n+4) in dom if=0(a,I1,J) by A10,A12,XBOOLE_0:def 2;
set Mi= i ';' J ';' Goto insloc (card I1 + 1);
set J2= I1 ';' SCM+FSA-Stop;
set J3= Goto insloc 0 ';' SCM+FSA-Stop;
A15: card Mi = card (i ';' J )+ card Goto insloc (card I1 + 1) by SCMFSA6A:61
.= card (i ';' J ) + 1 by SCMFSA8A:29
.= card (Macro i ';' J) + 1 by SCMFSA6A:def 5
.= card (Macro i) + card J + 1 by SCMFSA6A:61
.= 2 + 1 +1 by SCMFSA7B:6,SCMFSA8A:17
.= 3+ 1;
then n+4 >= card Mi by NAT_1:29;
then A16: not insloc (n+4) in dom Mi by SCMFSA6A:15;
A17: if=0(a, I1, J)
= Mi ';' I1 ';' SCM+FSA-Stop by SCMFSA8B:def 1
.= Mi ';' J2 by SCMFSA6A:62
.= Directed Mi +* ProgramPart Relocated(J2, 4) by A15,SCMFSA6A:def 4;
then A18: dom if=0(a,I1,J) = dom Directed Mi \/ dom ProgramPart Relocated(J2, 4
)
by FUNCT_4:def 1;
then dom if=0(a,I1,J)
= dom Mi \/ dom ProgramPart Relocated(J2, 4) by SCMFSA6A:14;
then A19: insloc (n+4) in dom ProgramPart Relocated(J2, 4) by A14,A16,XBOOLE_0:
def 2
;
A20: insloc n + 4 = insloc ( n + 4) by SCMFSA_4:def 1;
while=0(a,I) c= while=0(a,I) +* Start-At insloc 0 by SCMFSA8A:9;
then A21: dom while=0(a,I) c= dom (while=0(a,I) +* Start-At insloc 0)
by GRFUNC_1:8;
I c= I +* Start-At insloc 0 by SCMFSA8A:9;
then A22: dom I c= dom (I +* Start-At insloc 0) by GRFUNC_1:8;
A23: CurInstr sK2 =sK2.insloc n by A7,AMI_1:def 17
.=sI.insloc n by AMI_1:54
.=(I +* Start-At insloc 0).insloc n by A8,A22,FUNCT_4:14
.= I.insloc n by A8,SCMFSA6B:7;
sI is halting by A2,SCMFSA7B:def 8;
then A24: I.insloc n <> halt SCM+FSA by A3,A23,SCM_1:def 2;
A25: J2= I ';' J3 by SCMFSA6A:62;
then J2= Directed I +* ProgramPart Relocated(J3, card I) by SCMFSA6A:def 4
;
then dom J2 = dom Directed I \/ dom ProgramPart Relocated(J3, card I)
by FUNCT_4:def 1
.= dom I \/ dom ProgramPart Relocated(J3, card I) by SCMFSA6A:14;
then A26: insloc n in dom J2 by A8,XBOOLE_0:def 2;
then insloc n + 4 in { il+4 where il is Instruction-Location of SCM+FSA:
il in dom J2};
then A27: insloc (n+4) in dom Shift(J2,4) by A20,SCMFSA_4:31;
then A28: pi(Shift(J2,4),insloc (n+4)) =Shift(J2,4).(insloc n +4) by A20,AMI_5:
def 5
.=J2.insloc n by A26,SCMFSA_4:30
.=(Directed I).insloc n by A8,A25,SCMFSA8A:28
.=I.insloc n by A8,A24,SCMFSA8A:30;
A29: I.insloc n in rng I by A8,FUNCT_1:def 5;
rng I c= the Instructions of SCM+FSA by SCMFSA_4:1;
then reconsider j = I.insloc n as Instruction of SCM+FSA by A29;
sK1.insloc (n+4) = s1.insloc(n+4) by AMI_1:54
.= (while=0(a,I) +* Start-At insloc 0).insloc (n+4) by A12,A21,FUNCT_4:14
.= while=0(a,I).insloc (n+4) by A12,SCMFSA6B:7
.= (if=0(a, I1, J) +* f).insloc (n+4) by Def1
.= (Directed Mi +* ProgramPart Relocated(J2, 4)).insloc (n+4) by A10,A12,
A13,A17,FUNCT_4:def 1
.= (ProgramPart Relocated(J2,4)).insloc (n+4) by A14,A18,A19,FUNCT_4:def 1
.= IncAddr(Shift(ProgramPart(J2),4),4).insloc (n+4) by SCMFSA_5:2
.= IncAddr(Shift(J2,4),4).insloc (n+4) by AMI_5:72
.= IncAddr(j,4) by A27,A28,SCMFSA_4:24;
then A30: CurInstr sK1 =IncAddr(j,4) by A4,A7,A20,AMI_1:def 17;
A31: (Computation s1).(1 + k+1) = Following sK1 by AMI_1:def 19
.= Exec(IncAddr(j,4),sK1) by A30,AMI_1:def 18;
(Computation sI).(k+1) = Following sK2 by AMI_1:def 19
.= Exec(j,sK2) by A23,AMI_1:def 18;
hence thesis by A4,A5,A31,SCMFSA6A:41;
end;
theorem Th20:
for a being Int-Location, I being Macro-Instruction,
s being State of SCM+FSA st
I is_closed_on s & I is_halting_on s &
IC (Computation (s +* (while=0(a,I) +* Start-At insloc 0))).(1 +
LifeSpan (s +* (I +* Start-At insloc 0 ) ) ) =
IC (Computation (s +* ( I +* Start-At insloc 0))).
LifeSpan (s +* (I +* Start-At insloc 0 ) ) + 4
holds
CurInstr (Computation (s +* (while=0(a,I) +* Start-At insloc 0))).(1 +
LifeSpan (s +* (I +* Start-At insloc 0)) ) = goto insloc (card I +4)
proof
let a be Int-Location;
let I be Macro-Instruction;
let s be State of SCM+FSA;
set s1 = s +* (while=0(a,I) +* Start-At insloc 0);
set sI = s +* ( I +* Start-At insloc 0);
set life=LifeSpan (s +* (I +* Start-At insloc 0));
set sK1=(Computation s1).(1 + life);
set sK2= (Computation sI).life;
assume A1: I is_closed_on s;
assume A2: I is_halting_on s;
assume A3: IC sK1 = IC sK2 + 4;
set I1= I ';' Goto insloc 0;
set J = SCM+FSA-Stop;
set f = insloc (card I +4) .--> goto insloc 0;
set i = a =0_goto insloc (card J + 3);
A4: dom f = {insloc (card I + 4)} by CQC_LANG:5;
consider n being Nat such that A5: IC sK2 = insloc n by SCMFSA_2:21;
A6: insloc n in dom I by A1,A5,SCMFSA7B:def 7;
then A7: n < card I by SCMFSA6A:15;
then n + 4 <> card I + 4 by XCMPLX_1:2;
then insloc (n + 4) <> insloc (card I + 4) by SCMFSA_2:18;
then A8: not insloc (n+4) in dom f by A4,TARSKI:def 1;
A9: n+4 < card I+ 6 by A7,REAL_1:67;
card while=0(a,I) = card I + 6 by Th4;
then A10: insloc (n+4) in dom while=0(a,I) by A9,SCMFSA6A:15;
while=0(a,I) = if=0(a, I1, J) +* f by Def1;
then A11: dom while=0(a,I) = dom if=0(a,I1,J) \/ dom f by FUNCT_4:def 1;
then A12: insloc (n+4) in dom if=0(a,I1,J) by A8,A10,XBOOLE_0:def 2;
set Mi= i ';' J ';' Goto insloc (card I1 + 1);
set J2= I1 ';' SCM+FSA-Stop;
set J3= Goto insloc 0 ';' SCM+FSA-Stop;
A13: card Mi = card (i ';' J )+ card Goto insloc (card I1 + 1) by SCMFSA6A:61
.= card (i ';' J ) + 1 by SCMFSA8A:29
.= card (Macro i ';' J) + 1 by SCMFSA6A:def 5
.= card (Macro i) + card J + 1 by SCMFSA6A:61
.= 2 + 1 +1 by SCMFSA7B:6,SCMFSA8A:17
.= 3+ 1;
then n+4 >= card Mi by NAT_1:29;
then A14: not insloc (n+4) in dom Mi by SCMFSA6A:15;
A15: if=0(a, I1, J)
= Mi ';' I1 ';' SCM+FSA-Stop by SCMFSA8B:def 1
.= Mi ';' J2 by SCMFSA6A:62
.= Directed Mi +* ProgramPart Relocated(J2, 4) by A13,SCMFSA6A:def 4;
then A16: dom if=0(a,I1,J) = dom Directed Mi \/ dom ProgramPart Relocated(J2, 4
)
by FUNCT_4:def 1;
then dom if=0(a,I1,J)
= dom Mi \/ dom ProgramPart Relocated(J2, 4) by SCMFSA6A:14;
then A17: insloc (n+4) in dom ProgramPart Relocated(J2, 4) by A12,A14,XBOOLE_0:
def 2
;
A18: insloc n + 4 = insloc ( n + 4) by SCMFSA_4:def 1;
while=0(a,I) c= while=0(a,I) +* Start-At insloc 0 by SCMFSA8A:9;
then A19: dom while=0(a,I) c= dom (while=0(a,I) +* Start-At insloc 0)
by GRFUNC_1:8;
I c= I +* Start-At insloc 0 by SCMFSA8A:9;
then A20: dom I c= dom (I +* Start-At insloc 0) by GRFUNC_1:8;
A21: CurInstr sK2 =sK2.insloc n by A5,AMI_1:def 17
.=sI.insloc n by AMI_1:54
.=(I +* Start-At insloc 0).insloc n by A6,A20,FUNCT_4:14
.= I.insloc n by A6,SCMFSA6B:7;
sI is halting by A2,SCMFSA7B:def 8;
then A22: I.insloc n = halt SCM+FSA by A21,SCM_1:def 2;
A23: J2= I ';' J3 by SCMFSA6A:62;
then J2= Directed I +* ProgramPart Relocated(J3, card I) by SCMFSA6A:def 4
;
then dom J2 = dom Directed I \/ dom ProgramPart Relocated(J3, card I)
by FUNCT_4:def 1
.= dom I \/ dom ProgramPart Relocated(J3, card I) by SCMFSA6A:14;
then A24: insloc n in dom J2 by A6,XBOOLE_0:def 2;
then insloc n + 4 in { il+4 where il is Instruction-Location of SCM+FSA:
il in dom J2};
then A25: insloc (n+4) in dom Shift(J2,4) by A18,SCMFSA_4:31;
then A26: pi(Shift(J2,4),insloc (n+4)) =Shift(J2,4).(insloc n +4) by A18,AMI_5:
def 5
.=J2.insloc n by A24,SCMFSA_4:30
.=(Directed I).insloc n by A6,A23,SCMFSA8A:28
.=goto insloc card I by A6,A22,SCMFSA8A:30;
sK1.insloc (n+4) = s1.insloc(n+4) by AMI_1:54
.= (while=0(a,I) +* Start-At insloc 0).insloc (n+4) by A10,A19,FUNCT_4:14
.= while=0(a,I).insloc (n+4) by A10,SCMFSA6B:7
.= (if=0(a, I1, J) +* f).insloc (n+4) by Def1
.= (Directed Mi +* ProgramPart Relocated(J2, 4)).insloc (n+4) by A8,A10,A11
,A15,FUNCT_4:def 1
.= (ProgramPart Relocated(J2,4)).insloc (n+4) by A12,A16,A17,FUNCT_4:def 1
.= IncAddr(Shift(ProgramPart(J2),4),4).insloc (n+4) by SCMFSA_5:2
.= IncAddr(Shift(J2,4),4).insloc (n+4) by AMI_5:72
.= IncAddr(goto insloc card I,4) by A25,A26,SCMFSA_4:24
.= goto (insloc card I+4) by SCMFSA_4:14
.= goto insloc (card I+4) by SCMFSA_4:def 1;
hence thesis by A3,A5,A18,AMI_1:def 17;
end;
theorem Th21:
for a being Int-Location, I being Macro-Instruction holds
while=0(a,I).insloc (card I +4) = goto insloc 0
proof
let a be Int-Location;
let I be Macro-Instruction;
set I1= I ';' Goto insloc 0;
set J = SCM+FSA-Stop;
set f = insloc (card I +4) .--> goto insloc 0;
set Lc4=insloc (card I + 4 );
dom f = {Lc4} by CQC_LANG:5;
then A1: Lc4 in dom f by TARSKI:def 1;
A2: Lc4 in dom while=0(a,I) by Th13;
while=0(a,I) = if=0(a, I1, J) +* f by Def1;
then A3: dom while=0(a,I) = dom if=0(a,I1,J) \/ dom f by FUNCT_4:def 1;
thus while=0(a,I).Lc4 = (if=0(a, I1, J) +* f).Lc4 by Def1
.= f.Lc4 by A1,A2,A3,FUNCT_4:def 1
.=goto insloc 0 by CQC_LANG:6;
end;
reserve f for FinSeq-Location,
c for Int-Location;
theorem Th22:
for s being State of SCM+FSA, I being Macro-Instruction,
a being read-write Int-Location
st I is_closed_on s & I is_halting_on s & s.a =0 holds
IC (Computation (s +* (while=0(a,I) +* Start-At insloc 0))).
(LifeSpan (s +* (I +* Start-At insloc 0)) + 3) = insloc 0 &
for k being Nat st k <= LifeSpan (s +* (I +* Start-At insloc 0)) + 3
holds IC (Computation (s +* (while=0(a,I) +* Start-At insloc 0))).k
in dom while=0(a,I)
proof
let s be State of SCM+FSA;
let I be Macro-Instruction;
let a be read-write Int-Location;
assume A1: I is_closed_on s;
assume A2: I is_halting_on s;
assume A3: s.a = 0;
set D = Int-Locations \/ FinSeq-Locations;
set s1 = s +* (while=0(a,I) +* Start-At insloc 0);
set s2 = (Computation s1).1;
set C1 = Computation s1;
set i = a =0_goto insloc 4;
set sI = s +* (I +* Start-At insloc 0);
A4: insloc 0 in dom while=0(a,I) by Th10;
while=0(a,I) c= while=0(a,I) +* Start-At insloc 0 by SCMFSA8A:9;
then A5: dom while=0(a,I) c= dom (while=0(a,I) +* Start-At insloc 0)
by GRFUNC_1:8;
A6: IC SCM+FSA in dom (while=0(a,I) +* Start-At insloc 0) by SF_MASTR:65;
A7: IC s1 = s1.IC SCM+FSA by AMI_1:def 15
.= (while=0(a,I) +* Start-At insloc 0).IC SCM+FSA by A6,FUNCT_4:14
.= insloc 0 by SF_MASTR:66;
s1.insloc 0 = (while=0(a,I) +* Start-At insloc 0).insloc 0 by A4,A5,
FUNCT_4:14
.= while=0(a,I).insloc 0 by A4,SCMFSA6B:7
.= i by Th11;
then A8: CurInstr s1 = i by A7,AMI_1:def 17;
A9: (Computation s1).(0 + 1) = Following (Computation s1).0 by AMI_1:def 19
.= Following s1 by AMI_1:def 19
.= Exec(i,s1) by A8,AMI_1:def 18;
not a in dom (while=0(a,I) +* Start-At insloc 0) & a in dom s
by SCMFSA6B:12,SCMFSA_2:66;
then A10: s1.a = s.a by FUNCT_4:12;
A11: IC s2 = s2.IC SCM+FSA by AMI_1:def 15
.= insloc 4 by A3,A9,A10,SCMFSA_2:96;
(for c holds s2.c = s1.c) & for f holds s2.f = s1.f
by A9,SCMFSA_2:96;
then A12: s2 | D = s1 | D by SCMFSA6A:38
.= s | D by SCMFSA8A:11
.= sI | D by SCMFSA8A:11;
defpred P[Nat] means
$1 <= LifeSpan sI implies
IC (Computation s1).(1 + $1) = IC (Computation sI).$1 + 4 &
(Computation s1).(1 + $1) | D = (Computation sI).$1 | D;
A13: P[0]
proof assume 0 <= LifeSpan sI;
A14: IC SCM+FSA in dom (I +* Start-At insloc 0) by SF_MASTR:65;
IC (Computation sI).0 = IC sI by AMI_1:def 19
.= sI.IC SCM+FSA by AMI_1:def 15
.= (I +* Start-At insloc 0).IC SCM+FSA by A14,FUNCT_4:14
.= insloc 0 by SF_MASTR:66;
then IC (Computation sI).0 + 4 = insloc (0+ 4) by SCMFSA_4:def 1;
hence IC (Computation s1).(1 + 0) = IC (Computation sI).0 + 4 &
(Computation s1).(1 + 0) | D = (Computation sI).0 | D
by A11,A12,AMI_1:def 19;
end;
A15: now let k be Nat;
assume A16: P[k];
now assume A17: k + 1 <= LifeSpan sI;
k + 0 < k + 1 by REAL_1:53;
then k < LifeSpan sI by A17,AXIOMS:22;
hence
IC (Computation s1).(1 + k+1) = IC (Computation sI).(k+1) + 4 &
(Computation s1).(1 + k+1) | D = (Computation sI).(k+1) | D
by A1,A2,A16,Th19;
end;
hence P[k + 1];
end;
set s2=(Computation s1).(1 + LifeSpan sI);
set loc4=insloc (card I + 4);
set s3=(Computation s1).(1+LifeSpan sI+1);
A18: for k being Nat holds P[k] from Ind(A13,A15);
then P[LifeSpan sI];
then A19: CurInstr s2 = goto loc4 by A1,A2,Th20;
A20: s3 = Following s2 by AMI_1:def 19
.= Exec(goto loc4,s2) by A19,AMI_1:def 18;
A21: loc4 in dom while=0(a,I) by Th13;
A22: IC s3 = s3.IC SCM+FSA by AMI_1:def 15
.= loc4 by A20,SCMFSA_2:95;
set s4=(Computation s1).(1+LifeSpan sI+1+1);
s3.loc4 = s1.loc4 by AMI_1:54
.= (while=0(a,I) +* Start-At insloc 0).loc4 by A5,A21,FUNCT_4:14
.= while=0(a,I).loc4 by A21,SCMFSA6B:7
.= goto insloc 0 by Th21;
then A23: CurInstr s3 = goto insloc 0 by A22,AMI_1:def 17;
A24: s4 = Following s3 by AMI_1:def 19
.= Exec(goto insloc 0,s3) by A23,AMI_1:def 18;
A25: IC s4 = s4.IC SCM+FSA by AMI_1:def 15
.= insloc 0 by A24,SCMFSA_2:95;
A26: LifeSpan sI+1+1+1 = LifeSpan sI+(1+1)+1 by XCMPLX_1:1
.=LifeSpan sI+(2+1) by XCMPLX_1:1; hence
IC (Computation s1).(LifeSpan sI+3) = insloc 0 by A25;
A27: now let k be Nat;
assume A28: k <= LifeSpan sI+3;
assume k<>0;
then consider n being Nat such that
A29: k = n+ 1 by NAT_1:22;
k<=LifeSpan sI+1 or k >= LifeSpan sI+1+1 by NAT_1:38;
then A30: k<=LifeSpan sI+1 or k = LifeSpan sI+1+1 or k > LifeSpan sI+1+1
by REAL_1:def 5;
per cases by A26,A30,NAT_1:38;
suppose k<=LifeSpan sI+1;
then n <= LifeSpan sI by A29,REAL_1:53;
then A31: IC C1.(1 + n) = IC (Computation sI).n + 4 by A18;
consider m being Nat such that A32: IC (Computation sI).n = insloc m
by SCMFSA_2:21;
insloc m in dom I by A1,A32,SCMFSA7B:def 7;
then m < card I by SCMFSA6A:15;
then A33: m+4 < card I+ 6 by REAL_1:67;
card while=0(a,I) = card I + 6 by Th4;
then insloc (m+4) in dom while=0(a,I) by A33,SCMFSA6A:15;
hence IC C1.k in dom while=0(a,I) by A29,A31,A32,SCMFSA_4:def 1;
suppose k=LifeSpan sI+1+1;
hence IC C1.k in dom while=0(a,I) by A22,Th13;
suppose k >= LifeSpan sI+3;
then k = LifeSpan sI+3 by A28,AXIOMS:21;
hence IC C1.k in dom while=0(a,I) by A25,A26,Th10;
end;
now let k be Nat;
assume A34: k <= LifeSpan sI+3;
per cases;
suppose k = 0;
hence IC C1.k in dom while=0(a,I) by A4,A7,AMI_1:def 19;
suppose k <>0;
hence IC C1.k in dom while=0(a,I) by A27,A34;
end;hence
for k being Nat st k <= LifeSpan sI + 3 holds IC C1.k in dom while=0(a,I
);
end;
set sl0= Start-At insloc 0;
reserve s for State of SCM+FSA,
I for Macro-Instruction,
a for read-write Int-Location;
definition
let s,I,a;
deffunc U(Nat,Element of product the Object-Kind of SCM+FSA) =
(Computation ($2 +* (while=0(a,I) +* sl0))).
(LifeSpan ($2 +* (I +* sl0)) + 3);
func StepWhile=0(a,I,s) -> Function of NAT,product the Object-Kind of SCM+FSA
means
:Def4:
it.0 = s &
for i being Nat
holds it.(i+1)=(Computation (it.i +* (while=0(a,I) +* sl0))).
(LifeSpan (it.i +* (I +* sl0)) + 3);
existence
proof thus ex f being Function of NAT,product the Object-Kind of SCM+FSA st
f.0 = s & for i being Nat holds f.(i+1)= U(i,f.i)
from LambdaRecExD;
end;
uniqueness
proof
let F1,F2 be Function of NAT,product the Object-Kind of SCM+FSA
such that
A1: F1.0 = s & for i being Nat holds F1.(i+1)= U(i,F1.i) and
A2: F2.0 = s & for i being Nat holds F2.(i+1)= U(i,F2.i);
thus F1 = F2 from LambdaRecUnD(A1,A2);
end;
end;
reserve i,k,m,n for Nat;
canceled 2;
theorem Th25:
StepWhile=0(a,I,s).(k+1)=StepWhile=0(a,I,StepWhile=0(a,I,s).k).1
proof
set sk=StepWhile=0(a,I,s).k;
set sk0=StepWhile=0(a,I,sk).0;
sk0=sk by Def4;
hence StepWhile=0(a,I,s).(k+1) =(Computation (sk0 +*(while=0(a,I) +* sl0))
).
(LifeSpan (sk0 +* (I +* sl0)) + 3) by Def4
.=StepWhile=0(a,I,sk).(0+1) by Def4
.=StepWhile=0(a,I,sk).1;
end;
scheme MinIndex { F(Nat)->Nat,j() -> Nat} :
ex k st F(k)=0 & for n st F(n)=0 holds k <= n
provided
A1: F(0) = j() and
A2: for k holds (F(k+1) < F(k) or F(k) = 0)
proof
defpred P[Nat] means ex n st $1 = F(n);
A3: ex k st P[k] by A1;
A4: for k st k <> 0 & P[k] ex m st m < k & P[m]
proof let k; assume
A5: k <> 0 & P[k];
then consider n such that
A6: k = F(n);
take F(n + 1);
thus thesis by A2,A5,A6;
end;
defpred X[Nat] means F($1)=0;
P[0] from Regr(A3,A4);
then A7: ex k st X[k];
thus ex k st X[k] & for n st X[n] holds k <= n from Min(A7);
end;
theorem
for f,g being Function holds f +* g +* g = f +* g
proof
let f,g be Function;
thus f +* g +* g = f +*( g +* g ) by FUNCT_4:15
.= f +* g;
end;
theorem Th27:
for f,g,h being Function, D being set holds
(f +* g)|D =h | D implies (h +* g) | D = (f +* g) | D
proof
let f,g,h be Function, D be set;
assume A1: (f +* g)|D =h | D;
A2: dom ((f +* g) | D) = dom (f +* g) /\ D by RELAT_1:90
.= (dom f \/ dom g) /\ D by FUNCT_4:def 1;
A3: dom ((h +* g) | D) = dom (h +* g) /\ D by RELAT_1:90
.= (dom h \/ dom g) /\ D by FUNCT_4:def 1;
then A4: dom ((h +* g) | D) = (dom h /\ D) \/ (dom g /\ D) by XBOOLE_1:23
.= ((dom f \/ dom g) /\ D) \/ (dom g /\ D) by A1,A2,RELAT_1:90
.= ((dom f \/ dom g) \/ dom g) /\ D by XBOOLE_1:23
.= (dom f \/ (dom g \/ dom g)) /\ D by XBOOLE_1:4
.= (dom f \/ dom g ) /\ D;
now let x be set;
assume A5:x in dom ((f +* g) | D);
then A6: x in dom f \/ dom g & x in D by A2,XBOOLE_0:def 3;
A7: x in dom h \/ dom g by A2,A3,A4,A5,XBOOLE_0:def 3;
A8: ((h +* g) | D).x = (h +* g).x by A2,A4,A5,FUNCT_1:70;
per cases;
suppose A9: x in dom g;
((f +* g) | D).x = (f +* g).x by A5,FUNCT_1:70
.=g.x by A6,A9,FUNCT_4:def 1;
hence ((h +* g) | D).x =((f +* g) | D).x by A7,A8,A9,FUNCT_4:def 1;
suppose not x in dom g;
hence ((h +* g) | D).x = h.x by A7,A8,FUNCT_4:def 1
.=((f +* g) | D).x by A1,A6,FUNCT_1:72;
end;
hence thesis by A2,A4,FUNCT_1:9;
end;
theorem
for f,g,h being Function, D being set holds
f | D =h | D implies (h +* g) | D = (f +* g) | D
proof
let f,g,h be Function, D be set;
assume A1: f |D =h | D;
A2: dom ((f +* g) | D) = dom (f +* g) /\ D by RELAT_1:90
.= (dom f \/ dom g) /\ D by FUNCT_4:def 1;
A3: dom ((h +* g) | D) = dom (h +* g) /\ D by RELAT_1:90
.= (dom h \/ dom g) /\ D by FUNCT_4:def 1;
then A4: dom ((h +* g) | D) = (dom h /\ D) \/ (dom g /\ D) by XBOOLE_1:23
.= dom (f| D) \/ (dom g /\ D) by A1,RELAT_1:90
.= (dom f /\ D) \/ (dom g /\ D) by RELAT_1:90
.= (dom f \/ dom g ) /\ D by XBOOLE_1:23;
now let x be set;
assume A5:x in dom ((f +* g) | D);
then A6: x in dom f \/ dom g & x in D by A2,XBOOLE_0:def 3;
A7: x in dom h \/ dom g by A2,A3,A4,A5,XBOOLE_0:def 3;
A8: ((h +* g) | D).x = (h +* g).x by A2,A4,A5,FUNCT_1:70;
per cases;
suppose A9: x in dom g;
((f +* g) | D).x = (f +* g).x by A5,FUNCT_1:70
.=g.x by A6,A9,FUNCT_4:def 1;
hence ((h +* g) | D).x =((f +* g) | D).x by A7,A8,A9,FUNCT_4:def 1;
suppose A10:not x in dom g;
then A11: ((h +* g) | D).x = h.x by A7,A8,FUNCT_4:def 1
.=(h | D ).x by A6,FUNCT_1:72;
thus ((f +* g) | D).x = (f +* g).x by A5,FUNCT_1:70
.=f.x by A6,A10,FUNCT_4:def 1
.=((h +* g) | D).x by A1,A6,A11,FUNCT_1:72;
end;
hence thesis by A2,A4,FUNCT_1:9;
end;
set IL = the Instruction-Locations of SCM+FSA;
theorem Th29:
for s1,s2 being State of SCM+FSA
st IC s1 = IC s2 & s1 | (Int-Locations \/ FinSeq-Locations) =
s2 | (Int-Locations \/ FinSeq-Locations) & s1 | IL = s2 | IL
holds s1 = s2
proof
set IL = the Instruction-Locations of SCM+FSA;
let s1,s2 be State of SCM+FSA;
set D = Int-Locations \/ FinSeq-Locations;
assume A1: IC s1 = IC s2;
assume A2: s1 | D = s2 | D;
assume s1 | IL = s2 | IL;
then A3: for l being Instruction-Location of SCM+FSA holds s1.l = s2.l
by SCMFSA6A:36;
((for a being Int-Location holds s1.a = s2.a) &
for f being FinSeq-Location holds s1.f = s2.f) by A2,SCMFSA6A:38;
hence thesis by A1,A3,SCMFSA_2:86;
end;
theorem Th30:
for I being Macro-Instruction,a being read-write Int-Location,
s being State of SCM+FSA holds
StepWhile=0(a,I,s).(0+1)=(Computation (s +* (while=0(a,I) +* sl0))).
(LifeSpan (s+* (I +* sl0)) + 3)
proof
let I be Macro-Instruction,a be read-write Int-Location,
s be State of SCM+FSA;
thus StepWhile=0(a,I,s).(0+1)=(Computation (StepWhile=0(a,I,s).0 +*
(while=0(a,I) +* sl0))).(LifeSpan (StepWhile=0(a,I,s).0 +*
(I +* sl0)) + 3) by Def4
.=(Computation (s +* (while=0(a,I) +* sl0)))
.(LifeSpan (StepWhile=0(a,I,s).0+* (I +* sl0)) + 3) by Def4
.=(Computation (s +* (while=0(a,I) +* sl0)))
.(LifeSpan (s+* (I +* sl0)) + 3) by Def4;
end;
theorem Th31:
for I being Macro-Instruction,a being read-write Int-Location,
s being State of SCM+FSA,k,n being Nat st
IC StepWhile=0(a,I,s).k =insloc 0 & StepWhile=0(a,I,s).k=
(Computation (s +* (while=0(a,I) +* Start-At insloc 0))).n holds
StepWhile=0(a,I,s).k = StepWhile=0(a,I,s).k +* (while=0(a,I)+*
Start-At insloc 0) &
StepWhile=0(a,I,s).(k+1)=(Computation (s +* (while=0(a,I) +*
Start-At insloc 0))).
(n +(LifeSpan (StepWhile=0(a,I,s).k +* (I +* Start-At insloc 0)) + 3))
proof
set IL = the Instruction-Locations of SCM+FSA;
let I be Macro-Instruction,a be read-write Int-Location,
s be State of SCM+FSA,k,n be Nat;
set D = Int-Locations \/ FinSeq-Locations;
set s1 = s +* (while=0(a,I) +* Start-At insloc 0);
set sk=StepWhile=0(a,I,s).k;
set s2=sk +* (while=0(a,I)+* sl0);
assume A1:IC sk =insloc 0;
assume A2:sk =(Computation s1).n;
A3: IC SCM+FSA in dom (while=0(a,I) +* sl0 ) by SF_MASTR:65;
A4: IC s2 = s2.IC SCM+FSA by AMI_1:def 15
.= (while=0(a,I) +* sl0).IC SCM+FSA by A3,FUNCT_4:14
.= IC sk by A1,SF_MASTR:66;
A5: s2 | D = sk | D by SCMFSA8A:11;
sk | IL =s1 | IL by A2,SCMFSA6B:17;
then s2 | IL = sk | IL by Th27;hence
s2=sk by A4,A5,Th29;
hence
StepWhile=0(a,I,s).(k+1)=
(Computation sk).(LifeSpan (sk +* (I +* sl0)) + 3) by Def4
.=(Computation s1).(n +(LifeSpan (sk +* (I +* sl0)) + 3)) by A2,AMI_1:51;
end;
theorem Th32:
for I being Macro-Instruction,a being read-write Int-Location,
s being State of SCM+FSA st (for k being Nat holds
I is_closed_on StepWhile=0(a,I,s).k &
I is_halting_on StepWhile=0(a,I,s).k) &
ex f being Function of product the Object-Kind of SCM+FSA,NAT st
(for k being Nat holds (f.(StepWhile=0(a,I,s).(k+1)) <
f.(StepWhile=0(a,I,s).k)
or f.(StepWhile=0(a,I,s).k) = 0) &
( f.(StepWhile=0(a,I,s).k)=0 iff (StepWhile=0(a,I,s).k).a <> 0 ) )
holds
while=0(a,I) is_halting_on s & while=0(a,I) is_closed_on s
proof
set IL = the Instruction-Locations of SCM+FSA;
let I be Macro-Instruction,a be read-write Int-Location,
s be State of SCM+FSA;
assume A1: for k being Nat holds I is_closed_on StepWhile=0(a,I,s).k &
I is_halting_on StepWhile=0(a,I,s).k;
given f being Function of product the Object-Kind of SCM+FSA,NAT
such that A2:for k being Nat holds
(f.(StepWhile=0(a,I,s).(k+1)) < f.(StepWhile=0(a,I,s).k) or
f.(StepWhile=0(a,I,s).k) = 0) &
( f.(StepWhile=0(a,I,s).k)=0 iff (StepWhile=0(a,I,s).k).a <> 0 );
deffunc F(Nat) = f.(StepWhile=0(a,I,s).$1);
set s1 = s +* (while=0(a,I) +* Start-At insloc 0);
A3: F(0) =f.s by Def4;
A4: for k holds ( F(k+1) < F(k) or F(k) = 0 ) by A2;
consider m being Nat such that
A5: F(m)=0 and
A6: for n st F(n) =0 holds m <= n from MinIndex(A3,A4);
defpred P[Nat] means
$1+1 <= m implies
ex k st StepWhile=0(a,I,s).($1+1)=(Computation s1).k;
A7: P[0]
proof assume 0+1 <= m;
take n=(LifeSpan (s+* (I +* sl0)) + 3);
thus StepWhile=0(a,I,s).(0+1)=(Computation s1).n by Th30;
end;
A8: IC SCM+FSA in dom (while=0(a,I) +* sl0 ) by SF_MASTR:65;
A9: now let k be Nat;
assume A10: P[k];
now assume A11: (k+1)+ 1 <= m;
k + 0 < k+ (1+ 1) by REAL_1:53;
then k < (k+1) +1 by XCMPLX_1:1;
then A12: k < m by A11,AXIOMS:22;
A13: (k+1)+ 0 < (k+ 1)+ 1 by REAL_1:53;
set sk=StepWhile=0(a,I,s).k;
set sk1=StepWhile=0(a,I,s).(k+1);
consider n being Nat such that
A14: sk1 = (Computation s1).n by A10,A11,A13,AXIOMS:22;
A15: sk1= (Computation (sk +* (while=0(a,I)+* sl0))).
(LifeSpan (sk +* (I +* sl0)) + 3) by Def4;
A16: I is_closed_on sk & I is_halting_on sk by A1;
F(k) <> 0 by A6,A12;
then sk.a = 0 by A2;
then A17: IC sk1 =insloc 0 by A15,A16,Th22;
take m=n +(LifeSpan (sk1 +* (I +* sl0)) + 3);
thus StepWhile=0(a,I,s).((k+1)+1)=(Computation s1).m by A14,A17,Th31
;
end;
hence P[k+1];
end;
A18: for k being Nat holds P[k] from Ind(A7,A9);
now per cases;
suppose m=0;
then (StepWhile=0(a,I,s).0).a <> 0 by A2,A5;
then s.a <> 0 by Def4;
hence while=0(a,I) is_halting_on s & while=0(a,I) is_closed_on s
by Th18;
suppose A19:m<>0;
then consider i being Nat such that
A20: m=i+1 by NAT_1:22;
set si=StepWhile=0(a,I,s).i;
set sm=StepWhile=0(a,I,s).m;
set sm1=sm +* (while=0(a,I)+* sl0);
consider n being Nat such that
A21: sm = (Computation s1).n by A18,A20;
A22: sm.a <> 0 by A2,A5;
A23: sm= (Computation (si +* (while=0(a,I)+* sl0))).
(LifeSpan (si +* (I +* sl0)) + 3) by A20,Def4;
A24: I is_closed_on si & I is_halting_on si by A1;
i < m by A20,NAT_1:38;
then F(i) <> 0 by A6;
then si.a = 0 by A2;
then A25: IC sm =insloc 0 by A23,A24,Th22;
A26: IC sm1 = sm1.IC SCM+FSA by AMI_1:def 15
.= (while=0(a,I) +* sl0).IC SCM+FSA by A8,FUNCT_4:14
.= IC sm by A25,SF_MASTR:66;
set D = Int-Locations \/ FinSeq-Locations;
A27: sm1 | D = sm | D by SCMFSA8A:11;
sm | IL =s1 | IL by A21,SCMFSA6B:17;
then sm1 | IL = sm | IL by Th27;
then A28: sm1=sm by A26,A27,Th29;
while=0(a,I) is_halting_on sm by A22,Th18;
then sm1 is halting by SCMFSA7B:def 8;
then consider j being Nat such that
A29: CurInstr((Computation sm).j) = halt SCM+FSA by A28,AMI_1:def 20;
CurInstr (Computation s1).(n+j) = halt SCM+FSA by A21,A29,AMI_1:51;
then s1 is halting by AMI_1:def 20;
hence while=0(a,I) is_halting_on s by SCMFSA7B:def 8;
set p=(LifeSpan (s+* (I +* sl0)) + 3);
now let q be Nat;
A30: 0<m by A19,NAT_1:19;
per cases;
suppose A31: q <= p;
A32: StepWhile=0(a,I,s).0=s by Def4;
F(0) <> 0 by A6,A30;
then A33: s.a = 0 by A2,A32;
I is_closed_on s & I is_halting_on s by A1,A32;
hence IC (Computation s1).q in dom while=0(a,I) by A31,A33,
Th22;
suppose A34: q > p;
defpred P2[Nat] means
$1<=m & $1<>0 & (ex k st StepWhile=0(a,I,s).$1=
(Computation s1).k & k <= q);
A35: for i be Nat st P2[i] holds i <= m;
A36: now
take k=p;
thus StepWhile=0(a,I,s).1=(Computation s1).k &
k <= q by A34,Th30;
end;
0+1 < m +1 by A30,REAL_1:53;
then 1 <= m by NAT_1:38;
then A37: ex t be Nat st P2[t] by A36;
ex k st P2[k] & for i st P2[i] holds i <= k from Max(A35,A37
)
;
then consider t being Nat such that
A38: P2[t] & for i st P2[i] holds i <= t;
now per cases;
suppose t=m;
then consider r being Nat such that
A39: sm=(Computation s1).r & r <= q by A38;
consider x being Nat such that
A40: q = r+x by A39,NAT_1:28;
A41: (Computation s1).q = (Computation sm1).x by A28,A39,A40,
AMI_1:51;
while=0(a,I) is_closed_on sm by A22,Th18;
hence IC (Computation s1).q in dom while=0(a,I) by A41,
SCMFSA7B:def 7;
suppose t<>m;
then A42: t < m by A38,REAL_1:def 5;
consider y being Nat such that
A43: t=y+1 by A38,NAT_1:22;
consider z being Nat such that
A44: StepWhile=0(a,I,s).t=(Computation s1).z & z <= q by A38;
y+ 0 < t by A43,REAL_1:53;
then A45: y < m by A38,AXIOMS:22;
set Dy=StepWhile=0(a,I,s).y;
set Dt=StepWhile=0(a,I,s).t;
A46: Dt= (Computation (Dy +* (while=0(a,I)+* sl0))).
(LifeSpan (Dy +* (I +* sl0)) + 3) by A43,Def4;
A47: I is_closed_on Dy & I is_halting_on Dy by A1;
F(y) <> 0 by A6,A45;
then Dy.a = 0 by A2;
then A48: IC Dt =insloc 0 by A46,A47,Th22;
set z2=z +(LifeSpan (Dt +* (I +* sl0)) + 3);
A49: now assume A50: z2 <= q;
A51: now take k=z2;thus
StepWhile=0(a,I,s).(t+1)=(Computation s1).k & k <=q
by A44,A48,A50,Th31;
end;
t+1 <= m by A42,NAT_1:38;
then t+1 <= t by A38,A51;
hence contradiction by REAL_1:69;
end;
consider w being Nat such that
A52: q = z+w by A44,NAT_1:28;
A53: w < LifeSpan (Dt +* (I +* sl0)) + 3 by A49,A52,AXIOMS:24
;
A54: (Computation s1).q = (Computation Dt ).w by A44,A52,
AMI_1:51
.= (Computation (Dt +* (while=0(a,I)+* sl0))).w
by A44,A48,Th31;
A55: I is_closed_on Dt & I is_halting_on Dt by A1;
F(t) <> 0 by A6,A42;
then Dt.a = 0 by A2;
hence IC (Computation s1).q in dom while=0(a,I)
by A53,A54,A55,Th22;
end;
hence IC (Computation s1).q in dom while=0(a,I);
end;
hence while=0(a,I) is_closed_on s by SCMFSA7B:def 7;
end;
hence thesis;
end;
theorem Th33:
for I being parahalting Macro-Instruction, a being read-write
Int-Location, s being State of SCM+FSA st
ex f being Function of product the Object-Kind of SCM+FSA,NAT st
(for k being Nat holds (f.(StepWhile=0(a,I,s).(k+1)) <
f.(StepWhile=0(a,I,s).k) or f.(StepWhile=0(a,I,s).k) = 0) &
( f.(StepWhile=0(a,I,s).k)=0 iff (StepWhile=0(a,I,s).k).a <> 0 ) )
holds
while=0(a,I) is_halting_on s & while=0(a,I) is_closed_on s
proof
let I be parahalting Macro-Instruction,a be read-write
Int-Location,s be State of SCM+FSA;
assume A1:
ex f being Function of product the Object-Kind of SCM+FSA,NAT st
(for k being Nat holds (f.(StepWhile=0(a,I,s).(k+1)) <
f.(StepWhile=0(a,I,s).k) or f.(StepWhile=0(a,I,s).k) = 0) &
( f.(StepWhile=0(a,I,s).k)=0 iff (StepWhile=0(a,I,s).k).a <> 0 ) );
A2: for k being Nat holds I is_closed_on StepWhile=0(a,I,s).k by SCMFSA7B:24;
for k being Nat holds I is_halting_on StepWhile=0(a,I,s).k by SCMFSA7B:
25
;
hence thesis by A1,A2,Th32;
end;
theorem
for I being parahalting Macro-Instruction, a being read-write
Int-Location st
ex f being Function of product the Object-Kind of SCM+FSA,NAT st
(for s being State of SCM+FSA holds (f.(StepWhile=0(a,I,s).1) < f.s
or f.s = 0) & ( f.s =0 iff s.a <> 0 ))
holds while=0(a,I) is parahalting
proof
let I be parahalting Macro-Instruction,a be read-write
Int-Location;
given f being Function of product the Object-Kind of SCM+FSA,NAT
such that A1: for s being State of SCM+FSA holds
(f.(StepWhile=0(a,I,s).1) < f.s or f.s = 0) & ( f.s =0 iff s.a <> 0 );
now let t be State of SCM+FSA;
now let k be Nat;
(f.(StepWhile=0(a,I,StepWhile=0(a,I,t).k).1) <
f.(StepWhile=0(a,I,t).k) or f.(StepWhile=0(a,I,t).k) = 0) &
( f.(StepWhile=0(a,I,t).k)=0 iff (StepWhile=0(a,I,t).k).a <> 0 )
by A1;hence
(f.(StepWhile=0(a,I,t).(k+1)) <
f.(StepWhile=0(a,I,t).k) or f.(StepWhile=0(a,I,t).k) = 0) &
( f.(StepWhile=0(a,I,t).k)=0 iff (StepWhile=0(a,I,t).k).a <> 0 )
by Th25;
end;
hence while=0(a,I) is_halting_on t by Th33;
end;
hence thesis by SCMFSA7B:25;
end;
theorem Th35:
for l1,l2 being Instruction-Location of SCM+FSA,a being Int-Location holds
(l1 .--> goto l2) does_not_destroy a
proof
let l1,l2 be Instruction-Location of SCM+FSA,a be Int-Location;
set I=l1 .--> goto l2;
A1: rng I={goto l2 } by CQC_LANG:5;
now let i be Instruction of SCM+FSA;
assume i in rng I;
then i=goto l2 by A1,TARSKI:def 1;
hence i does_not_destroy a by SCMFSA7B:17;
end;
hence thesis by SCMFSA7B:def 4;
end;
theorem Th36:
for i being Instruction of SCM+FSA st i does_not_destroy intloc 0 holds
Macro i is good
proof
let i be Instruction of SCM+FSA;
assume A1:i does_not_destroy intloc 0;
set I=Macro i;
I = (insloc 0,insloc 1) --> (i,halt SCM+FSA) by SCMFSA6A:def 2;
then A2: rng I c={i,halt SCM+FSA} by FUNCT_4:65;
now let x be Instruction of SCM+FSA;
assume A3: x in rng I;
per cases by A2,A3,TARSKI:def 2;
suppose x = i;
hence x does_not_destroy intloc 0 by A1;
suppose x = halt SCM+FSA;
hence x does_not_destroy intloc 0 by SCMFSA7B:11;
end;
then I does_not_destroy intloc 0 by SCMFSA7B:def 4;
hence thesis by SCMFSA7B:def 5;
end;
definition
let I,J be good Macro-Instruction,a be Int-Location;
cluster if=0(a,I,J) -> good;
correctness
proof
set i = a =0_goto insloc (card J + 3);
i does_not_destroy intloc 0 by SCMFSA7B:18;
then reconsider Mi=Macro i as good Macro-Instruction by Th36;
if=0(a,I,J) = i ';' J ';' Goto insloc (card I + 1) ';' I ';'
SCM+FSA-Stop by SCMFSA8B:def 1
.= Mi ';' J ';' Goto insloc (card I + 1) ';' I ';'
SCM+FSA-Stop by SCMFSA6A:def 5;
hence thesis;
end;
end;
definition
let I be good Macro-Instruction,a be Int-Location;
cluster while=0(a,I) -> good;
correctness
proof
set J=insloc (card I +4) .--> goto insloc 0;
set F=if=0(a, I ';' Goto insloc 0, SCM+FSA-Stop);
A1: J does_not_destroy intloc 0 by Th35;
A2: F does_not_destroy intloc 0 by SCMFSA7B:def 5;
while=0(a,I) = F+*J by Def1;
then while=0(a,I) does_not_destroy intloc 0 by A1,A2,SCMFSA8A:25;
hence thesis by SCMFSA7B:def 5;
end;
end;
:: -----------------------------------------------------------
:: WHILE>0 Statement
theorem Th37:
for a being Int-Location, I being Macro-Instruction,k being Nat st
k < 6 holds insloc k in dom while>0(a,I)
proof
let a be Int-Location, I be Macro-Instruction,k be Nat;
assume A1: k < 6;
6 <= card I + 6 by NAT_1:29;
then A2: k < card I + 6 by A1,AXIOMS:22;
card while>0(a,I) = card I + 6 by Th5;
hence thesis by A2,SCMFSA6A:15;
end;
theorem Th38:
for a being Int-Location, I being Macro-Instruction,k being Nat st
k < 6 holds insloc (card I +k) in dom while>0(a,I)
proof
let a be Int-Location, I be Macro-Instruction,k be Nat;
assume k < 6;
then A1: card I + k < card I + 6 by REAL_1:53;
card while>0(a,I) = card I + 6 by Th5;
hence thesis by A1,SCMFSA6A:15;
end;
theorem Th39:
for a being Int-Location, I being Macro-Instruction holds
while>0(a,I).insloc (card I +5) = halt SCM+FSA
proof
let a be Int-Location;
let I be Macro-Instruction;
set I1= I ';' Goto insloc 0;
set J = SCM+FSA-Stop;
set f = insloc (card I +4) .--> goto insloc 0;
set i = a >0_goto insloc (card J + 3);
set c5 = card I + 5;
set Lc5=insloc c5;
A1: dom f = {insloc (card I + 4)} by CQC_LANG:5;
c5 <> card I + 4 by XCMPLX_1:2;
then Lc5 <> insloc (card I + 4) by SCMFSA_2:18;
then A2: not Lc5 in dom f by A1,TARSKI:def 1;
A3: Lc5 in dom while>0(a,I) by Th38;
while>0(a,I) = if>0(a, I1, J) +* f by Def2;
then A4: dom while>0(a,I) = dom if>0(a,I1,J) \/ dom f by FUNCT_4:def 1;
then A5: Lc5 in dom if>0(a,I1,J) by A2,A3,XBOOLE_0:def 2;
set Mi= Macro i ';' J ';' Goto insloc (card I1 + 1) ';' I1;
set J1= SCM+FSA-Stop;
A6: if>0(a, I1, J)
= i ';' J ';' Goto insloc (card I1 + 1) ';' I1 ';' SCM+FSA-Stop
by SCMFSA8B:def 2
.= Mi ';' J1 by SCMFSA6A:def 5;
then card if>0(a, I1,J) = card Mi + card J1 by SCMFSA6A:61;
then A7: card Mi = card if>0(a,I1,J)-card J1 by XCMPLX_1:26
.= card I + 6 - 1 by Th2,SCMFSA8A:17
.= card I + (5+1-1) by XCMPLX_1:29
.= c5;
then A8: not Lc5 in dom Mi by SCMFSA6A:15;
A9: if>0(a, I1, J) = Directed Mi +* ProgramPart Relocated(J1, c5) by A6,A7,
SCMFSA6A:def 4;
then A10: dom if>0(a,I1,J) = dom Directed Mi \/ dom ProgramPart Relocated(J1,
c5)
by FUNCT_4:def 1;
then dom if>0(a,I1,J)
= dom Mi \/ dom ProgramPart Relocated(J1, c5) by SCMFSA6A:14;
then A11: Lc5 in dom ProgramPart Relocated(J1, c5) by A5,A8,XBOOLE_0:def 2;
A12: insloc 0 + c5 = insloc ( 0 + c5) by SCMFSA_4:def 1;
insloc 0 + c5 in { il+c5 where il is Instruction-Location of SCM+FSA:
il in dom J1} by SCMFSA8A:16;
then A13: insloc c5 in dom Shift(J1,c5) by A12,SCMFSA_4:31;
then A14: pi(Shift(J1,c5),Lc5) = Shift(J1,c5).(insloc 0 +c5) by A12,AMI_5:def 5
.= halt SCM+FSA by SCMFSA8A:16,SCMFSA_4:30;
thus while>0(a,I).Lc5 = (if>0(a, I1, J) +* f).Lc5 by Def2
.= (Directed Mi +* ProgramPart Relocated(J1, c5)).Lc5 by A2,A3,A4,A9,FUNCT_4
:def 1
.= (ProgramPart Relocated(J1,c5)).Lc5 by A5,A10,A11,FUNCT_4:def 1
.= IncAddr(Shift(ProgramPart(J1),c5),c5).Lc5 by SCMFSA_5:2
.= IncAddr(Shift(J1,c5),c5).Lc5 by AMI_5:72
.= IncAddr( halt SCM+FSA, c5 ) by A13,A14,SCMFSA_4:24
.= halt SCM+FSA by SCMFSA_4:8;
end;
theorem Th40:
for a being Int-Location, I being Macro-Instruction holds
while>0(a,I).insloc 3 = goto insloc (card I +5)
proof
let a be Int-Location;
let I be Macro-Instruction;
set I1= I ';' Goto insloc 0;
set J = SCM+FSA-Stop;
set f = insloc (card I +4) .--> goto insloc 0;
set i = a >0_goto insloc (card J + 3);
A1: dom f = {insloc (card I + 4)} by CQC_LANG:5;
3 <> card I + 4 by NAT_1:29;
then insloc 3 <> insloc (card I + 4) by SCMFSA_2:18;
then A2: not insloc 3 in dom f by A1,TARSKI:def 1;
A3: insloc 3 in dom while>0(a,I) by Th37;
while>0(a,I) = if>0(a, I1, J) +* f by Def2;
then A4: dom while>0(a,I) = dom if>0(a,I1,J) \/ dom f by FUNCT_4:def 1;
then A5: insloc 3 in dom if>0(a,I1,J) by A2,A3,XBOOLE_0:def 2;
set Mi=Macro i ';' J;
set G=Goto insloc (card I1 + 1);
set J2= (I1 ';' SCM+FSA-Stop);
set J1=G ';' J2;
A6: card Mi = card Macro i + card J by SCMFSA6A:61
.= 2 + 1 by SCMFSA7B:6,SCMFSA8A:17;
then A7: not insloc 3 in dom Mi by SCMFSA6A:15;
A8: if>0(a, I1, J)
= i ';' J ';' Goto insloc (card I1 + 1) ';' I1 ';' SCM+FSA-Stop
by SCMFSA8B:def 2
.= i ';' J ';' Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop)
by SCMFSA6A:62
.= i ';' J ';' J1 by SCMFSA6A:62
.= Mi ';' J1 by SCMFSA6A:def 5
.= Directed Mi +* ProgramPart Relocated(J1, 3) by A6,SCMFSA6A:def 4;
then A9: dom if>0(a,I1,J) = dom Directed Mi \/ dom ProgramPart Relocated(J1, 3)
by FUNCT_4:def 1;
then dom if>0(a,I1,J)
= dom Mi \/ dom ProgramPart Relocated(J1, 3) by SCMFSA6A:14;
then A10: insloc 3 in dom ProgramPart Relocated(J1, 3) by A5,A7,XBOOLE_0:def 2;
A11: insloc 0 in dom G by SCMFSA8A:47;
A12: G.insloc 0 = goto insloc (card I1 + 1) by SCMFSA8A:47
.= goto insloc (card I + card Goto insloc 0 + 1) by SCMFSA6A:61
.= goto insloc (card I + 1 + 1) by SCMFSA8A:29
.= goto insloc (card I +(1+1)) by XCMPLX_1:1;
then A13: G.insloc 0 <> halt SCM+FSA by Th9;
A14: insloc 0 + 3 = insloc ( 0 + 3) by SCMFSA_4:def 1;
J1= Directed G +* ProgramPart Relocated(J2, card G) by SCMFSA6A:def 4;
then dom J1 = dom Directed G \/ dom ProgramPart Relocated(J2, card G)
by FUNCT_4:def 1
.= dom G \/ dom ProgramPart Relocated(J2, card G) by SCMFSA6A:14;
then A15: insloc 0 in dom J1 by A11,XBOOLE_0:def 2;
then insloc 0 + 3 in { il+3 where il is Instruction-Location of SCM+FSA:
il in dom J1};
then A16: insloc 3 in dom Shift(J1,3) by A14,SCMFSA_4:31;
then A17: pi(Shift(J1,3),insloc 3) =Shift(J1,3).(insloc 0 +3) by A14,AMI_5:def
5
.=J1.insloc 0 by A15,SCMFSA_4:30
.=(Directed G).insloc 0 by A11,SCMFSA8A:28
.=goto insloc (card I + 2) by A11,A12,A13,SCMFSA8A:30;
thus while>0(a,I).insloc 3 = (if>0(a, I1, J) +* f).insloc 3 by Def2
.= (Directed Mi +* ProgramPart Relocated(J1, 3)).insloc 3 by A2,A3,A4,A8,
FUNCT_4:def 1
.= (ProgramPart Relocated(J1,3)).insloc 3 by A5,A9,A10,FUNCT_4:def 1
.= IncAddr(Shift(ProgramPart(J1),3),3).insloc 3 by SCMFSA_5:2
.= IncAddr(Shift(J1,3),3).insloc 3 by AMI_5:72
.= IncAddr(goto insloc (card I +2),3) by A16,A17,SCMFSA_4:24
.= goto (insloc (card I +2) + 3) by SCMFSA_4:14
.= goto insloc (card I+ 2 +3) by SCMFSA_4:def 1
.= goto insloc (card I+ (2 +3)) by XCMPLX_1:1
.= goto insloc (card I+ 5);
end;
theorem Th41:
for a being Int-Location, I being Macro-Instruction holds
while>0(a,I).insloc 2 = goto insloc 3
proof
let a be Int-Location;
let I be Macro-Instruction;
set I1= I ';' Goto insloc 0;
set J = SCM+FSA-Stop;
set f = insloc (card I +4) .--> goto insloc 0;
set i = a >0_goto insloc (card J + 3);
A1: dom f = {insloc (card I + 4)} by CQC_LANG:5;
2 <> card I + 4 by NAT_1:29;
then insloc 2 <> insloc (card I + 4) by SCMFSA_2:18;
then A2: not insloc 2 in dom f by A1,TARSKI:def 1;
A3: insloc 2 in dom while>0(a,I) by Th37;
while>0(a,I) = if>0(a, I1, J) +* f by Def2;
then A4: dom while>0(a,I) = dom if>0(a,I1,J) \/ dom f by FUNCT_4:def 1;
then A5: insloc 2 in dom if>0(a,I1,J) by A2,A3,XBOOLE_0:def 2;
set Mi=Macro i;
set J2=Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop);
set J1=J ';' J2;
A6: card Mi = 2 by SCMFSA7B:6;
then A7: not insloc 2 in dom Mi by SCMFSA6A:15;
A8: if>0(a, I1, J)
= i ';' J ';' Goto insloc (card I1 + 1) ';' I1 ';' SCM+FSA-Stop
by SCMFSA8B:def 2
.= i ';' J ';' Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop)
by SCMFSA6A:62
.= i ';' J ';' (Goto insloc (card I1 + 1) ';' (I1 ';' SCM+FSA-Stop))
by SCMFSA6A:62
.= i ';' J1 by SCMFSA6A:66
.= Mi ';' J1 by SCMFSA6A:def 5
.= Directed Mi +* ProgramPart Relocated(J1, 2) by A6,SCMFSA6A:def 4;
then A9: dom if>0(a,I1,J) = dom Directed Mi \/ dom ProgramPart Relocated(J1, 2)
by FUNCT_4:def 1;
then dom if>0(a,I1,J)
= dom Mi \/ dom ProgramPart Relocated(J1, 2) by SCMFSA6A:14;
then A10: insloc 2 in dom ProgramPart Relocated(J1, 2) by A5,A7,XBOOLE_0:def 2;
A11: insloc 0 + 2 = insloc ( 0 + 2) by SCMFSA_4:def 1;
J1= Directed J +* ProgramPart Relocated(J2, card J) by SCMFSA6A:def 4;
then dom J1 = dom Directed J \/ dom ProgramPart Relocated(J2, card J)
by FUNCT_4:def 1
.= dom J \/ dom ProgramPart Relocated(J2, card J) by SCMFSA6A:14;
then A12: insloc 0 in dom J1 by SCMFSA8A:16,XBOOLE_0:def 2;
then insloc 0 + 2 in { il+2 where il is Instruction-Location of SCM+FSA:
il in dom J1};
then A13: insloc 2 in dom Shift(J1,2) by A11,SCMFSA_4:31;
then A14: pi(Shift(J1,2),insloc 2) =Shift(J1,2).(insloc 0 +2) by A11,AMI_5:def
5
.=J1.insloc 0 by A12,SCMFSA_4:30
.=(Directed J).insloc 0 by SCMFSA8A:16,28
.=goto insloc card J by SCMFSA8A:16,30;
thus while>0(a,I).insloc 2 = (if>0(a, I1, J) +* f).insloc 2 by Def2
.= (Directed Mi +* ProgramPart Relocated(J1, 2)).insloc 2 by A2,A3,A4,A8,
FUNCT_4:def 1
.= (ProgramPart Relocated(J1,2)).insloc 2 by A5,A9,A10,FUNCT_4:def 1
.= IncAddr(Shift(ProgramPart(J1),2),2).insloc 2 by SCMFSA_5:2
.= IncAddr(Shift(J1,2),2).insloc 2 by AMI_5:72
.= IncAddr(goto insloc card J,2) by A13,A14,SCMFSA_4:24
.= goto (insloc 1 + 2) by SCMFSA8A:17,SCMFSA_4:14
.= goto insloc (1+2) by SCMFSA_4:def 1
.= goto insloc 3;
end;
theorem
for a being Int-Location, I being Macro-Instruction,k being Nat st
k < card I +6 holds insloc k in dom while>0(a,I)
proof
let a be Int-Location, I be Macro-Instruction,k be Nat;
assume A1: k < card I +6;
card while>0(a,I) = card I + 6 by Th5;
hence thesis by A1,SCMFSA6A:15;
end;
theorem Th43:
for s being State of SCM+FSA, I being Macro-Instruction,
a being read-write Int-Location
st s.a <= 0 holds
while>0(a,I) is_halting_on s & while>0(a,I) is_closed_on s
proof
let s be State of SCM+FSA;
let I be Macro-Instruction;
let a be read-write Int-Location;
assume A1: s.a <= 0;
set s1 = s +* (while>0(a,I) +* Start-At insloc 0);
set s2 = (Computation s1).1;
set s3 = (Computation s1).2;
set s4 = (Computation s1).3;
set s5 = (Computation s1).4;
set C1 = Computation s1;
set i = a >0_goto insloc 4;
A2: insloc 0 in dom while>0(a,I) by Th10;
while>0(a,I) c= while>0(a,I) +* Start-At insloc 0 by SCMFSA8A:9;
then A3: dom while>0(a,I) c= dom (while>0(a,I) +* Start-At insloc 0)
by GRFUNC_1:8;
A4: IC SCM+FSA in dom (while>0(a,I) +* Start-At insloc 0) by SF_MASTR:65;
A5: IC s1 = s1.IC SCM+FSA by AMI_1:def 15
.= (while>0(a,I) +* Start-At insloc 0).IC SCM+FSA by A4,FUNCT_4:14
.= insloc 0 by SF_MASTR:66;
s1.insloc 0 = (while>0(a,I) +* Start-At insloc 0).insloc 0 by A2,A3,
FUNCT_4:14
.= while>0(a,I).insloc 0 by A2,SCMFSA6B:7
.= i by Th11;
then A6: CurInstr s1 = i by A5,AMI_1:def 17;
A7: (Computation s1).(0 + 1) = Following (Computation s1).0 by AMI_1:def 19
.= Following s1 by AMI_1:def 19
.= Exec(i,s1) by A6,AMI_1:def 18;
not a in dom (while>0(a,I) +* Start-At insloc 0) & a in dom s
by SCMFSA6B:12,SCMFSA_2:66;
then A8: s1.a = s.a by FUNCT_4:12;
A9: IC C1.1 = C1.1.IC SCM+FSA by AMI_1:def 15
.= Next insloc 0 by A1,A5,A7,A8,SCMFSA_2:97
.= insloc (0 + 1) by SCMFSA_2:32;
A10: insloc 1 in dom while>0(a,I) by Th10;
C1.1.insloc 1 = s1.insloc 1 by AMI_1:54
.= (while>0(a,I) +* Start-At insloc 0).insloc 1 by A3,A10,FUNCT_4:14
.= while>0(a,I).insloc 1 by A10,SCMFSA6B:7
.= goto insloc 2 by Th11;
then A11: CurInstr C1.1 = goto insloc 2 by A9,AMI_1:def 17;
A12: (Computation s1).(1 + 1) = Following s2 by AMI_1:def 19
.= Exec(goto insloc 2,s2) by A11,AMI_1:def 18;
A13: insloc 2 in dom while>0(a,I) by Th37;
A14: IC s3 = s3.IC SCM+FSA by AMI_1:def 15
.= insloc 2 by A12,SCMFSA_2:95;
s3.insloc 2 = s1.insloc 2 by AMI_1:54
.= (while>0(a,I) +* Start-At insloc 0).insloc 2 by A3,A13,FUNCT_4:14
.= while>0(a,I).insloc 2 by A13,SCMFSA6B:7
.= goto insloc 3 by Th41;
then A15: CurInstr s3 = goto insloc 3 by A14,AMI_1:def 17;
A16: (Computation s1).(2 + 1) = Following s3 by AMI_1:def 19
.= Exec(goto insloc 3,s3) by A15,AMI_1:def 18;
A17: insloc 3 in dom while>0(a,I) by Th37;
set loc5= insloc (card I +5);
A18: IC s4 = s4.IC SCM+FSA by AMI_1:def 15
.= insloc 3 by A16,SCMFSA_2:95;
s4.insloc 3 = s1.insloc 3 by AMI_1:54
.= (while>0(a,I) +* Start-At insloc 0).insloc 3 by A3,A17,FUNCT_4:14
.= while>0(a,I).insloc 3 by A17,SCMFSA6B:7
.= goto loc5 by Th40;
then A19: CurInstr s4 = goto loc5 by A18,AMI_1:def 17;
A20: (Computation s1).(3 + 1) = Following s4 by AMI_1:def 19
.= Exec(goto loc5,s4) by A19,AMI_1:def 18;
A21: loc5 in dom while>0(a,I) by Th38;
A22: IC s5 = s5.IC SCM+FSA by AMI_1:def 15
.= loc5 by A20,SCMFSA_2:95;
s5.loc5 = s1.loc5 by AMI_1:54
.= (while>0(a,I) +* Start-At insloc 0).loc5 by A3,A21,FUNCT_4:14
.= while>0(a,I).loc5 by A21,SCMFSA6B:7
.= halt SCM+FSA by Th39;
then A23: CurInstr s5 = halt SCM+FSA by A22,AMI_1:def 17;
then s1 is halting by AMI_1:def 20;
hence while>0(a,I) is_halting_on s by SCMFSA7B:def 8;
now let k be Nat;
A24: k<=3 or k >= 3+1 by NAT_1:38;
per cases by A24,CQC_THE1:4;
suppose k = 0;
hence IC C1.k in dom while>0(a,I) by A2,A5,AMI_1:def 19;
suppose k = 1;
hence IC C1.k in dom while>0(a,I) by A9,Th10;
suppose k = 2;
hence IC C1.k in dom while>0(a,I) by A14,Th37;
suppose k = 3;
hence IC C1.k in dom while>0(a,I) by A18,Th37;
suppose k >= 4;
hence IC C1.k in dom while>0(a,I) by A21,A22,A23,AMI_1:52;
end;
hence while>0(a,I) is_closed_on s by SCMFSA7B:def 7;
end;
set D = Int-Locations \/ FinSeq-Locations;
theorem Th44:
for a being Int-Location, I being Macro-Instruction,
s being State of SCM+FSA,k being Nat st
I is_closed_on s & I is_halting_on s &
k < LifeSpan (s +* (I +* Start-At insloc 0)) &
IC (Computation (s +* (while>0(a,I) +* Start-At insloc 0))).(1 + k) =
IC (Computation (s +* ( I +* Start-At insloc 0))).k + 4 &
(Computation (s +* (while>0(a,I) +* Start-At insloc 0))).(1 + k) | D =
(Computation (s +* ( I +* Start-At insloc 0))).k | D
holds
IC (Computation (s +* (while>0(a,I) +* Start-At insloc 0))).(1 + k+1) =
IC (Computation (s +* (I +* Start-At insloc 0))).(k+1) + 4 &
(Computation (s +* (while>0(a,I) +* Start-At insloc 0))).(1 + k+1) | D =
(Computation (s +* (I +* Start-At insloc 0))).(k+1) | D
proof
let a be Int-Location;
let I be Macro-Instruction;
let s be State of SCM+FSA;
let k be Nat;
set s1 = s +* (while>0(a,I) +* Start-At insloc 0);
set sI = s +* ( I +* Start-At insloc 0);
set sK1=(Computation s1).(1 + k);
set sK2= (Computation sI).k;
set l3=IC (Computation sI).k;
assume A1: I is_closed_on s;
assume A2: I is_halting_on s;
assume A3: k < LifeSpan sI;
assume A4: IC (Computation s1).(1 + k)=l3 + 4;
assume A5:sK1 | D = sK2 | D;
set I1= I ';' Goto insloc 0;
set J = SCM+FSA-Stop;
set f = insloc (card I +4) .--> goto insloc 0;
set i = a >0_goto insloc (card J + 3);
A6: dom f = {insloc (card I + 4)} by CQC_LANG:5;
consider n being Nat such that A7: l3 = insloc n by SCMFSA_2:21;
A8: insloc n in dom I by A1,A7,SCMFSA7B:def 7;
then A9: n < card I by SCMFSA6A:15;
then n + 4 <> card I + 4 by XCMPLX_1:2;
then insloc (n + 4) <> insloc (card I + 4) by SCMFSA_2:18;
then A10: not insloc (n+4) in dom f by A6,TARSKI:def 1;
A11: n+4 < card I+ 6 by A9,REAL_1:67;
card while>0(a,I) = card I + 6 by Th5;
then A12: insloc (n+4) in dom while>0(a,I) by A11,SCMFSA6A:15;
while>0(a,I) = if>0(a, I1, J) +* f by Def2;
then A13: dom while>0(a,I) = dom if>0(a,I1,J) \/ dom f by FUNCT_4:def 1;
then A14: insloc (n+4) in dom if>0(a,I1,J) by A10,A12,XBOOLE_0:def 2;
set Mi= i ';' J ';' Goto insloc (card I1 + 1);
set J2= I1 ';' SCM+FSA-Stop;
set J3= Goto insloc 0 ';' SCM+FSA-Stop;
A15: card Mi = card (i ';' J )+ card Goto insloc (card I1 + 1) by SCMFSA6A:61
.= card (i ';' J ) + 1 by SCMFSA8A:29
.= card (Macro i ';' J) + 1 by SCMFSA6A:def 5
.= card (Macro i) + card J + 1 by SCMFSA6A:61
.= 2 + 1 +1 by SCMFSA7B:6,SCMFSA8A:17
.= 3+ 1;
then n+4 >= card Mi by NAT_1:29;
then A16: not insloc (n+4) in dom Mi by SCMFSA6A:15;
A17: if>0(a, I1, J)
= Mi ';' I1 ';' SCM+FSA-Stop by SCMFSA8B:def 2
.= Mi ';' J2 by SCMFSA6A:62
.= Directed Mi +* ProgramPart Relocated(J2, 4) by A15,SCMFSA6A:def 4;
then A18: dom if>0(a,I1,J) = dom Directed Mi \/ dom ProgramPart Relocated(J2, 4
)
by FUNCT_4:def 1;
then dom if>0(a,I1,J)
= dom Mi \/ dom ProgramPart Relocated(J2, 4) by SCMFSA6A:14;
then A19: insloc (n+4) in dom ProgramPart Relocated(J2, 4) by A14,A16,XBOOLE_0:
def 2
;
A20: insloc n + 4 = insloc ( n + 4) by SCMFSA_4:def 1;
while>0(a,I) c= while>0(a,I) +* Start-At insloc 0 by SCMFSA8A:9;
then A21: dom while>0(a,I) c= dom (while>0(a,I) +* Start-At insloc 0)
by GRFUNC_1:8;
I c= I +* Start-At insloc 0 by SCMFSA8A:9;
then A22: dom I c= dom (I +* Start-At insloc 0) by GRFUNC_1:8;
A23: CurInstr sK2 =sK2.insloc n by A7,AMI_1:def 17
.=sI.insloc n by AMI_1:54
.=(I +* Start-At insloc 0).insloc n by A8,A22,FUNCT_4:14
.= I.insloc n by A8,SCMFSA6B:7;
sI is halting by A2,SCMFSA7B:def 8;
then A24: I.insloc n <> halt SCM+FSA by A3,A23,SCM_1:def 2;
A25: J2= I ';' J3 by SCMFSA6A:62;
then J2= Directed I +* ProgramPart Relocated(J3, card I) by SCMFSA6A:def 4
;
then dom J2 = dom Directed I \/ dom ProgramPart Relocated(J3, card I)
by FUNCT_4:def 1
.= dom I \/ dom ProgramPart Relocated(J3, card I) by SCMFSA6A:14;
then A26: insloc n in dom J2 by A8,XBOOLE_0:def 2;
then insloc n + 4 in { il+4 where il is Instruction-Location of SCM+FSA:
il in dom J2};
then A27: insloc (n+4) in dom Shift(J2,4) by A20,SCMFSA_4:31;
then A28: pi(Shift(J2,4),insloc (n+4)) =Shift(J2,4).(insloc n +4) by A20,AMI_5:
def 5
.=J2.insloc n by A26,SCMFSA_4:30
.=(Directed I).insloc n by A8,A25,SCMFSA8A:28
.=I.insloc n by A8,A24,SCMFSA8A:30;
A29: I.insloc n in rng I by A8,FUNCT_1:def 5;
rng I c= the Instructions of SCM+FSA by SCMFSA_4:1;
then reconsider j = I.insloc n as Instruction of SCM+FSA by A29;
sK1.insloc (n+4) = s1.insloc(n+4) by AMI_1:54
.= (while>0(a,I) +* Start-At insloc 0).insloc (n+4) by A12,A21,FUNCT_4:14
.= while>0(a,I).insloc (n+4) by A12,SCMFSA6B:7
.= (if>0(a, I1, J) +* f).insloc (n+4) by Def2
.= (Directed Mi +* ProgramPart Relocated(J2, 4)).insloc (n+4) by A10,A12,
A13,A17,FUNCT_4:def 1
.= (ProgramPart Relocated(J2,4)).insloc (n+4) by A14,A18,A19,FUNCT_4:def 1
.= IncAddr(Shift(ProgramPart(J2),4),4).insloc (n+4) by SCMFSA_5:2
.= IncAddr(Shift(J2,4),4).insloc (n+4) by AMI_5:72
.= IncAddr(j,4) by A27,A28,SCMFSA_4:24;
then A30: CurInstr sK1 =IncAddr(j,4) by A4,A7,A20,AMI_1:def 17;
A31: (Computation s1).(1 + k+1) = Following sK1 by AMI_1:def 19
.= Exec(IncAddr(j,4),sK1) by A30,AMI_1:def 18;
(Computation sI).(k+1) = Following sK2 by AMI_1:def 19
.= Exec(j,sK2) by A23,AMI_1:def 18;
hence thesis by A4,A5,A31,SCMFSA6A:41;
end;
theorem Th45:
for a being Int-Location, I being Macro-Instruction,
s being State of SCM+FSA st
I is_closed_on s & I is_halting_on s &
IC (Computation (s +* (while>0(a,I) +* Start-At insloc 0))).(1 +
LifeSpan (s +* (I +* Start-At insloc 0 ) ) ) =
IC (Computation (s +* ( I +* Start-At insloc 0))).
LifeSpan (s +* (I +* Start-At insloc 0 ) ) + 4
holds
CurInstr (Computation (s +* (while>0(a,I) +* Start-At insloc 0))).(1 +
LifeSpan (s +* (I +* Start-At insloc 0)) ) = goto insloc (card I +4)
proof
let a be Int-Location;
let I be Macro-Instruction;
let s be State of SCM+FSA;
set s1 = s +* (while>0(a,I) +* Start-At insloc 0);
set sI = s +* ( I +* Start-At insloc 0);
set life=LifeSpan (s +* (I +* Start-At insloc 0));
set sK1=(Computation s1).(1 + life);
set sK2= (Computation sI).life;
assume A1: I is_closed_on s;
assume A2: I is_halting_on s;
assume A3: IC sK1 = IC sK2 + 4;
set I1= I ';' Goto insloc 0;
set J = SCM+FSA-Stop;
set f = insloc (card I +4) .--> goto insloc 0;
set i = a >0_goto insloc (card J + 3);
A4: dom f = {insloc (card I + 4)} by CQC_LANG:5;
consider n being Nat such that A5: IC sK2 = insloc n by SCMFSA_2:21;
A6: insloc n in dom I by A1,A5,SCMFSA7B:def 7;
then A7: n < card I by SCMFSA6A:15;
then n + 4 <> card I + 4 by XCMPLX_1:2;
then insloc (n + 4) <> insloc (card I + 4) by SCMFSA_2:18;
then A8: not insloc (n+4) in dom f by A4,TARSKI:def 1;
A9: n+4 < card I+ 6 by A7,REAL_1:67;
card while>0(a,I) = card I + 6 by Th5;
then A10: insloc (n+4) in dom while>0(a,I) by A9,SCMFSA6A:15;
while>0(a,I) = if>0(a, I1, J) +* f by Def2;
then A11: dom while>0(a,I) = dom if>0(a,I1,J) \/ dom f by FUNCT_4:def 1;
then A12: insloc (n+4) in dom if>0(a,I1,J) by A8,A10,XBOOLE_0:def 2;
set Mi= i ';' J ';' Goto insloc (card I1 + 1);
set J2= I1 ';' SCM+FSA-Stop;
set J3= Goto insloc 0 ';' SCM+FSA-Stop;
A13: card Mi = card (i ';' J )+ card Goto insloc (card I1 + 1) by SCMFSA6A:61
.= card (i ';' J ) + 1 by SCMFSA8A:29
.= card (Macro i ';' J) + 1 by SCMFSA6A:def 5
.= card (Macro i) + card J + 1 by SCMFSA6A:61
.= 2 + 1 +1 by SCMFSA7B:6,SCMFSA8A:17
.= 3+ 1;
then n+4 >= card Mi by NAT_1:29;
then A14: not insloc (n+4) in dom Mi by SCMFSA6A:15;
A15: if>0(a, I1, J) = Mi ';' I1 ';' SCM+FSA-Stop by SCMFSA8B:def 2
.= Mi ';' J2 by SCMFSA6A:62
.= Directed Mi +* ProgramPart Relocated(J2, 4) by A13,SCMFSA6A:def 4;
then A16: dom if>0(a,I1,J) = dom Directed Mi \/ dom ProgramPart Relocated(J2, 4
)
by FUNCT_4:def 1;
then dom if>0(a,I1,J)
= dom Mi \/ dom ProgramPart Relocated(J2, 4) by SCMFSA6A:14;
then A17: insloc (n+4) in dom ProgramPart Relocated(J2, 4) by A12,A14,XBOOLE_0:
def 2
;
A18: insloc n + 4 = insloc ( n + 4) by SCMFSA_4:def 1;
while>0(a,I) c= while>0(a,I) +* Start-At insloc 0 by SCMFSA8A:9;
then A19: dom while>0(a,I) c= dom (while>0(a,I) +* Start-At insloc 0)
by GRFUNC_1:8;
I c= I +* Start-At insloc 0 by SCMFSA8A:9;
then A20: dom I c= dom (I +* Start-At insloc 0) by GRFUNC_1:8;
A21: CurInstr sK2 =sK2.insloc n by A5,AMI_1:def 17
.=sI.insloc n by AMI_1:54
.=(I +* Start-At insloc 0).insloc n by A6,A20,FUNCT_4:14
.= I.insloc n by A6,SCMFSA6B:7;
sI is halting by A2,SCMFSA7B:def 8;
then A22: I.insloc n = halt SCM+FSA by A21,SCM_1:def 2;
A23: J2= I ';' J3 by SCMFSA6A:62;
then J2= Directed I +* ProgramPart Relocated(J3, card I) by SCMFSA6A:def 4
;
then dom J2 = dom Directed I \/ dom ProgramPart Relocated(J3, card I)
by FUNCT_4:def 1
.= dom I \/ dom ProgramPart Relocated(J3, card I) by SCMFSA6A:14;
then A24: insloc n in dom J2 by A6,XBOOLE_0:def 2;
then insloc n + 4 in { il+4 where il is Instruction-Location of SCM+FSA:
il in dom J2};
then A25: insloc (n+4) in dom Shift(J2,4) by A18,SCMFSA_4:31;
then A26: pi(Shift(J2,4),insloc (n+4)) =Shift(J2,4).(insloc n +4) by A18,AMI_5:
def 5
.=J2.insloc n by A24,SCMFSA_4:30
.=(Directed I).insloc n by A6,A23,SCMFSA8A:28
.=goto insloc card I by A6,A22,SCMFSA8A:30;
sK1.insloc (n+4) = s1.insloc(n+4) by AMI_1:54
.= (while>0(a,I) +* Start-At insloc 0).insloc (n+4) by A10,A19,FUNCT_4:14
.= while>0(a,I).insloc (n+4) by A10,SCMFSA6B:7
.= (if>0(a, I1, J) +* f).insloc (n+4) by Def2
.= (Directed Mi +* ProgramPart Relocated(J2, 4)).insloc (n+4) by A8,A10,A11
,A15,FUNCT_4:def 1
.= (ProgramPart Relocated(J2,4)).insloc (n+4) by A12,A16,A17,FUNCT_4:def 1
.= IncAddr(Shift(ProgramPart(J2),4),4).insloc (n+4) by SCMFSA_5:2
.= IncAddr(Shift(J2,4),4).insloc (n+4) by AMI_5:72
.= IncAddr(goto insloc card I,4) by A25,A26,SCMFSA_4:24
.= goto (insloc card I+4) by SCMFSA_4:14
.= goto insloc (card I+4) by SCMFSA_4:def 1;
hence thesis by A3,A5,A18,AMI_1:def 17;
end;
theorem Th46:
for a being Int-Location, I being Macro-Instruction holds
while>0(a,I).insloc (card I +4) = goto insloc 0
proof
let a be Int-Location;
let I be Macro-Instruction;
set I1= I ';' Goto insloc 0;
set J = SCM+FSA-Stop;
set f = insloc (card I +4) .--> goto insloc 0;
set Lc4=insloc (card I + 4 );
dom f = {Lc4} by CQC_LANG:5;
then A1: Lc4 in dom f by TARSKI:def 1;
A2: Lc4 in dom while>0(a,I) by Th38;
while>0(a,I) = if>0(a, I1, J) +* f by Def2;
then A3: dom while>0(a,I) = dom if>0(a,I1,J) \/ dom f by FUNCT_4:def 1;
thus while>0(a,I).Lc4 = (if>0(a, I1, J) +* f).Lc4 by Def2
.= f.Lc4 by A1,A2,A3,FUNCT_4:def 1
.=goto insloc 0 by CQC_LANG:6;
end;
theorem Th47:
for s being State of SCM+FSA, I being Macro-Instruction,
a being read-write Int-Location
st I is_closed_on s & I is_halting_on s & s.a >0 holds
IC (Computation (s +* (while>0(a,I) +* Start-At insloc 0))).
(LifeSpan (s +* (I +* Start-At insloc 0)) + 3) = insloc 0 &
for k being Nat st k <= LifeSpan (s +* (I +* Start-At insloc 0)) + 3
holds IC (Computation (s +* (while>0(a,I) +* Start-At insloc 0))).k
in dom while>0(a,I)
proof
let s be State of SCM+FSA;
let I be Macro-Instruction;
let a be read-write Int-Location;
assume A1: I is_closed_on s;
assume A2: I is_halting_on s;
assume A3: s.a > 0;
set s1 = s +* (while>0(a,I) +* Start-At insloc 0);
set s2 = (Computation s1).1;
set C1 = Computation s1;
set i = a >0_goto insloc 4;
set sI = s +* (I +* Start-At insloc 0);
A4: insloc 0 in dom while>0(a,I) by Th10;
while>0(a,I) c= while>0(a,I) +* Start-At insloc 0 by SCMFSA8A:9;
then A5: dom while>0(a,I) c= dom (while>0(a,I) +* Start-At insloc 0)
by GRFUNC_1:8;
A6: IC SCM+FSA in dom (while>0(a,I) +* Start-At insloc 0) by SF_MASTR:65;
A7: IC s1 = s1.IC SCM+FSA by AMI_1:def 15
.= (while>0(a,I) +* Start-At insloc 0).IC SCM+FSA by A6,FUNCT_4:14
.= insloc 0 by SF_MASTR:66;
s1.insloc 0 = (while>0(a,I) +* Start-At insloc 0).insloc 0
by A4,A5,FUNCT_4:14
.= while>0(a,I).insloc 0 by A4,SCMFSA6B:7
.= i by Th11;
then A8: CurInstr s1 = i by A7,AMI_1:def 17;
A9: (Computation s1).(0 + 1) = Following (Computation s1).0 by AMI_1:def 19
.= Following s1 by AMI_1:def 19
.= Exec(i,s1) by A8,AMI_1:def 18;
not a in dom (while>0(a,I) +* Start-At insloc 0) & a in dom s
by SCMFSA6B:12,SCMFSA_2:66;
then A10: s1.a = s.a by FUNCT_4:12;
A11: IC s2 = s2.IC SCM+FSA by AMI_1:def 15
.= insloc 4 by A3,A9,A10,SCMFSA_2:97;
(for c holds s2.c = s1.c) & for f holds s2.f = s1.f
by A9,SCMFSA_2:97;
then A12: s2 | D = s1 | D by SCMFSA6A:38
.= s | D by SCMFSA8A:11
.= sI | D by SCMFSA8A:11;
defpred P[Nat] means
$1 <= LifeSpan sI implies
IC (Computation s1).(1 + $1) = IC (Computation sI).$1 + 4 &
(Computation s1).(1 + $1) | D = (Computation sI).$1 | D;
A13: P[0]
proof assume 0 <= LifeSpan sI;
A14: IC SCM+FSA in dom (I +* Start-At insloc 0) by SF_MASTR:65;
IC (Computation sI).0 = IC sI by AMI_1:def 19
.= sI.IC SCM+FSA by AMI_1:def 15
.= (I +* Start-At insloc 0).IC SCM+FSA by A14,FUNCT_4:14
.= insloc 0 by SF_MASTR:66;
then IC (Computation sI).0 + 4 = insloc (0+ 4) by SCMFSA_4:def 1;
hence IC (Computation s1).(1 + 0) = IC (Computation sI).0 + 4 &
(Computation s1).(1 + 0) | D = (Computation sI).0 | D by A11,A12,AMI_1:
def 19;
end;
A15: now let k be Nat;
assume A16: P[k];
now assume A17: k + 1 <= LifeSpan sI;
k + 0 < k + 1 by REAL_1:53;
then k < LifeSpan sI by A17,AXIOMS:22;
hence
IC (Computation s1).(1 + k+1) = IC (Computation sI).(k+1) + 4 &
(Computation s1).(1 + k+1) | D = (Computation sI).(k+1) | D
by A1,A2,A16,Th44;
end;
hence P[k + 1];
end;
set s2=(Computation s1).(1 + LifeSpan sI);
set loc4=insloc (card I + 4);
set s3=(Computation s1).(1+LifeSpan sI+1);
A18: for k being Nat holds P[k] from Ind(A13,A15);
then P[LifeSpan sI];
then A19: CurInstr s2 = goto loc4 by A1,A2,Th45;
A20: s3 = Following s2 by AMI_1:def 19
.= Exec(goto loc4,s2) by A19,AMI_1:def 18;
A21: loc4 in dom while>0(a,I) by Th38;
A22: IC s3 = s3.IC SCM+FSA by AMI_1:def 15
.= loc4 by A20,SCMFSA_2:95;
set s4=(Computation s1).(1+LifeSpan sI+1+1);
s3.loc4 = s1.loc4 by AMI_1:54
.= (while>0(a,I) +* Start-At insloc 0).loc4 by A5,A21,FUNCT_4:14
.= while>0(a,I).loc4 by A21,SCMFSA6B:7
.= goto insloc 0 by Th46;
then A23: CurInstr s3 = goto insloc 0 by A22,AMI_1:def 17;
A24: s4 = Following s3 by AMI_1:def 19
.= Exec(goto insloc 0,s3) by A23,AMI_1:def 18;
A25: IC s4 = s4.IC SCM+FSA by AMI_1:def 15
.= insloc 0 by A24,SCMFSA_2:95;
A26: LifeSpan sI+1+1+1 = LifeSpan sI+(1+1)+1 by XCMPLX_1:1
.=LifeSpan sI+(2+1) by XCMPLX_1:1; hence
IC (Computation s1).(LifeSpan sI+3) = insloc 0 by A25;
A27: now let k be Nat;
assume A28: k <= LifeSpan sI+3;
assume k<>0;
then consider n being Nat such that
A29: k = n+ 1 by NAT_1:22;
k<=LifeSpan sI+1 or k >= LifeSpan sI+1+1 by NAT_1:38;
then A30: k<=LifeSpan sI+1 or k = LifeSpan sI+1+1 or k > LifeSpan sI+1+1
by REAL_1:def 5;
per cases by A26,A30,NAT_1:38;
suppose k<=LifeSpan sI+1;
then n <= LifeSpan sI by A29,REAL_1:53;
then A31: IC C1.(1 + n) = IC (Computation sI).n + 4 by A18;
consider m being Nat such that A32: IC (Computation sI).n = insloc m
by SCMFSA_2:21;
insloc m in dom I by A1,A32,SCMFSA7B:def 7;
then m < card I by SCMFSA6A:15;
then A33: m+4 < card I+ 6 by REAL_1:67;
card while>0(a,I) = card I + 6 by Th5;
then insloc (m+4) in dom while>0(a,I) by A33,SCMFSA6A:15;
hence IC C1.k in dom while>0(a,I) by A29,A31,A32,SCMFSA_4:def 1;
suppose k=LifeSpan sI+1+1;
hence IC C1.k in dom while>0(a,I) by A22,Th38;
suppose k >= LifeSpan sI+3;
then k = LifeSpan sI+3 by A28,AXIOMS:21;
hence IC C1.k in dom while>0(a,I) by A25,A26,Th10;
end;
now let k be Nat;
assume A34: k <= LifeSpan sI+3;
per cases;
suppose k = 0;
hence IC C1.k in dom while>0(a,I) by A4,A7,AMI_1:def 19;
suppose k <>0;
hence IC C1.k in dom while>0(a,I) by A27,A34;
end;hence
for k being Nat st k <= LifeSpan sI + 3 holds IC C1.k in dom while>0(a,I
);
end;
set sl0= Start-At insloc 0;
reserve s for State of SCM+FSA,
I for Macro-Instruction,
a for read-write Int-Location;
definition
let s,I,a;
deffunc U(Nat,Element of product the Object-Kind of SCM+FSA) =
(Computation ($2 +* (while>0(a,I) +* sl0))).
(LifeSpan ($2 +* (I +* sl0)) + 3);
func StepWhile>0(a,I,s) -> Function of NAT,product the Object-Kind of SCM+FSA
means :Def5:
it.0 = s & for i being Nat holds
it.(i+1)=(Computation (it.i +* (while>0(a,I) +* sl0))).
(LifeSpan (it.i +* (I +* sl0)) + 3);
existence
proof
thus ex f being Function of NAT,product the Object-Kind of SCM+FSA st
f.0 = s & for i being Nat holds f.(i+1)= U(i,f.i) from LambdaRecExD;
end;
uniqueness
proof let F1,F2 be Function of NAT,product the Object-Kind of SCM+FSA
such that
A1: F1.0 = s & for i being Nat holds F1.(i+1)= U(i,F1.i) and
A2: F2.0 = s & for i being Nat holds F2.(i+1)= U(i,F2.i);
thus F1 = F2 from LambdaRecUnD(A1,A2);
end;
end;
canceled 2;
theorem Th50:
StepWhile>0(a,I,s).(k+1)=StepWhile>0(a,I,StepWhile>0(a,I,s).k).1
proof
set sk=StepWhile>0(a,I,s).k;
set sk0=StepWhile>0(a,I,sk).0;
sk0=sk by Def5;
hence StepWhile>0(a,I,s).(k+1) =(Computation (sk0 +*(while>0(a,I) +* sl0))
).
(LifeSpan (sk0 +* (I +* sl0)) + 3) by Def5
.=StepWhile>0(a,I,sk).(0+1) by Def5
.=StepWhile>0(a,I,sk).1;
end;
theorem Th51:
for I being Macro-Instruction,a being read-write Int-Location,
s being State of SCM+FSA holds
StepWhile>0(a,I,s).(0+1)=(Computation (s +* (while>0(a,I) +* sl0))).
(LifeSpan (s+* (I +* sl0)) + 3)
proof
let I be Macro-Instruction,a be read-write Int-Location,
s be State of SCM+FSA;
thus StepWhile>0(a,I,s).(0+1)=(Computation (StepWhile>0(a,I,s).0 +*
(while>0(a,I) +* sl0))).(LifeSpan (StepWhile>0(a,I,s).0 +*
(I +* sl0)) + 3) by Def5
.=(Computation (s +* (while>0(a,I) +* sl0)))
.(LifeSpan (StepWhile>0(a,I,s).0+* (I +* sl0)) + 3) by Def5
.=(Computation (s +* (while>0(a,I) +* sl0)))
.(LifeSpan (s+* (I +* sl0)) + 3) by Def5;
end;
theorem Th52:
for I being Macro-Instruction,a being read-write Int-Location,
s being State of SCM+FSA,k,n being Nat st
IC StepWhile>0(a,I,s).k =insloc 0 & StepWhile>0(a,I,s).k=
(Computation (s +* (while>0(a,I) +* Start-At insloc 0))).n holds
StepWhile>0(a,I,s).k = StepWhile>0(a,I,s).k +* (while>0(a,I)+*
Start-At insloc 0) &
StepWhile>0(a,I,s).(k+1)=(Computation (s +* (while>0(a,I) +*
Start-At insloc 0))).
(n +(LifeSpan (StepWhile>0(a,I,s).k +* (I +* Start-At insloc 0)) + 3))
proof
let I be Macro-Instruction,a be read-write Int-Location,
s be State of SCM+FSA,k,n be Nat;
set s1 = s +* (while>0(a,I) +* Start-At insloc 0);
set sk=StepWhile>0(a,I,s).k;
set s2=sk +* (while>0(a,I)+* sl0);
assume A1:IC sk =insloc 0;
assume A2:sk =(Computation s1).n;
A3: IC SCM+FSA in dom (while>0(a,I) +* sl0 ) by SF_MASTR:65;
A4: IC s2 = s2.IC SCM+FSA by AMI_1:def 15
.= (while>0(a,I) +* sl0).IC SCM+FSA by A3,FUNCT_4:14
.= IC sk by A1,SF_MASTR:66;
A5: s2 | D = sk | D by SCMFSA8A:11;
sk | IL =s1 | IL by A2,SCMFSA6B:17;
then s2 | IL = sk | IL by Th27;hence
s2=sk by A4,A5,Th29;
hence
StepWhile>0(a,I,s).(k+1)=
(Computation sk).(LifeSpan (sk +* (I +* sl0)) + 3) by Def5
.=(Computation s1).(n +(LifeSpan (sk +* (I +* sl0)) + 3)) by A2,AMI_1:51;
end;
theorem Th53:
for I being Macro-Instruction,a being read-write Int-Location,
s being State of SCM+FSA st (for k being Nat holds
I is_closed_on StepWhile>0(a,I,s).k &
I is_halting_on StepWhile>0(a,I,s).k) &
ex f being Function of product the Object-Kind of SCM+FSA,NAT st
(for k being Nat holds (f.(StepWhile>0(a,I,s).(k+1)) <
f.(StepWhile>0(a,I,s).k)
or f.(StepWhile>0(a,I,s).k) = 0) &
( f.(StepWhile>0(a,I,s).k)=0 iff (StepWhile>0(a,I,s).k).a <= 0 ) )
holds
while>0(a,I) is_halting_on s & while>0(a,I) is_closed_on s
proof
let I be Macro-Instruction,a be read-write Int-Location,
s be State of SCM+FSA;
assume A1: for k being Nat holds I is_closed_on StepWhile>0(a,I,s).k &
I is_halting_on StepWhile>0(a,I,s).k;
given f being Function of product the Object-Kind of SCM+FSA,NAT
such that A2:for k being Nat holds
(f.(StepWhile>0(a,I,s).(k+1)) < f.(StepWhile>0(a,I,s).k) or
f.(StepWhile>0(a,I,s).k) = 0) &
( f.(StepWhile>0(a,I,s).k)=0 iff (StepWhile>0(a,I,s).k).a <= 0 );
deffunc F(Nat) = f.(StepWhile>0(a,I,s).$1);
set s1 = s +* (while>0(a,I) +* Start-At insloc 0);
A3: F(0) =f.s by Def5;
A4: for k holds ( F(k+1) < F(k) or F(k) = 0 ) by A2;
consider m being Nat such that
A5: F(m)=0 and
A6: for n st F(n) =0 holds m <= n from MinIndex(A3,A4);
defpred P[Nat] means
$1+1 <= m implies
ex k st StepWhile>0(a,I,s).($1+1)=(Computation s1).k;
A7: P[0]
proof assume 0+1 <= m;
take n=(LifeSpan (s+* (I +* sl0)) + 3);
thus StepWhile>0(a,I,s).(0+1)=(Computation s1).n by Th51;
end;
A8: IC SCM+FSA in dom (while>0(a,I) +* sl0 ) by SF_MASTR:65;
A9: now let k be Nat;
assume A10: P[k];
now assume A11: (k+1)+ 1 <= m;
k + 0 < k+ (1+ 1) by REAL_1:53;
then k < (k+1) +1 by XCMPLX_1:1;
then A12: k < m by A11,AXIOMS:22;
A13: (k+1)+ 0 < (k+ 1)+ 1 by REAL_1:53;
set sk=StepWhile>0(a,I,s).k;
set sk1=StepWhile>0(a,I,s).(k+1);
consider n being Nat such that
A14: sk1 = (Computation s1).n by A10,A11,A13,AXIOMS:22;
A15: sk1= (Computation (sk +* (while>0(a,I)+* sl0))).
(LifeSpan (sk +* (I +* sl0)) + 3) by Def5;
A16: I is_closed_on sk & I is_halting_on sk by A1;
F(k) <> 0 by A6,A12;
then sk.a > 0 by A2;
then A17: IC sk1 =insloc 0 by A15,A16,Th47;
take m=n +(LifeSpan (sk1 +* (I +* sl0)) + 3);
thus StepWhile>0(a,I,s).((k+1)+1)=(Computation s1).m
by A14,A17,Th52;
end;
hence P[k+1];
end;
A18: for k being Nat holds P[k] from Ind(A7,A9);
now per cases;
suppose m=0;
then (StepWhile>0(a,I,s).0).a <= 0 by A2,A5;
then s.a <= 0 by Def5;
hence while>0(a,I) is_halting_on s & while>0(a,I) is_closed_on s
by Th43;
suppose A19:m<>0;
then consider i being Nat such that
A20: m=i+1 by NAT_1:22;
set si=StepWhile>0(a,I,s).i;
set sm=StepWhile>0(a,I,s).m;
set sm1=sm +* (while>0(a,I)+* sl0);
consider n being Nat such that
A21: sm = (Computation s1).n by A18,A20;
A22: sm.a <= 0 by A2,A5;
A23: sm= (Computation (si +* (while>0(a,I)+* sl0))).
(LifeSpan (si +* (I +* sl0)) + 3) by A20,Def5;
A24: I is_closed_on si & I is_halting_on si by A1;
i < m by A20,NAT_1:38;
then F(i) <> 0 by A6;
then si.a > 0 by A2;
then A25: IC sm =insloc 0 by A23,A24,Th47;
A26: IC sm1 = sm1.IC SCM+FSA by AMI_1:def 15
.= (while>0(a,I) +* sl0).IC SCM+FSA by A8,FUNCT_4:14
.= IC sm by A25,SF_MASTR:66;
A27: sm1 | D = sm | D by SCMFSA8A:11;
sm | IL =s1 | IL by A21,SCMFSA6B:17;
then sm1 | IL = sm | IL by Th27;
then A28: sm1=sm by A26,A27,Th29;
while>0(a,I) is_halting_on sm by A22,Th43;
then sm1 is halting by SCMFSA7B:def 8;
then consider j being Nat such that
A29: CurInstr((Computation sm).j) = halt SCM+FSA by A28,AMI_1:def 20;
CurInstr (Computation s1).(n+j) = halt SCM+FSA by A21,A29,AMI_1:51;
then s1 is halting by AMI_1:def 20;
hence while>0(a,I) is_halting_on s by SCMFSA7B:def 8;
set p=(LifeSpan (s+* (I +* sl0)) + 3);
now let q be Nat;
A30: 0<m by A19,NAT_1:19;
per cases;
suppose A31: q <= p;
A32: StepWhile>0(a,I,s).0=s by Def5;
F(0) <> 0 by A6,A30;
then A33: s.a > 0 by A2,A32;
I is_closed_on s & I is_halting_on s by A1,A32;
hence IC (Computation s1).q in dom while>0(a,I) by A31,A33,Th47;
suppose A34: q > p;
defpred P2[Nat] means
$1<=m & $1<>0 & (ex k st StepWhile>0(a,I,s).$1=
(Computation s1).k & k <= q);
A35: for i be Nat st P2[i] holds i <= m;
A36: now
take k=p;
thus StepWhile>0(a,I,s).1=(Computation s1).k & k <= q
by A34,Th51;
end;
0+1 < m +1 by A30,REAL_1:53;
then 1 <= m by NAT_1:38;
then A37: ex t be Nat st P2[t] by A36;
ex k st P2[k] & for i st P2[i] holds i <= k from Max(A35,A37);
then consider t being Nat such that
A38: P2[t] & for i st P2[i] holds i <= t;
now per cases;
suppose t=m;
then consider r being Nat such that
A39: sm=(Computation s1).r & r <= q by A38;
consider x being Nat such that
A40: q = r+x by A39,NAT_1:28;
A41: (Computation s1).q = (Computation sm1).x by A28,A39,A40,
AMI_1:51;
while>0(a,I) is_closed_on sm by A22,Th43;
hence IC (Computation s1).q in dom while>0(a,I) by A41,
SCMFSA7B:def 7;
suppose t<>m;
then A42: t < m by A38,REAL_1:def 5;
consider y being Nat such that
A43: t=y+1 by A38,NAT_1:22;
consider z being Nat such that
A44: StepWhile>0(a,I,s).t=(Computation s1).z & z <= q by A38;
y+ 0 < t by A43,REAL_1:53;
then A45: y < m by A38,AXIOMS:22;
set Dy=StepWhile>0(a,I,s).y;
set Dt=StepWhile>0(a,I,s).t;
A46: Dt= (Computation (Dy +* (while>0(a,I)+* sl0))).
(LifeSpan (Dy +* (I +* sl0)) + 3) by A43,Def5;
A47: I is_closed_on Dy & I is_halting_on Dy by A1;
F(y) <> 0 by A6,A45;
then Dy.a > 0 by A2;
then A48: IC Dt =insloc 0 by A46,A47,Th47;
set z2=z +(LifeSpan (Dt +* (I +* sl0)) + 3);
A49: now assume A50: z2 <= q;
A51: now take k=z2;thus
StepWhile>0(a,I,s).(t+1)=(Computation s1).k & k <=q
by A44,A48,A50,Th52;
end;
t+1 <= m by A42,NAT_1:38;
then t+1 <= t by A38,A51;
hence contradiction by REAL_1:69;
end;
consider w being Nat such that
A52: q = z+w by A44,NAT_1:28;
A53: w < LifeSpan (Dt +* (I +* sl0)) + 3 by A49,A52,AXIOMS:24;
A54: (Computation s1).q = (Computation Dt ).w by A44,A52,AMI_1:
51
.= (Computation (Dt +* (while>0(a,I)+* sl0))).w
by A44,A48,Th52;
A55: I is_closed_on Dt & I is_halting_on Dt by A1;
F(t) <> 0 by A6,A42;
then Dt.a > 0 by A2;
hence IC (Computation s1).q in dom while>0(a,I)
by A53,A54,A55,Th47;
end;
hence IC (Computation s1).q in dom while>0(a,I);
end;
hence while>0(a,I) is_closed_on s by SCMFSA7B:def 7;
end;
hence thesis;
end;
theorem Th54:
for I being parahalting Macro-Instruction, a being read-write
Int-Location, s being State of SCM+FSA st
ex f being Function of product the Object-Kind of SCM+FSA,NAT st
(for k being Nat holds (f.(StepWhile>0(a,I,s).(k+1)) <
f.(StepWhile>0(a,I,s).k) or f.(StepWhile>0(a,I,s).k) = 0) &
( f.(StepWhile>0(a,I,s).k)=0 iff (StepWhile>0(a,I,s).k).a <= 0 ) )
holds
while>0(a,I) is_halting_on s & while>0(a,I) is_closed_on s
proof
let I be parahalting Macro-Instruction,a be read-write
Int-Location,s be State of SCM+FSA;
assume A1:
ex f being Function of product the Object-Kind of SCM+FSA,NAT st
(for k being Nat holds (f.(StepWhile>0(a,I,s).(k+1)) <
f.(StepWhile>0(a,I,s).k) or f.(StepWhile>0(a,I,s).k) = 0) &
( f.(StepWhile>0(a,I,s).k)=0 iff (StepWhile>0(a,I,s).k).a <= 0 ) );
A2: for k being Nat holds I is_closed_on StepWhile>0(a,I,s).k by SCMFSA7B:24;
for k being Nat holds I is_halting_on StepWhile>0(a,I,s).k by SCMFSA7B:25
;
hence thesis by A1,A2,Th53;
end;
theorem
for I being parahalting Macro-Instruction, a being read-write
Int-Location st
ex f being Function of product the Object-Kind of SCM+FSA,NAT st
(for s being State of SCM+FSA holds (f.(StepWhile>0(a,I,s).1) < f.s
or f.s = 0) & ( f.s =0 iff s.a <= 0 ))
holds while>0(a,I) is parahalting
proof
let I be parahalting Macro-Instruction,a be read-write
Int-Location;
given f being Function of product the Object-Kind of SCM+FSA,NAT
such that A1: for s being State of SCM+FSA holds
(f.(StepWhile>0(a,I,s).1) < f.s or f.s = 0) & ( f.s =0 iff s.a <= 0 );
now let t be State of SCM+FSA;
now let k be Nat;
(f.(StepWhile>0(a,I,StepWhile>0(a,I,t).k).1) <
f.(StepWhile>0(a,I,t).k) or f.(StepWhile>0(a,I,t).k) = 0) &
( f.(StepWhile>0(a,I,t).k)=0 iff (StepWhile>0(a,I,t).k).a <= 0 )
by A1;hence
(f.(StepWhile>0(a,I,t).(k+1)) <
f.(StepWhile>0(a,I,t).k) or f.(StepWhile>0(a,I,t).k) = 0) &
( f.(StepWhile>0(a,I,t).k)=0 iff (StepWhile>0(a,I,t).k).a <= 0 )
by Th50;
end;
hence while>0(a,I) is_halting_on t by Th54;
end;
hence thesis by SCMFSA7B:25;
end;
definition
let I,J be good Macro-Instruction,a be Int-Location;
cluster if>0(a,I,J) -> good;
correctness
proof
set i = a >0_goto insloc (card J + 3);
i does_not_destroy intloc 0 by SCMFSA7B:19;
then reconsider Mi=Macro i as good Macro-Instruction by Th36;
if>0(a,I,J) = i ';' J ';' Goto insloc (card I + 1) ';' I ';'
SCM+FSA-Stop by SCMFSA8B:def 2
.= Mi ';' J ';' Goto insloc (card I + 1) ';' I ';'
SCM+FSA-Stop by SCMFSA6A:def 5;
hence thesis;
end;
end;
definition
let I be good Macro-Instruction,a be Int-Location;
cluster while>0(a,I) -> good;
correctness
proof
set J=insloc (card I +4) .--> goto insloc 0;
set F=if>0(a, I ';' Goto insloc 0, SCM+FSA-Stop);
A1: J does_not_destroy intloc 0 by Th35;
A2: F does_not_destroy intloc 0 by SCMFSA7B:def 5;
while>0(a,I) = F+*J by Def2;
then while>0(a,I) does_not_destroy intloc 0 by A1,A2,SCMFSA8A:25;
hence thesis by SCMFSA7B:def 5;
end;
end;