let q be NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function; :: according to AMISTD_5:def 4 :: thesis: for b_{1} being set

for b_{2} being set holds

( not b_{1} c= b_{2} or for b_{3} being set holds

( not q c= b_{3} or for b_{4} being set holds IC (Comput (b_{3},b_{2},b_{4})) in dom q ) )

let p be non empty q -autonomic FinPartState of (SCM R); :: thesis: for b_{1} being set holds

( not p c= b_{1} or for b_{2} being set holds

( not q c= b_{2} or for b_{3} being set holds IC (Comput (b_{2},b_{1},b_{3})) in dom q ) )

let s be State of (SCM R); :: thesis: ( not p c= s or for b_{1} being set holds

( not q c= b_{1} or for b_{2} being set holds IC (Comput (b_{1},s,b_{2})) in dom q ) )

assume A1: p c= s ; :: thesis: for b_{1} being set holds

( not q c= b_{1} or for b_{2} being set holds IC (Comput (b_{1},s,b_{2})) in dom q )

let P be Instruction-Sequence of (SCM R); :: thesis: ( not q c= P or for b_{1} being set holds IC (Comput (P,s,b_{1})) in dom q )

assume A2: q c= P ; :: thesis: for b_{1} being set holds IC (Comput (P,s,b_{1})) in dom q

let i be Nat; :: thesis: IC (Comput (P,s,i)) in dom q

set Csi = Comput (P,s,i);

set loc = IC (Comput (P,s,i));

set loc1 = (IC (Comput (P,s,i))) + 1;

assume A3: not IC (Comput (P,s,i)) in dom q ; :: thesis: contradiction

set I = (dl. (R,0)) := (dl. (R,0));

set q1 = q +* ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0))));

set q2 = q +* ((IC (Comput (P,s,i))) .--> (halt (SCM R)));

reconsider P1 = P +* ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) as Instruction-Sequence of (SCM R) ;

reconsider P2 = P +* ((IC (Comput (P,s,i))) .--> (halt (SCM R))) as Instruction-Sequence of (SCM R) ;

A5: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> (halt (SCM R))) by TARSKI:def 1;

A7: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) by TARSKI:def 1;

A8: dom q misses dom ((IC (Comput (P,s,i))) .--> (halt (SCM R))) by A3, ZFMISC_1:50;

A9: dom q misses dom ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) by A3, ZFMISC_1:50;

A10: q +* ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) c= P1 by A2, FUNCT_4:123;

A11: q +* ((IC (Comput (P,s,i))) .--> (halt (SCM R))) c= P2 by A2, FUNCT_4:123;

set Cs2i = Comput (P2,s,i);

set Cs1i = Comput (P1,s,i);

not p is q -autonomic

for b

( not b

( not q c= b

let p be non empty q -autonomic FinPartState of (SCM R); :: thesis: for b

( not p c= b

( not q c= b

let s be State of (SCM R); :: thesis: ( not p c= s or for b

( not q c= b

assume A1: p c= s ; :: thesis: for b

( not q c= b

let P be Instruction-Sequence of (SCM R); :: thesis: ( not q c= P or for b

assume A2: q c= P ; :: thesis: for b

let i be Nat; :: thesis: IC (Comput (P,s,i)) in dom q

set Csi = Comput (P,s,i);

set loc = IC (Comput (P,s,i));

set loc1 = (IC (Comput (P,s,i))) + 1;

assume A3: not IC (Comput (P,s,i)) in dom q ; :: thesis: contradiction

set I = (dl. (R,0)) := (dl. (R,0));

set q1 = q +* ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0))));

set q2 = q +* ((IC (Comput (P,s,i))) .--> (halt (SCM R)));

reconsider P1 = P +* ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) as Instruction-Sequence of (SCM R) ;

reconsider P2 = P +* ((IC (Comput (P,s,i))) .--> (halt (SCM R))) as Instruction-Sequence of (SCM R) ;

A5: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> (halt (SCM R))) by TARSKI:def 1;

A7: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) by TARSKI:def 1;

A8: dom q misses dom ((IC (Comput (P,s,i))) .--> (halt (SCM R))) by A3, ZFMISC_1:50;

A9: dom q misses dom ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) by A3, ZFMISC_1:50;

A10: q +* ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) c= P1 by A2, FUNCT_4:123;

A11: q +* ((IC (Comput (P,s,i))) .--> (halt (SCM R))) c= P2 by A2, FUNCT_4:123;

set Cs2i = Comput (P2,s,i);

set Cs1i = Comput (P1,s,i);

not p is q -autonomic

proof

hence
contradiction
; :: thesis: verum
((IC (Comput (P,s,i))) .--> (halt (SCM R))) . (IC (Comput (P,s,i))) = halt (SCM R)
by FUNCOP_1:72;

then A12: P2 . (IC (Comput (P,s,i))) = halt (SCM R) by A5, FUNCT_4:13;

A13: ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) . (IC (Comput (P,s,i))) = (dl. (R,0)) := (dl. (R,0)) by FUNCOP_1:72;

take P1 ; :: according to EXTPRO_1:def 10 :: thesis: ex b_{1} being set st

( q c= P1 & q c= b_{1} & ex b_{2}, b_{3} being set st

( p c= b_{2} & p c= b_{3} & not for b_{4} being set holds (Comput (P1,b_{2},b_{4})) | (dom p) = (Comput (b_{1},b_{3},b_{4})) | (dom p) ) )

take P2 ; :: thesis: ( q c= P1 & q c= P2 & ex b_{1}, b_{2} being set st

( p c= b_{1} & p c= b_{2} & not for b_{3} being set holds (Comput (P1,b_{1},b_{3})) | (dom p) = (Comput (P2,b_{2},b_{3})) | (dom p) ) )

q c= q +* ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) by A9, FUNCT_4:32;

hence A14: q c= P1 by A10, XBOOLE_1:1; :: thesis: ( q c= P2 & ex b_{1}, b_{2} being set st

( p c= b_{1} & p c= b_{2} & not for b_{3} being set holds (Comput (P1,b_{1},b_{3})) | (dom p) = (Comput (P2,b_{2},b_{3})) | (dom p) ) )

q c= q +* ((IC (Comput (P,s,i))) .--> (halt (SCM R))) by A8, FUNCT_4:32;

hence A15: q c= P2 by A11, XBOOLE_1:1; :: thesis: ex b_{1}, b_{2} being set st

( p c= b_{1} & p c= b_{2} & not for b_{3} being set holds (Comput (P1,b_{1},b_{3})) | (dom p) = (Comput (P2,b_{2},b_{3})) | (dom p) )

take s ; :: thesis: ex b_{1} being set st

( p c= s & p c= b_{1} & not for b_{2} being set holds (Comput (P1,s,b_{2})) | (dom p) = (Comput (P2,b_{1},b_{2})) | (dom p) )

take s ; :: thesis: ( p c= s & p c= s & not for b_{1} being set holds (Comput (P1,s,b_{1})) | (dom p) = (Comput (P2,s,b_{1})) | (dom p) )

thus p c= s by A1; :: thesis: ( p c= s & not for b_{1} being set holds (Comput (P1,s,b_{1})) | (dom p) = (Comput (P2,s,b_{1})) | (dom p) )

A16: (Comput (P1,s,i)) | (dom p) = (Comput (P,s,i)) | (dom p) by A14, A2, A1, EXTPRO_1:def 10;

thus p c= s by A1; :: thesis: not for b_{1} being set holds (Comput (P1,s,b_{1})) | (dom p) = (Comput (P2,s,b_{1})) | (dom p)

A17: (Comput (P1,s,i)) | (dom p) = (Comput (P2,s,i)) | (dom p) by A14, A15, A1, EXTPRO_1:def 10;

take k = i + 1; :: thesis: not (Comput (P1,s,k)) | (dom p) = (Comput (P2,s,k)) | (dom p)

set Cs1k = Comput (P1,s,k);

A18: IC in dom p by AMISTD_5:6;

IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p)) by A18, FUNCT_1:49;

then IC (Comput (P1,s,i)) = IC (Comput (P,s,i)) by A16, A18, FUNCT_1:49;

then A19: CurInstr (P1,(Comput (P1,s,i))) = P1 . (IC (Comput (P,s,i))) by PBOOLE:143

.= (dl. (R,0)) := (dl. (R,0)) by A13, A7, FUNCT_4:13 ;

A20: Comput (P1,s,k) = Following (P1,(Comput (P1,s,i))) by EXTPRO_1:3

.= Exec (((dl. (R,0)) := (dl. (R,0))),(Comput (P1,s,i))) by A19 ;

A21: IC (Exec (((dl. (R,0)) := (dl. (R,0))),(Comput (P1,s,i)))) = (IC (Comput (P1,s,i))) + 1 by SCMRING2:11;

A22: IC in dom p by AMISTD_5:6;

A23: IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p)) by A22, FUNCT_1:49;

then A24: IC (Comput (P1,s,k)) = (IC (Comput (P,s,i))) + 1 by A20, A21, A16, A22, FUNCT_1:49;

set Cs2k = Comput (P2,s,k);

A25: Comput (P2,s,k) = Following (P2,(Comput (P2,s,i))) by EXTPRO_1:3

.= Exec ((CurInstr (P2,(Comput (P2,s,i)))),(Comput (P2,s,i))) ;

A26: P2 /. (IC (Comput (P2,s,i))) = P2 . (IC (Comput (P2,s,i))) by PBOOLE:143;

IC (Comput (P2,s,i)) = IC (Comput (P,s,i)) by A16, A23, A17, A22, FUNCT_1:49;

then A27: IC (Comput (P2,s,k)) = IC (Comput (P,s,i)) by A25, A12, A26, EXTPRO_1:def 3;

( IC ((Comput (P1,s,k)) | (dom p)) = IC (Comput (P1,s,k)) & IC ((Comput (P2,s,k)) | (dom p)) = IC (Comput (P2,s,k)) ) by A22, FUNCT_1:49;

hence not (Comput (P1,s,k)) | (dom p) = (Comput (P2,s,k)) | (dom p) by A24, A27; :: thesis: verum

end;then A12: P2 . (IC (Comput (P,s,i))) = halt (SCM R) by A5, FUNCT_4:13;

A13: ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) . (IC (Comput (P,s,i))) = (dl. (R,0)) := (dl. (R,0)) by FUNCOP_1:72;

take P1 ; :: according to EXTPRO_1:def 10 :: thesis: ex b

( q c= P1 & q c= b

( p c= b

take P2 ; :: thesis: ( q c= P1 & q c= P2 & ex b

( p c= b

q c= q +* ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) by A9, FUNCT_4:32;

hence A14: q c= P1 by A10, XBOOLE_1:1; :: thesis: ( q c= P2 & ex b

( p c= b

q c= q +* ((IC (Comput (P,s,i))) .--> (halt (SCM R))) by A8, FUNCT_4:32;

hence A15: q c= P2 by A11, XBOOLE_1:1; :: thesis: ex b

( p c= b

take s ; :: thesis: ex b

( p c= s & p c= b

take s ; :: thesis: ( p c= s & p c= s & not for b

thus p c= s by A1; :: thesis: ( p c= s & not for b

A16: (Comput (P1,s,i)) | (dom p) = (Comput (P,s,i)) | (dom p) by A14, A2, A1, EXTPRO_1:def 10;

thus p c= s by A1; :: thesis: not for b

A17: (Comput (P1,s,i)) | (dom p) = (Comput (P2,s,i)) | (dom p) by A14, A15, A1, EXTPRO_1:def 10;

take k = i + 1; :: thesis: not (Comput (P1,s,k)) | (dom p) = (Comput (P2,s,k)) | (dom p)

set Cs1k = Comput (P1,s,k);

A18: IC in dom p by AMISTD_5:6;

IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p)) by A18, FUNCT_1:49;

then IC (Comput (P1,s,i)) = IC (Comput (P,s,i)) by A16, A18, FUNCT_1:49;

then A19: CurInstr (P1,(Comput (P1,s,i))) = P1 . (IC (Comput (P,s,i))) by PBOOLE:143

.= (dl. (R,0)) := (dl. (R,0)) by A13, A7, FUNCT_4:13 ;

A20: Comput (P1,s,k) = Following (P1,(Comput (P1,s,i))) by EXTPRO_1:3

.= Exec (((dl. (R,0)) := (dl. (R,0))),(Comput (P1,s,i))) by A19 ;

A21: IC (Exec (((dl. (R,0)) := (dl. (R,0))),(Comput (P1,s,i)))) = (IC (Comput (P1,s,i))) + 1 by SCMRING2:11;

A22: IC in dom p by AMISTD_5:6;

A23: IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p)) by A22, FUNCT_1:49;

then A24: IC (Comput (P1,s,k)) = (IC (Comput (P,s,i))) + 1 by A20, A21, A16, A22, FUNCT_1:49;

set Cs2k = Comput (P2,s,k);

A25: Comput (P2,s,k) = Following (P2,(Comput (P2,s,i))) by EXTPRO_1:3

.= Exec ((CurInstr (P2,(Comput (P2,s,i)))),(Comput (P2,s,i))) ;

A26: P2 /. (IC (Comput (P2,s,i))) = P2 . (IC (Comput (P2,s,i))) by PBOOLE:143;

IC (Comput (P2,s,i)) = IC (Comput (P,s,i)) by A16, A23, A17, A22, FUNCT_1:49;

then A27: IC (Comput (P2,s,k)) = IC (Comput (P,s,i)) by A25, A12, A26, EXTPRO_1:def 3;

( IC ((Comput (P1,s,k)) | (dom p)) = IC (Comput (P1,s,k)) & IC ((Comput (P2,s,k)) | (dom p)) = IC (Comput (P2,s,k)) ) by A22, FUNCT_1:49;

hence not (Comput (P1,s,k)) | (dom p) = (Comput (P2,s,k)) | (dom p) by A24, A27; :: thesis: verum