:: EXTPRO_1 semantic presentation begin definition let N be set ; attrc2 is strict ; struct AMI-Struct over N -> Mem-Struct over N, COM-Struct ; aggrAMI-Struct(# carrier, ZeroF, InstructionsF, Object-Kind, ValuesF, Execution #) -> AMI-Struct over N; sel Execution c2 -> Action of the InstructionsF of c2,(product ( the ValuesF of c2 * the Object-Kind of c2)); end; definition let N be with_zero set ; func Trivial-AMI N -> strict AMI-Struct over N means :Def1: :: EXTPRO_1:def 1 ( the carrier of it = {0} & the ZeroF of it = 0 & the InstructionsF of it = {[0,{},{}]} & the Object-Kind of it = 0 .--> 0 & the ValuesF of it = N --> NAT & the Execution of it = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) ); existence ex b1 being strict AMI-Struct over N st ( the carrier of b1 = {0} & the ZeroF of b1 = 0 & the InstructionsF of b1 = {[0,{},{}]} & the Object-Kind of b1 = 0 .--> 0 & the ValuesF of b1 = N --> NAT & the Execution of b1 = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) ) proof set I = {[0,{},{}]}; reconsider i = [0,{},{}] as Element of {[0,{},{}]} by TARSKI:def_1; set f = 0 .--> 0; A1: dom (0 .--> 0) = dom (0 .--> 0) .= {0} by FUNCOP_1:13 ; A2: rng (0 .--> 0) c= {0} by FUNCOP_1:13; 0 in N by MEASURE6:def_2; then {0} c= N by ZFMISC_1:31; then rng (0 .--> 0) c= N by A2, XBOOLE_1:1; then reconsider f = 0 .--> 0 as Function of {0},N by A1, RELSET_1:4; reconsider y = 0 as Element of {0} by TARSKI:def_1; reconsider E = {[0,{},{}]} --> (id (product ((N --> NAT) * f))) as Action of {[0,{},{}]},(product ((N --> NAT) * f)) by FUNCOP_1:45, FUNCT_2:9; take S = AMI-Struct(# {0},y,{[0,{},{}]},f,(N --> NAT),E #); ::_thesis: ( the carrier of S = {0} & the ZeroF of S = 0 & the InstructionsF of S = {[0,{},{}]} & the Object-Kind of S = 0 .--> 0 & the ValuesF of S = N --> NAT & the Execution of S = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) ) thus ( the carrier of S = {0} & the ZeroF of S = 0 & the InstructionsF of S = {[0,{},{}]} & the Object-Kind of S = 0 .--> 0 & the ValuesF of S = N --> NAT & the Execution of S = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict AMI-Struct over N st the carrier of b1 = {0} & the ZeroF of b1 = 0 & the InstructionsF of b1 = {[0,{},{}]} & the Object-Kind of b1 = 0 .--> 0 & the ValuesF of b1 = N --> NAT & the Execution of b1 = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) & the carrier of b2 = {0} & the ZeroF of b2 = 0 & the InstructionsF of b2 = {[0,{},{}]} & the Object-Kind of b2 = 0 .--> 0 & the ValuesF of b2 = N --> NAT & the Execution of b2 = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) holds b1 = b2 ; end; :: deftheorem Def1 defines Trivial-AMI EXTPRO_1:def_1_:_ for N being with_zero set for b2 being strict AMI-Struct over N holds ( b2 = Trivial-AMI N iff ( the carrier of b2 = {0} & the ZeroF of b2 = 0 & the InstructionsF of b2 = {[0,{},{}]} & the Object-Kind of b2 = 0 .--> 0 & the ValuesF of b2 = N --> NAT & the Execution of b2 = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) ) ); registration let N be with_zero set ; cluster Trivial-AMI N -> 1 -element strict ; coherence Trivial-AMI N is 1 -element proof set S = Trivial-AMI N; thus the carrier of (Trivial-AMI N) is 1 -element by Def1; :: according to STRUCT_0:def_19 ::_thesis: verum end; end; registration let N be with_zero set ; cluster non empty for AMI-Struct over N; existence not for b1 being AMI-Struct over N holds b1 is empty proof take Trivial-AMI N ; ::_thesis: not Trivial-AMI N is empty thus not Trivial-AMI N is empty ; ::_thesis: verum end; end; registration let N be with_zero set ; cluster Trivial-AMI N -> with_non-empty_values strict ; coherence Trivial-AMI N is with_non-empty_values proof let n be set ; :: according to FUNCT_1:def_9,MEMSTR_0:def_3 ::_thesis: ( not n in proj1 (the_Values_of (Trivial-AMI N)) or not (the_Values_of (Trivial-AMI N)) . n is empty ) set S = Trivial-AMI N; set F = the_Values_of (Trivial-AMI N); assume A1: n in dom (the_Values_of (Trivial-AMI N)) ; ::_thesis: not (the_Values_of (Trivial-AMI N)) . n is empty then A2: the Object-Kind of (Trivial-AMI N) . n in dom the ValuesF of (Trivial-AMI N) by FUNCT_1:11; A3: the ValuesF of (Trivial-AMI N) = N --> NAT by Def1; then A4: the Object-Kind of (Trivial-AMI N) . n in N by A2, FUNCOP_1:13; (the_Values_of (Trivial-AMI N)) . n = the ValuesF of (Trivial-AMI N) . ( the Object-Kind of (Trivial-AMI N) . n) by A1, FUNCT_1:12 .= NAT by A4, A3, FUNCOP_1:7 ; hence not (the_Values_of (Trivial-AMI N)) . n is empty ; ::_thesis: verum end; end; registration let N be with_zero set ; cluster1 -element with_non-empty_values for AMI-Struct over N; existence ex b1 being AMI-Struct over N st ( b1 is with_non-empty_values & b1 is 1 -element ) proof take Trivial-AMI N ; ::_thesis: ( Trivial-AMI N is with_non-empty_values & Trivial-AMI N is 1 -element ) thus ( Trivial-AMI N is with_non-empty_values & Trivial-AMI N is 1 -element ) ; ::_thesis: verum end; end; definition let N be with_zero set ; let S be with_non-empty_values AMI-Struct over N; let I be Instruction of S; let s be State of S; func Exec (I,s) -> State of S equals :: EXTPRO_1:def 2 ( the Execution of S . I) . s; coherence ( the Execution of S . I) . s is State of S proof consider f being Function such that A1: ( the Execution of S . I = f & dom f = product (the_Values_of S) ) and A2: rng f c= product (the_Values_of S) by FUNCT_2:def_2; reconsider s = s as Element of product (the_Values_of S) by CARD_3:107; ( the Execution of S . I) . s in rng f by A1, FUNCT_1:def_3; hence ( the Execution of S . I) . s is State of S by A2; ::_thesis: verum end; end; :: deftheorem defines Exec EXTPRO_1:def_2_:_ for N being with_zero set for S being with_non-empty_values AMI-Struct over N for I being Instruction of S for s being State of S holds Exec (I,s) = ( the Execution of S . I) . s; definition let N be with_zero set ; let S be with_non-empty_values AMI-Struct over N; let I be Instruction of S; attrI is halting means :Def3: :: EXTPRO_1:def 3 for s being State of S holds Exec (I,s) = s; end; :: deftheorem Def3 defines halting EXTPRO_1:def_3_:_ for N being with_zero set for S being with_non-empty_values AMI-Struct over N for I being Instruction of S holds ( I is halting iff for s being State of S holds Exec (I,s) = s ); definition let N be with_zero set ; let S be with_non-empty_values AMI-Struct over N; attrS is halting means :Def4: :: EXTPRO_1:def 4 halt S is halting ; end; :: deftheorem Def4 defines halting EXTPRO_1:def_4_:_ for N being with_zero set for S being with_non-empty_values AMI-Struct over N holds ( S is halting iff halt S is halting ); registration let N be with_zero set ; cluster Trivial-AMI N -> strict halting ; coherence Trivial-AMI N is halting proof set T = Trivial-AMI N; set f = (N --> NAT) * (0 .--> 0); A1: ( the Object-Kind of (Trivial-AMI N) = 0 .--> 0 & the ValuesF of (Trivial-AMI N) = N --> NAT ) by Def1; set I = halt (Trivial-AMI N); let s be State of (Trivial-AMI N); :: according to EXTPRO_1:def_3,EXTPRO_1:def_4 ::_thesis: Exec ((halt (Trivial-AMI N)),s) = s reconsider ss = s as Element of product (the_Values_of (Trivial-AMI N)) by CARD_3:107; ((halt (Trivial-AMI N)) .--> (id (product ((N --> NAT) * (0 .--> 0))))) . (halt (Trivial-AMI N)) = id (product ((N --> NAT) * (0 .--> 0))) by FUNCOP_1:72; hence Exec ((halt (Trivial-AMI N)),s) = (id (product ((N --> NAT) * (0 .--> 0)))) . ss by Def1 .= s by A1, FUNCT_1:18 ; ::_thesis: verum end; end; registration let N be with_zero set ; cluster non empty with_non-empty_values halting for AMI-Struct over N; existence ex b1 being non empty with_non-empty_values AMI-Struct over N st b1 is halting proof take Trivial-AMI N ; ::_thesis: Trivial-AMI N is halting thus Trivial-AMI N is halting ; ::_thesis: verum end; end; registration let N be with_zero set ; let S be with_non-empty_values halting AMI-Struct over N; cluster halt S -> halting ; coherence halt S is halting by Def4; end; registration let N be with_zero set ; let S be with_non-empty_values halting AMI-Struct over N; cluster halting for Element of the InstructionsF of S; existence ex b1 being Instruction of S st b1 is halting proof take halt S ; ::_thesis: halt S is halting thus halt S is halting ; ::_thesis: verum end; end; theorem :: EXTPRO_1:1 for N being with_zero set for s being State of (Trivial-AMI N) for i being Instruction of (Trivial-AMI N) holds Exec (i,s) = s proof let N be with_zero set ; ::_thesis: for s being State of (Trivial-AMI N) for i being Instruction of (Trivial-AMI N) holds Exec (i,s) = s set T = Trivial-AMI N; let s be State of (Trivial-AMI N); ::_thesis: for i being Instruction of (Trivial-AMI N) holds Exec (i,s) = s let i be Instruction of (Trivial-AMI N); ::_thesis: Exec (i,s) = s set f = (N --> NAT) * (0 .--> 0); A1: ( the Object-Kind of (Trivial-AMI N) = 0 .--> 0 & the ValuesF of (Trivial-AMI N) = N --> NAT ) by Def1; reconsider ss = s as Element of product (the_Values_of (Trivial-AMI N)) by CARD_3:107; the InstructionsF of (Trivial-AMI N) = {[0,{},{}]} by Def1; then ( (i .--> (id (product ((N --> NAT) * (0 .--> 0))))) . i = id (product ((N --> NAT) * (0 .--> 0))) & i = [0,{},{}] ) by FUNCOP_1:72, TARSKI:def_1; hence Exec (i,s) = (id (product ((N --> NAT) * (0 .--> 0)))) . ss by Def1 .= s by A1, FUNCT_1:18 ; ::_thesis: verum end; registration let E be with_zero set ; cluster Trivial-AMI E -> IC-Ins-separated strict ; coherence Trivial-AMI E is IC-Ins-separated proof set S = Trivial-AMI E; A1: ( the Object-Kind of (Trivial-AMI E) = 0 .--> 0 & the ValuesF of (Trivial-AMI E) = E --> NAT ) by Def1; A2: 0 in E by MEASURE6:def_2; A3: 0 in dom (0 .--> 0) by FUNCOP_1:73; thus Values (IC ) = (the_Values_of (Trivial-AMI E)) . 0 by Def1 .= ((E --> NAT) * (0 .--> 0)) . 0 by A1 .= (E --> NAT) . ((0 .--> 0) . 0) by A3, FUNCT_1:13 .= (E --> NAT) . 0 by FUNCOP_1:72 .= NAT by A2, FUNCOP_1:7 ; :: according to MEMSTR_0:def_6 ::_thesis: verum end; end; registration let M be with_zero set ; cluster non empty trivial with_non-empty_values IC-Ins-separated strict for AMI-Struct over M; existence ex b1 being non empty with_non-empty_values AMI-Struct over M st ( b1 is IC-Ins-separated & b1 is strict & b1 is trivial ) proof take Trivial-AMI M ; ::_thesis: ( Trivial-AMI M is IC-Ins-separated & Trivial-AMI M is strict & Trivial-AMI M is trivial ) thus ( Trivial-AMI M is IC-Ins-separated & Trivial-AMI M is strict & Trivial-AMI M is trivial ) ; ::_thesis: verum end; end; registration let N be with_zero set ; cluster non empty trivial finite 1 -element with_non-empty_values IC-Ins-separated strict halting for AMI-Struct over N; existence ex b1 being 1 -element with_non-empty_values AMI-Struct over N st ( b1 is IC-Ins-separated & b1 is halting & b1 is strict ) proof take Trivial-AMI N ; ::_thesis: ( Trivial-AMI N is IC-Ins-separated & Trivial-AMI N is halting & Trivial-AMI N is strict ) thus ( Trivial-AMI N is IC-Ins-separated & Trivial-AMI N is halting & Trivial-AMI N is strict ) ; ::_thesis: verum end; end; begin definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; let p be the InstructionsF of S -valued Function; let s be State of S; func CurInstr (p,s) -> Instruction of S equals :: EXTPRO_1:def 5 p /. (IC s); coherence p /. (IC s) is Instruction of S ; end; :: deftheorem defines CurInstr EXTPRO_1:def_5_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for p being the InstructionsF of b2 -valued Function for s being State of S holds CurInstr (p,s) = p /. (IC s); definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; let s be State of S; let p be the InstructionsF of S -valued Function; func Following (p,s) -> State of S equals :: EXTPRO_1:def 6 Exec ((CurInstr (p,s)),s); correctness coherence Exec ((CurInstr (p,s)),s) is State of S; ; end; :: deftheorem defines Following EXTPRO_1:def_6_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for s being State of S for p being the InstructionsF of b2 -valued Function holds Following (p,s) = Exec ((CurInstr (p,s)),s); definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; let p be NAT -defined the InstructionsF of S -valued Function; deffunc H1( set , State of S) -> Element of product (the_Values_of S) = down (Following (p,\$2)); let s be State of S; let k be Nat; func Comput (p,s,k) -> State of S means :Def7: :: EXTPRO_1:def 7 ex f being Function of NAT,(product (the_Values_of S)) st ( it = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ); existence ex b1 being State of S ex f being Function of NAT,(product (the_Values_of S)) st ( b1 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) proof reconsider ss = s as Element of product (the_Values_of S) by CARD_3:107; consider f being Function of NAT,(product (the_Values_of S)) such that A1: f . 0 = ss and A2: for n being Nat holds f . (n + 1) = H1(n,f . n) from NAT_1:sch_12(); take f . k ; ::_thesis: ex f being Function of NAT,(product (the_Values_of S)) st ( f . k = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) take f ; ::_thesis: ( f . k = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) thus f . k = f . k ; ::_thesis: ( f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) thus f . 0 = s by A1; ::_thesis: for i being Nat holds f . (i + 1) = Following (p,(f . i)) let i be Nat; ::_thesis: f . (i + 1) = Following (p,(f . i)) thus f . (i + 1) = H1(i,f . i) by A2 .= Following (p,(f . i)) ; ::_thesis: verum end; uniqueness for b1, b2 being State of S st ex f being Function of NAT,(product (the_Values_of S)) st ( b1 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) & ex f being Function of NAT,(product (the_Values_of S)) st ( b2 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) holds b1 = b2 proof let s1, s2 be State of S; ::_thesis: ( ex f being Function of NAT,(product (the_Values_of S)) st ( s1 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) & ex f being Function of NAT,(product (the_Values_of S)) st ( s2 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) implies s1 = s2 ) given f1 being Function of NAT,(product (the_Values_of S)) such that A3: s1 = f1 . k and A4: f1 . 0 = s and A5: for i being Nat holds f1 . (i + 1) = Following (p,(f1 . i)) ; ::_thesis: ( for f being Function of NAT,(product (the_Values_of S)) holds ( not s2 = f . k or not f . 0 = s or ex i being Nat st not f . (i + 1) = Following (p,(f . i)) ) or s1 = s2 ) given f2 being Function of NAT,(product (the_Values_of S)) such that A6: s2 = f2 . k and A7: f2 . 0 = s and A8: for i being Nat holds f2 . (i + 1) = Following (p,(f2 . i)) ; ::_thesis: s1 = s2 reconsider s = s as Element of product (the_Values_of S) by CARD_3:107; A9: f1 . 0 = s by A4; A10: for i being Nat holds f1 . (i + 1) = H1(i,f1 . i) by A5; A11: f2 . 0 = s by A7; A12: for i being Nat holds f2 . (i + 1) = H1(i,f2 . i) by A8; f1 = f2 from NAT_1:sch_16(A9, A10, A11, A12); hence s1 = s2 by A3, A6; ::_thesis: verum end; end; :: deftheorem Def7 defines Comput EXTPRO_1:def_7_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S for k being Nat for b6 being State of S holds ( b6 = Comput (p,s,k) iff ex f being Function of NAT,(product (the_Values_of S)) st ( b6 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) ); definition let N be with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; let p be NAT -defined the InstructionsF of S -valued Function; let s be State of S; predp halts_on s means :Def8: :: EXTPRO_1:def 8 ex k being Nat st ( IC (Comput (p,s,k)) in dom p & CurInstr (p,(Comput (p,s,k))) = halt S ); end; :: deftheorem Def8 defines halts_on EXTPRO_1:def_8_:_ for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S holds ( p halts_on s iff ex k being Nat st ( IC (Comput (p,s,k)) in dom p & CurInstr (p,(Comput (p,s,k))) = halt S ) ); registration let N be non empty with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; let p be NAT -defined the InstructionsF of S -valued Function; let s be State of S; reduce Comput (p,s,0) to s; reducibility Comput (p,s,0) = s proof ex f being Function of NAT,(product (the_Values_of S)) st ( Comput (p,s,0) = f . 0 & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) by Def7; hence Comput (p,s,0) = s ; ::_thesis: verum end; end; theorem :: EXTPRO_1:2 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S holds Comput (p,s,0) = s ; theorem Th3: :: EXTPRO_1:3 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k))) proof let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for p being NAT -defined the InstructionsF of b1 -valued Function for s being State of S for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k))) let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued Function for s being State of S for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k))) let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k))) let s be State of S; ::_thesis: for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k))) let k be Nat; ::_thesis: Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k))) deffunc H1( set , State of S) -> Element of product (the_Values_of S) = down (Following (p,\$2)); reconsider s = s as Element of product (the_Values_of S) by CARD_3:107; consider f being Function of NAT,(product (the_Values_of S)) such that A1: Comput (p,s,(k + 1)) = f . (k + 1) and A2: f . 0 = s and A3: for i being Nat holds f . (i + 1) = Following (p,(f . i)) by Def7; consider g being Function of NAT,(product (the_Values_of S)) such that A4: Comput (p,s,k) = g . k and A5: g . 0 = s and A6: for i being Nat holds g . (i + 1) = Following (p,(g . i)) by Def7; A7: for i being Nat holds f . (i + 1) = H1(i,f . i) by A3; A8: for i being Nat holds g . (i + 1) = H1(i,g . i) by A6; f = g from NAT_1:sch_16(A2, A7, A5, A8); hence Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k))) by A1, A4, A6; ::_thesis: verum end; theorem Th4: :: EXTPRO_1:4 for i being Element of NAT for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for s being State of S for p being NAT -defined the InstructionsF of b3 -valued Function for k being Element of NAT holds Comput (p,s,(i + k)) = Comput (p,(Comput (p,s,i)),k) proof let i be Element of NAT ; ::_thesis: for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for s being State of S for p being NAT -defined the InstructionsF of b2 -valued Function for k being Element of NAT holds Comput (p,s,(i + k)) = Comput (p,(Comput (p,s,i)),k) let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for s being State of S for p being NAT -defined the InstructionsF of b1 -valued Function for k being Element of NAT holds Comput (p,s,(i + k)) = Comput (p,(Comput (p,s,i)),k) let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for s being State of S for p being NAT -defined the InstructionsF of S -valued Function for k being Element of NAT holds Comput (p,s,(i + k)) = Comput (p,(Comput (p,s,i)),k) let s be State of S; ::_thesis: for p being NAT -defined the InstructionsF of S -valued Function for k being Element of NAT holds Comput (p,s,(i + k)) = Comput (p,(Comput (p,s,i)),k) let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for k being Element of NAT holds Comput (p,s,(i + k)) = Comput (p,(Comput (p,s,i)),k) defpred S1[ Element of NAT ] means Comput (p,s,(i + \$1)) = Comput (p,(Comput (p,s,i)),\$1); A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] Comput (p,s,(i + (k + 1))) = Comput (p,s,((i + k) + 1)) .= Following (p,(Comput (p,s,(i + k)))) by Th3 .= Comput (p,(Comput (p,s,i)),(k + 1)) by A2, Th3 ; hence S1[k + 1] ; ::_thesis: verum end; A3: S1[ 0 ] ; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1); ::_thesis: verum end; theorem Th5: :: EXTPRO_1:5 for i, j being Element of NAT st i <= j holds for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b4 -valued Function for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds Comput (p,s,j) = Comput (p,s,i) proof let i, j be Element of NAT ; ::_thesis: ( i <= j implies for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds Comput (p,s,j) = Comput (p,s,i) ) assume i <= j ; ::_thesis: for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds Comput (p,s,j) = Comput (p,s,i) then consider k being Nat such that A1: j = i + k by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; A2: j = i + k by A1; let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b1 -valued Function for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds Comput (p,s,j) = Comput (p,s,i) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued Function for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds Comput (p,s,j) = Comput (p,s,i) let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds Comput (p,s,j) = Comput (p,s,i) let s be State of S; ::_thesis: ( CurInstr (p,(Comput (p,s,i))) = halt S implies Comput (p,s,j) = Comput (p,s,i) ) assume A3: CurInstr (p,(Comput (p,s,i))) = halt S ; ::_thesis: Comput (p,s,j) = Comput (p,s,i) defpred S1[ Element of NAT ] means Comput (p,s,(i + \$1)) = Comput (p,s,i); A4: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: S1[k] ; ::_thesis: S1[k + 1] Comput (p,s,(i + (k + 1))) = Comput (p,s,((i + k) + 1)) .= Following (p,(Comput (p,s,(i + k)))) by Th3 .= Comput (p,s,i) by A3, A5, Def3 ; hence S1[k + 1] ; ::_thesis: verum end; A6: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A6, A4); hence Comput (p,s,j) = Comput (p,s,i) by A2; ::_thesis: verum end; definition let N be non empty with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; let p be NAT -defined the InstructionsF of S -valued Function; let s be State of S; assume A1: p halts_on s ; func Result (p,s) -> State of S means :Def9: :: EXTPRO_1:def 9 ex k being Element of NAT st ( it = Comput (p,s,k) & CurInstr (p,it) = halt S ); uniqueness for b1, b2 being State of S st ex k being Element of NAT st ( b1 = Comput (p,s,k) & CurInstr (p,b1) = halt S ) & ex k being Element of NAT st ( b2 = Comput (p,s,k) & CurInstr (p,b2) = halt S ) holds b1 = b2 proof let s1, s2 be State of S; ::_thesis: ( ex k being Element of NAT st ( s1 = Comput (p,s,k) & CurInstr (p,s1) = halt S ) & ex k being Element of NAT st ( s2 = Comput (p,s,k) & CurInstr (p,s2) = halt S ) implies s1 = s2 ) given k1 being Element of NAT such that A1: ( s1 = Comput (p,s,k1) & CurInstr (p,s1) = halt S ) ; ::_thesis: ( for k being Element of NAT holds ( not s2 = Comput (p,s,k) or not CurInstr (p,s2) = halt S ) or s1 = s2 ) given k2 being Element of NAT such that A2: ( s2 = Comput (p,s,k2) & CurInstr (p,s2) = halt S ) ; ::_thesis: s1 = s2 ( k1 <= k2 or k2 <= k1 ) ; hence s1 = s2 by A1, A2, Th5; ::_thesis: verum end; correctness existence ex b1 being State of S ex k being Element of NAT st ( b1 = Comput (p,s,k) & CurInstr (p,b1) = halt S ); proof consider k being Nat such that IC (Comput (p,s,k)) in dom p and A3: CurInstr (p,(Comput (p,s,k))) = halt S by A1, Def8; k in NAT by ORDINAL1:def_12; hence ex b1 being State of S ex k being Element of NAT st ( b1 = Comput (p,s,k) & CurInstr (p,b1) = halt S ) by A3; ::_thesis: verum end; end; :: deftheorem Def9 defines Result EXTPRO_1:def_9_:_ for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S st p halts_on s holds for b5 being State of S holds ( b5 = Result (p,s) iff ex k being Element of NAT st ( b5 = Comput (p,s,k) & CurInstr (p,b5) = halt S ) ); theorem :: EXTPRO_1:6 for k being Element of NAT for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for P being Instruction-Sequence of S for s being State of S holds Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k))) proof let k be Element of NAT ; ::_thesis: for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for P being Instruction-Sequence of S for s being State of S holds Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k))) let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for P being Instruction-Sequence of S for s being State of S holds Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k))) let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S for s being State of S holds Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k))) let P be Instruction-Sequence of S; ::_thesis: for s being State of S holds Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k))) let s be State of S; ::_thesis: Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k))) A1: dom P = NAT by PARTFUN1:def_2; thus Comput (P,s,(k + 1)) = Following (P,(Comput (P,s,k))) by Th3 .= Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k))) by A1, PARTFUN1:def_6 ; ::_thesis: verum end; theorem Th7: :: EXTPRO_1:7 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S for k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds Result (P,s) = Comput (P,s,k) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S for k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds Result (P,s) = Comput (P,s,k) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S for s being State of S for k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds Result (P,s) = Comput (P,s,k) let P be Instruction-Sequence of S; ::_thesis: for s being State of S for k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds Result (P,s) = Comput (P,s,k) let s be State of S; ::_thesis: for k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds Result (P,s) = Comput (P,s,k) let k be Element of NAT ; ::_thesis: ( P . (IC (Comput (P,s,k))) = halt S implies Result (P,s) = Comput (P,s,k) ) A1: dom P = NAT by PARTFUN1:def_2; assume P . (IC (Comput (P,s,k))) = halt S ; ::_thesis: Result (P,s) = Comput (P,s,k) then A2: CurInstr (P,(Comput (P,s,k))) = halt S by A1, PARTFUN1:def_6; then P halts_on s by Def8, A1; hence Result (P,s) = Comput (P,s,k) by A2, Def9; ::_thesis: verum end; theorem Th8: :: EXTPRO_1:8 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S st ex k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i))) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S st ex k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i))) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S for s being State of S st ex k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i))) let P be Instruction-Sequence of S; ::_thesis: for s being State of S st ex k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i))) let s be State of S; ::_thesis: ( ex k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S implies for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i))) ) given k being Element of NAT such that A1: P . (IC (Comput (P,s,k))) = halt S ; ::_thesis: for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i))) let i be Element of NAT ; ::_thesis: Result (P,s) = Result (P,(Comput (P,s,i))) A2: dom P = NAT by PARTFUN1:def_2; set s9 = Comput (P,s,k); A3: CurInstr (P,(Comput (P,s,k))) = halt S by A1, A2, PARTFUN1:def_6; now__::_thesis:_Result_(P,s)_=_Result_(P,(Comput_(P,s,i))) percases ( i <= k or i >= k ) ; suppose i <= k ; ::_thesis: Result (P,s) = Result (P,(Comput (P,s,i))) then consider j being Nat such that A4: k = i + j by NAT_1:10; reconsider j = j as Element of NAT by ORDINAL1:def_12; A5: Comput (P,s,k) = Comput (P,(Comput (P,s,i)),j) by A4, Th4; A6: P halts_on Comput (P,s,i) by A3, A5, Def8, A2; thus Result (P,s) = Comput (P,s,k) by A1, Th7 .= Result (P,(Comput (P,s,i))) by A3, A5, A6, Def9 ; ::_thesis: verum end; supposeA7: i >= k ; ::_thesis: Result (P,s) = Result (P,(Comput (P,s,i))) A8: Comput (P,(Comput (P,s,k)),0) = Comput (P,s,k) ; A9: Comput (P,s,i) = Comput (P,s,k) by A3, A7, Th5; A10: P halts_on Comput (P,s,i) by Def8, A2, A9, A3, A8; thus Result (P,s) = Comput (P,s,k) by A1, Th7 .= Result (P,(Comput (P,s,i))) by A3, A9, A8, A10, Def9 ; ::_thesis: verum end; end; end; hence Result (P,s) = Result (P,(Comput (P,s,i))) ; ::_thesis: verum end; definition let N be non empty with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; let p be NAT -defined the InstructionsF of S -valued Function; let IT be PartState of S; attrIT is p -autonomic means :Def10: :: EXTPRO_1:def 10 for P, Q being Instruction-Sequence of S st p c= P & p c= Q holds for s1, s2 being State of S st IT c= s1 & IT c= s2 holds for i being Element of NAT holds (Comput (P,s1,i)) | (dom IT) = (Comput (Q,s2,i)) | (dom IT); end; :: deftheorem Def10 defines -autonomic EXTPRO_1:def_10_:_ for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for IT being PartState of S holds ( IT is p -autonomic iff for P, Q being Instruction-Sequence of S st p c= P & p c= Q holds for s1, s2 being State of S st IT c= s1 & IT c= s2 holds for i being Element of NAT holds (Comput (P,s1,i)) | (dom IT) = (Comput (Q,s2,i)) | (dom IT) ); definition let N be non empty with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; let p be NAT -defined the InstructionsF of S -valued Function; let IT be PartState of S; attrIT is p -halted means :Def11: :: EXTPRO_1:def 11 for s being State of S st IT c= s holds for P being Instruction-Sequence of S st p c= P holds P halts_on s; end; :: deftheorem Def11 defines -halted EXTPRO_1:def_11_:_ for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for IT being PartState of S holds ( IT is p -halted iff for s being State of S st IT c= s holds for P being Instruction-Sequence of S st p c= P holds P halts_on s ); registration let N be non empty with_zero set ; cluster non empty with_non-empty_values IC-Ins-separated strict halting for AMI-Struct over N; existence ex b1 being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st ( b1 is halting & b1 is strict ) proof take Trivial-AMI N ; ::_thesis: ( Trivial-AMI N is halting & Trivial-AMI N is strict ) thus ( Trivial-AMI N is halting & Trivial-AMI N is strict ) ; ::_thesis: verum end; end; begin theorem Th9: :: EXTPRO_1:9 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for l being Element of NAT for I being Instruction of S for P being NAT -defined the InstructionsF of b2 -valued Function st l .--> I c= P holds for s being State of S st (IC ) .--> l c= s holds CurInstr (P,s) = I proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for l being Element of NAT for I being Instruction of S for P being NAT -defined the InstructionsF of b1 -valued Function st l .--> I c= P holds for s being State of S st (IC ) .--> l c= s holds CurInstr (P,s) = I let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for l being Element of NAT for I being Instruction of S for P being NAT -defined the InstructionsF of S -valued Function st l .--> I c= P holds for s being State of S st (IC ) .--> l c= s holds CurInstr (P,s) = I let l be Element of NAT ; ::_thesis: for I being Instruction of S for P being NAT -defined the InstructionsF of S -valued Function st l .--> I c= P holds for s being State of S st (IC ) .--> l c= s holds CurInstr (P,s) = I let I be Instruction of S; ::_thesis: for P being NAT -defined the InstructionsF of S -valued Function st l .--> I c= P holds for s being State of S st (IC ) .--> l c= s holds CurInstr (P,s) = I let P be NAT -defined the InstructionsF of S -valued Function; ::_thesis: ( l .--> I c= P implies for s being State of S st (IC ) .--> l c= s holds CurInstr (P,s) = I ) assume A1: l .--> I c= P ; ::_thesis: for s being State of S st (IC ) .--> l c= s holds CurInstr (P,s) = I let s be State of S; ::_thesis: ( (IC ) .--> l c= s implies CurInstr (P,s) = I ) assume A2: (IC ) .--> l c= s ; ::_thesis: CurInstr (P,s) = I dom ((IC ) .--> l) = {(IC )} by FUNCOP_1:13; then IC in dom ((IC ) .--> l) by TARSKI:def_1; then A3: IC s = ((IC ) .--> l) . (IC ) by A2, GRFUNC_1:2 .= l by FUNCOP_1:72 ; dom (l .--> I) = {l} by FUNCOP_1:13; then A4: IC s in dom (l .--> I) by A3, TARSKI:def_1; dom (l .--> I) c= dom P by A1, RELAT_1:11; hence CurInstr (P,s) = P . (IC s) by A4, PARTFUN1:def_6 .= (l .--> I) . (IC s) by A4, A1, GRFUNC_1:2 .= I by A3, FUNCOP_1:72 ; ::_thesis: verum end; theorem Th10: :: EXTPRO_1:10 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for l being Element of NAT for P being NAT -defined the InstructionsF of b2 -valued Function st l .--> (halt S) c= P holds for p being b3 -started PartState of S holds p is P -halted proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for l being Element of NAT for P being NAT -defined the InstructionsF of b1 -valued Function st l .--> (halt S) c= P holds for p being b2 -started PartState of S holds p is P -halted let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for l being Element of NAT for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds for p being b1 -started PartState of S holds p is P -halted let l be Element of NAT ; ::_thesis: for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds for p being l -started PartState of S holds p is P -halted let P be NAT -defined the InstructionsF of S -valued Function; ::_thesis: ( l .--> (halt S) c= P implies for p being l -started PartState of S holds p is P -halted ) assume A1: l .--> (halt S) c= P ; ::_thesis: for p being l -started PartState of S holds p is P -halted let p be l -started PartState of S; ::_thesis: p is P -halted set h = halt S; set I = p +* P; let s be State of S; :: according to EXTPRO_1:def_11 ::_thesis: ( p c= s implies for P being Instruction-Sequence of S st P c= P holds P halts_on s ) assume A2: p c= s ; ::_thesis: for P being Instruction-Sequence of S st P c= P holds P halts_on s let Q be Instruction-Sequence of S; ::_thesis: ( P c= Q implies Q halts_on s ) assume A3: P c= Q ; ::_thesis: Q halts_on s take 0 ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (Q,s,0)) in dom Q & CurInstr (Q,(Comput (Q,s,0))) = halt S ) dom Q = NAT by PARTFUN1:def_2; hence IC (Comput (Q,s,0)) in dom Q ; ::_thesis: CurInstr (Q,(Comput (Q,s,0))) = halt S Start-At (l,S) c= p by MEMSTR_0:29; then A4: Start-At (l,S) c= s by A2, XBOOLE_1:1; A5: l .--> (halt S) c= Q by A1, A3, XBOOLE_1:1; A6: dom (l .--> (halt S)) = {l} by FUNCOP_1:13; IC in dom (Start-At (l,S)) by MEMSTR_0:15; then A7: IC s = IC (Start-At (l,S)) by A4, GRFUNC_1:2 .= l by FUNCOP_1:72 ; A8: IC s in dom (l .--> (halt S)) by A6, A7, TARSKI:def_1; A9: dom (l .--> (halt S)) c= dom Q by A5, RELAT_1:11; thus CurInstr (Q,(Comput (Q,s,0))) = CurInstr (Q,s) .= Q . (IC s) by A9, A8, PARTFUN1:def_6 .= (l .--> (halt S)) . (IC s) by A8, A5, GRFUNC_1:2 .= CurInstr ((l .--> (halt S)),s) by A8, PARTFUN1:def_6 .= halt S by A4, Th9 ; ::_thesis: verum end; theorem Th11: :: EXTPRO_1:11 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for l being Element of NAT for P being NAT -defined the InstructionsF of b2 -valued Function st l .--> (halt S) c= P holds for p being b3 -started PartState of S for s being State of S st p c= s holds for i being Element of NAT holds Comput (P,s,i) = s proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for l being Element of NAT for P being NAT -defined the InstructionsF of b1 -valued Function st l .--> (halt S) c= P holds for p being b2 -started PartState of S for s being State of S st p c= s holds for i being Element of NAT holds Comput (P,s,i) = s let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for l being Element of NAT for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds for p being b1 -started PartState of S for s being State of S st p c= s holds for i being Element of NAT holds Comput (P,s,i) = s let l be Element of NAT ; ::_thesis: for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds for p being l -started PartState of S for s being State of S st p c= s holds for i being Element of NAT holds Comput (P,s,i) = s let P be NAT -defined the InstructionsF of S -valued Function; ::_thesis: ( l .--> (halt S) c= P implies for p being l -started PartState of S for s being State of S st p c= s holds for i being Element of NAT holds Comput (P,s,i) = s ) assume A1: l .--> (halt S) c= P ; ::_thesis: for p being l -started PartState of S for s being State of S st p c= s holds for i being Element of NAT holds Comput (P,s,i) = s let p be l -started PartState of S; ::_thesis: for s being State of S st p c= s holds for i being Element of NAT holds Comput (P,s,i) = s set h = halt S; let s be State of S; ::_thesis: ( p c= s implies for i being Element of NAT holds Comput (P,s,i) = s ) assume A2: p c= s ; ::_thesis: for i being Element of NAT holds Comput (P,s,i) = s A3: Start-At (l,S) c= p by MEMSTR_0:29; defpred S1[ Element of NAT ] means Comput (P,s,\$1) = s; A4: Start-At (l,S) c= s by A3, A2, XBOOLE_1:1; A5: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_ S1[i_+_1] let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A6: S1[i] ; ::_thesis: S1[i + 1] Comput (P,s,(i + 1)) = Following (P,s) by A6, Th3 .= Exec ((halt S),s) by A4, A1, Th9 .= s by Def3 ; hence S1[i + 1] ; ::_thesis: verum end; A7: S1[ 0 ] ; thus for i being Element of NAT holds S1[i] from NAT_1:sch_1(A7, A5); ::_thesis: verum end; theorem Th12: :: EXTPRO_1:12 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for l being Element of NAT for P being NAT -defined the InstructionsF of b2 -valued Function st l .--> (halt S) c= P holds for p being b3 -started PartState of S holds p is P -autonomic proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for l being Element of NAT for P being NAT -defined the InstructionsF of b1 -valued Function st l .--> (halt S) c= P holds for p being b2 -started PartState of S holds p is P -autonomic let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for l being Element of NAT for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds for p being b1 -started PartState of S holds p is P -autonomic let l be Element of NAT ; ::_thesis: for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds for p being l -started PartState of S holds p is P -autonomic set h = halt S; set p = Start-At (l,S); let P be NAT -defined the InstructionsF of S -valued Function; ::_thesis: ( l .--> (halt S) c= P implies for p being l -started PartState of S holds p is P -autonomic ) assume A1: l .--> (halt S) c= P ; ::_thesis: for p being l -started PartState of S holds p is P -autonomic let p be l -started PartState of S; ::_thesis: p is P -autonomic set I = p +* P; let Q1, Q2 be Instruction-Sequence of S; :: according to EXTPRO_1:def_10 ::_thesis: ( P c= Q1 & P c= Q2 implies for s1, s2 being State of S st p c= s1 & p c= s2 holds for i being Element of NAT holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p) ) assume A2: ( P c= Q1 & P c= Q2 ) ; ::_thesis: for s1, s2 being State of S st p c= s1 & p c= s2 holds for i being Element of NAT holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p) let s1, s2 be State of S; ::_thesis: ( p c= s1 & p c= s2 implies for i being Element of NAT holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p) ) assume that A3: p c= s1 and A4: p c= s2 ; ::_thesis: for i being Element of NAT holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p) let i be Element of NAT ; ::_thesis: (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p) A5: ( l .--> (halt S) c= Q1 & l .--> (halt S) c= Q2 ) by A1, A2, XBOOLE_1:1; hence (Comput (Q1,s1,i)) | (dom p) = s1 | (dom p) by A3, Th11 .= p by A3, GRFUNC_1:23 .= s2 | (dom p) by A4, GRFUNC_1:23 .= (Comput (Q2,s2,i)) | (dom p) by A4, Th11, A5 ; ::_thesis: verum end; registration let N be non empty with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; let P be NAT -defined the InstructionsF of S -valued non halt-free Function; cluster non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() P -autonomic P -halted for set ; existence ex b1 being FinPartState of S st ( b1 is P -autonomic & b1 is P -halted & not b1 is empty ) proof halt S in rng P by COMPOS_1:def_11; then consider i being set such that A1: i in dom P and A2: P . i = halt S by FUNCT_1:def_3; dom P c= NAT by RELAT_1:def_18; then reconsider i = i as Element of NAT by A1; take p = Start-At (i,S); ::_thesis: ( p is P -autonomic & p is P -halted & not p is empty ) i .--> (halt S) c= P by A1, A2, FUNCT_4:85; hence ( p is P -autonomic & p is P -halted & not p is empty ) by Th10, Th12; ::_thesis: verum end; end; definition let N be non empty with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; let P be NAT -defined the InstructionsF of S -valued non halt-free Function; mode Autonomy of P -> FinPartState of S means :Def12: :: EXTPRO_1:def 12 ( it is P -autonomic & it is P -halted ); existence ex b1 being FinPartState of S st ( b1 is P -autonomic & b1 is P -halted ) proof halt S in rng P by COMPOS_1:def_11; then consider x being set such that A1: x in dom P and A2: P . x = halt S by FUNCT_1:def_3; dom P c= NAT by RELAT_1:def_18; then reconsider m = x as Element of NAT by A1; [m,(halt S)] in P by A1, A2, FUNCT_1:def_2; then {[m,(halt S)]} c= P by ZFMISC_1:31; then A3: m .--> (halt S) c= P by FUNCT_4:82; take d = Start-At (m,S); ::_thesis: ( d is P -autonomic & d is P -halted ) thus d is P -autonomic by A3, Th12; ::_thesis: d is P -halted thus d is P -halted by A3, Th10; ::_thesis: verum end; end; :: deftheorem Def12 defines Autonomy EXTPRO_1:def_12_:_ for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being NAT -defined the InstructionsF of b2 -valued non halt-free Function for b4 being FinPartState of S holds ( b4 is Autonomy of P iff ( b4 is P -autonomic & b4 is P -halted ) ); definition let N be non empty with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; let p be NAT -defined the InstructionsF of S -valued non halt-free Function; let d be FinPartState of S; assume A1: d is Autonomy of p ; func Result (p,d) -> FinPartState of S means :: EXTPRO_1:def 13 for P being Instruction-Sequence of S st p c= P holds for s being State of S st d c= s holds it = (Result (P,s)) | (dom d); existence ex b1 being FinPartState of S st for P being Instruction-Sequence of S st p c= P holds for s being State of S st d c= s holds b1 = (Result (P,s)) | (dom d) proof consider h being State of S such that A2: d c= h by PBOOLE:141; consider H being Instruction-Sequence of S such that A3: p c= H by PBOOLE:145; A4: ( d is p -halted & d is p -autonomic ) by A1, Def12; then H halts_on h by Def11, A3, A2; then consider k1 being Element of NAT such that A5: Result (H,h) = Comput (H,h,k1) and A6: CurInstr (H,(Result (H,h))) = halt S by Def9; reconsider R = (Result (H,h)) | (dom d) as FinPartState of S ; take R ; ::_thesis: for P being Instruction-Sequence of S st p c= P holds for s being State of S st d c= s holds R = (Result (P,s)) | (dom d) let P be Instruction-Sequence of S; ::_thesis: ( p c= P implies for s being State of S st d c= s holds R = (Result (P,s)) | (dom d) ) assume A7: p c= P ; ::_thesis: for s being State of S st d c= s holds R = (Result (P,s)) | (dom d) let s be State of S; ::_thesis: ( d c= s implies R = (Result (P,s)) | (dom d) ) assume A8: d c= s ; ::_thesis: R = (Result (P,s)) | (dom d) then P halts_on s by Def11, A4, A7; then consider k2 being Element of NAT such that A9: Result (P,s) = Comput (P,s,k2) and A10: CurInstr (P,(Result (P,s))) = halt S by Def9; percases ( k1 <= k2 or k1 >= k2 ) ; suppose k1 <= k2 ; ::_thesis: R = (Result (P,s)) | (dom d) then Result (H,h) = Comput (H,h,k2) by A5, A6, Th5; hence R = (Result (P,s)) | (dom d) by A9, Def10, A4, A3, A7, A8, A2; ::_thesis: verum end; suppose k1 >= k2 ; ::_thesis: R = (Result (P,s)) | (dom d) then Result (P,s) = Comput (P,s,k1) by A9, A10, Th5; hence R = (Result (P,s)) | (dom d) by A5, Def10, A4, A3, A7, A8, A2; ::_thesis: verum end; end; end; correctness uniqueness for b1, b2 being FinPartState of S st ( for P being Instruction-Sequence of S st p c= P holds for s being State of S st d c= s holds b1 = (Result (P,s)) | (dom d) ) & ( for P being Instruction-Sequence of S st p c= P holds for s being State of S st d c= s holds b2 = (Result (P,s)) | (dom d) ) holds b1 = b2; proof consider h being State of S such that A11: d c= h by PBOOLE:141; consider H being Instruction-Sequence of S such that A12: p c= H by PBOOLE:145; let p1, p2 be FinPartState of S; ::_thesis: ( ( for P being Instruction-Sequence of S st p c= P holds for s being State of S st d c= s holds p1 = (Result (P,s)) | (dom d) ) & ( for P being Instruction-Sequence of S st p c= P holds for s being State of S st d c= s holds p2 = (Result (P,s)) | (dom d) ) implies p1 = p2 ) assume that A13: for P being Instruction-Sequence of S st p c= P holds for s being State of S st d c= s holds p1 = (Result (P,s)) | (dom d) and A14: for P being Instruction-Sequence of S st p c= P holds for s being State of S st d c= s holds p2 = (Result (P,s)) | (dom d) ; ::_thesis: p1 = p2 thus p1 = (Result (H,h)) | (dom d) by A13, A11, A12 .= p2 by A14, A11, A12 ; ::_thesis: verum end; end; :: deftheorem defines Result EXTPRO_1:def_13_:_ for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued non halt-free Function for d being FinPartState of S st d is Autonomy of p holds for b5 being FinPartState of S holds ( b5 = Result (p,d) iff for P being Instruction-Sequence of S st p c= P holds for s being State of S st d c= s holds b5 = (Result (P,s)) | (dom d) ); begin definition let N be non empty with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; let p be NAT -defined the InstructionsF of S -valued non halt-free Function; let d be FinPartState of S; let F be Function; predp,d computes F means :Def14: :: EXTPRO_1:def 14 for x being set st x in dom F holds ex s being FinPartState of S st ( x = s & d +* s is Autonomy of p & F . s c= Result (p,(d +* s)) ); end; :: deftheorem Def14 defines computes EXTPRO_1:def_14_:_ for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued non halt-free Function for d being FinPartState of S for F being Function holds ( p,d computes F iff for x being set st x in dom F holds ex s being FinPartState of S st ( x = s & d +* s is Autonomy of p & F . s c= Result (p,(d +* s)) ) ); theorem :: EXTPRO_1:13 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued non halt-free Function for d being FinPartState of S holds p,d computes {} proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b1 -valued non halt-free Function for d being FinPartState of S holds p,d computes {} let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued non halt-free Function for d being FinPartState of S holds p,d computes {} let p be NAT -defined the InstructionsF of S -valued non halt-free Function; ::_thesis: for d being FinPartState of S holds p,d computes {} let d be FinPartState of S; ::_thesis: p,d computes {} let x be set ; :: according to EXTPRO_1:def_14 ::_thesis: ( x in dom {} implies ex s being FinPartState of S st ( x = s & d +* s is Autonomy of p & {} . s c= Result (p,(d +* s)) ) ) assume A1: x in dom {} ; ::_thesis: ex s being FinPartState of S st ( x = s & d +* s is Autonomy of p & {} . s c= Result (p,(d +* s)) ) then reconsider x = x as FinPartState of S ; take x ; ::_thesis: ( x = x & d +* x is Autonomy of p & {} . x c= Result (p,(d +* x)) ) thus ( x = x & d +* x is Autonomy of p & {} . x c= Result (p,(d +* x)) ) by A1; ::_thesis: verum end; theorem :: EXTPRO_1:14 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued non halt-free Function for d being FinPartState of S holds ( d is Autonomy of p iff p,d computes {} .--> (Result (p,d)) ) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b1 -valued non halt-free Function for d being FinPartState of S holds ( d is Autonomy of p iff p,d computes {} .--> (Result (p,d)) ) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued non halt-free Function for d being FinPartState of S holds ( d is Autonomy of p iff p,d computes {} .--> (Result (p,d)) ) let p be NAT -defined the InstructionsF of S -valued non halt-free Function; ::_thesis: for d being FinPartState of S holds ( d is Autonomy of p iff p,d computes {} .--> (Result (p,d)) ) let d be FinPartState of S; ::_thesis: ( d is Autonomy of p iff p,d computes {} .--> (Result (p,d)) ) thus ( d is Autonomy of p implies p,d computes {} .--> (Result (p,d)) ) ::_thesis: ( p,d computes {} .--> (Result (p,d)) implies d is Autonomy of p ) proof A1: dom ({} .--> (Result (p,d))) = {{}} by FUNCOP_1:13; assume A2: d is Autonomy of p ; ::_thesis: p,d computes {} .--> (Result (p,d)) let x be set ; :: according to EXTPRO_1:def_14 ::_thesis: ( x in dom ({} .--> (Result (p,d))) implies ex s being FinPartState of S st ( x = s & d +* s is Autonomy of p & ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) ) ) assume A3: x in dom ({} .--> (Result (p,d))) ; ::_thesis: ex s being FinPartState of S st ( x = s & d +* s is Autonomy of p & ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) ) then A4: x = {} by A1, TARSKI:def_1; then reconsider s = x as FinPartState of S by FUNCT_1:104, RELAT_1:171; take s ; ::_thesis: ( x = s & d +* s is Autonomy of p & ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) ) thus x = s ; ::_thesis: ( d +* s is Autonomy of p & ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) ) A5: d +* {} = d ; hence d +* s is Autonomy of p by A2, A3, A1, TARSKI:def_1; ::_thesis: ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) d +* s = d by A3, A1, TARSKI:def_1, A5; hence ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) by FUNCOP_1:72, A4; ::_thesis: verum end; dom ({} .--> (Result (p,d))) = {{}} by FUNCOP_1:13; then A6: {} in dom ({} .--> (Result (p,d))) by TARSKI:def_1; A7: d +* {} = d ; assume p,d computes {} .--> (Result (p,d)) ; ::_thesis: d is Autonomy of p then ex s being FinPartState of S st ( {} = s & d +* s is Autonomy of p & ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) ) by A6, Def14; hence d is Autonomy of p by A7; ::_thesis: verum end; theorem :: EXTPRO_1:15 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued non halt-free Function for d being FinPartState of S holds ( d is Autonomy of p iff p,d computes {} .--> {} ) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b1 -valued non halt-free Function for d being FinPartState of S holds ( d is Autonomy of p iff p,d computes {} .--> {} ) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued non halt-free Function for d being FinPartState of S holds ( d is Autonomy of p iff p,d computes {} .--> {} ) let p be NAT -defined the InstructionsF of S -valued non halt-free Function; ::_thesis: for d being FinPartState of S holds ( d is Autonomy of p iff p,d computes {} .--> {} ) let d be FinPartState of S; ::_thesis: ( d is Autonomy of p iff p,d computes {} .--> {} ) thus ( d is Autonomy of p implies p,d computes {} .--> {} ) ::_thesis: ( p,d computes {} .--> {} implies d is Autonomy of p ) proof A1: dom ({} .--> {}) = {{}} by FUNCOP_1:13; assume A2: d is Autonomy of p ; ::_thesis: p,d computes {} .--> {} let x be set ; :: according to EXTPRO_1:def_14 ::_thesis: ( x in dom ({} .--> {}) implies ex s being FinPartState of S st ( x = s & d +* s is Autonomy of p & ({} .--> {}) . s c= Result (p,(d +* s)) ) ) assume A3: x in dom ({} .--> {}) ; ::_thesis: ex s being FinPartState of S st ( x = s & d +* s is Autonomy of p & ({} .--> {}) . s c= Result (p,(d +* s)) ) then A4: x = {} by A1, TARSKI:def_1; then reconsider s = x as FinPartState of S by FUNCT_1:104, RELAT_1:171; take s ; ::_thesis: ( x = s & d +* s is Autonomy of p & ({} .--> {}) . s c= Result (p,(d +* s)) ) A5: d +* {} = d ; thus x = s ; ::_thesis: ( d +* s is Autonomy of p & ({} .--> {}) . s c= Result (p,(d +* s)) ) thus d +* s is Autonomy of p by A2, A3, A5, A1, TARSKI:def_1; ::_thesis: ({} .--> {}) . s c= Result (p,(d +* s)) ({} .--> {}) . s = {} by A4, FUNCOP_1:72; hence ({} .--> {}) . s c= Result (p,(d +* s)) by XBOOLE_1:2; ::_thesis: verum end; dom ({} .--> {}) = {{}} by FUNCOP_1:13; then A6: {} in dom ({} .--> {}) by TARSKI:def_1; A7: d +* {} = d ; assume p,d computes {} .--> {} ; ::_thesis: d is Autonomy of p then ex s being FinPartState of S st ( {} = s & d +* s is Autonomy of p & ({} .--> {}) . s c= Result (p,(d +* s)) ) by A6, Def14; hence d is Autonomy of p by A7; ::_thesis: verum end; begin registration let N be non empty with_zero set ; cluster non empty IC-Ins-separated for AMI-Struct over N; existence ex b1 being non empty AMI-Struct over N st b1 is IC-Ins-separated proof take Trivial-AMI N ; ::_thesis: Trivial-AMI N is IC-Ins-separated thus Trivial-AMI N is IC-Ins-separated ; ::_thesis: verum end; end; begin theorem Th16: :: EXTPRO_1:16 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S holds ( p halts_on s iff ex i being Element of NAT st p halts_at IC (Comput (p,s,i)) ) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b1 -valued Function for s being State of S holds ( p halts_on s iff ex i being Element of NAT st p halts_at IC (Comput (p,s,i)) ) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued Function for s being State of S holds ( p halts_on s iff ex i being Element of NAT st p halts_at IC (Comput (p,s,i)) ) let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S holds ( p halts_on s iff ex i being Element of NAT st p halts_at IC (Comput (p,s,i)) ) let s be State of S; ::_thesis: ( p halts_on s iff ex i being Element of NAT st p halts_at IC (Comput (p,s,i)) ) hereby ::_thesis: ( ex i being Element of NAT st p halts_at IC (Comput (p,s,i)) implies p halts_on s ) assume p halts_on s ; ::_thesis: ex i being Element of NAT st p halts_at IC (Comput (p,s,i)) then consider i being Nat such that A1: IC (Comput (p,s,i)) in dom p and A2: CurInstr (p,(Comput (p,s,i))) = halt S by Def8; reconsider i = i as Element of NAT by ORDINAL1:def_12; take i = i; ::_thesis: p halts_at IC (Comput (p,s,i)) p . (IC (Comput (p,s,i))) = halt S by A1, A2, PARTFUN1:def_6; hence p halts_at IC (Comput (p,s,i)) by A1, COMPOS_1:def_12; ::_thesis: verum end; given i being Element of NAT such that A3: p halts_at IC (Comput (p,s,i)) ; ::_thesis: p halts_on s A4: IC (Comput (p,s,i)) in dom p by A3, COMPOS_1:def_12; A5: p . (IC (Comput (p,s,i))) = halt S by A3, COMPOS_1:def_12; take i ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (p,s,i)) in dom p & CurInstr (p,(Comput (p,s,i))) = halt S ) thus IC (Comput (p,s,i)) in dom p by A3, COMPOS_1:def_12; ::_thesis: CurInstr (p,(Comput (p,s,i))) = halt S thus CurInstr (p,(Comput (p,s,i))) = halt S by A4, A5, PARTFUN1:def_6; ::_thesis: verum end; theorem Th17: :: EXTPRO_1:17 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S for k being Nat st p halts_on s holds ( Result (p,s) = Comput (p,s,k) iff p halts_at IC (Comput (p,s,k)) ) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b1 -valued Function for s being State of S for k being Nat st p halts_on s holds ( Result (p,s) = Comput (p,s,k) iff p halts_at IC (Comput (p,s,k)) ) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued Function for s being State of S for k being Nat st p halts_on s holds ( Result (p,s) = Comput (p,s,k) iff p halts_at IC (Comput (p,s,k)) ) let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S for k being Nat st p halts_on s holds ( Result (p,s) = Comput (p,s,k) iff p halts_at IC (Comput (p,s,k)) ) let s be State of S; ::_thesis: for k being Nat st p halts_on s holds ( Result (p,s) = Comput (p,s,k) iff p halts_at IC (Comput (p,s,k)) ) let k be Nat; ::_thesis: ( p halts_on s implies ( Result (p,s) = Comput (p,s,k) iff p halts_at IC (Comput (p,s,k)) ) ) assume A1: p halts_on s ; ::_thesis: ( Result (p,s) = Comput (p,s,k) iff p halts_at IC (Comput (p,s,k)) ) then consider n being Nat such that A2: IC (Comput (p,s,n)) in dom p and A3: CurInstr (p,(Comput (p,s,n))) = halt S by Def8; hereby ::_thesis: ( p halts_at IC (Comput (p,s,k)) implies Result (p,s) = Comput (p,s,k) ) assume A4: Result (p,s) = Comput (p,s,k) ; ::_thesis: p halts_at IC (Comput (p,s,k)) consider i being Element of NAT such that A5: Result (p,s) = Comput (p,s,i) and A6: CurInstr (p,(Result (p,s))) = halt S by A1, Def9; reconsider i = i, n = n as Element of NAT by ORDINAL1:def_12; A7: now__::_thesis:_Comput_(p,s,i)_=_Comput_(p,s,n) percases ( i <= n or n <= i ) ; suppose i <= n ; ::_thesis: Comput (p,s,i) = Comput (p,s,n) hence Comput (p,s,i) = Comput (p,s,n) by A5, A6, Th5; ::_thesis: verum end; suppose n <= i ; ::_thesis: Comput (p,s,i) = Comput (p,s,n) hence Comput (p,s,i) = Comput (p,s,n) by A3, Th5; ::_thesis: verum end; end; end; p . (IC (Comput (p,s,k))) = halt S by A7, A6, A4, A2, A5, PARTFUN1:def_6; hence p halts_at IC (Comput (p,s,k)) by A7, A2, A5, A4, COMPOS_1:def_12; ::_thesis: verum end; assume that A8: IC (Comput (p,s,k)) in dom p and A9: p . (IC (Comput (p,s,k))) = halt S ; :: according to COMPOS_1:def_12 ::_thesis: Result (p,s) = Comput (p,s,k) A10: CurInstr (p,(Comput (p,s,k))) = halt S by A8, A9, PARTFUN1:def_6; reconsider k = k, n = n as Element of NAT by ORDINAL1:def_12; now__::_thesis:_Comput_(p,s,k)_=_Comput_(p,s,n) percases ( n <= k or k <= n ) ; suppose n <= k ; ::_thesis: Comput (p,s,k) = Comput (p,s,n) hence Comput (p,s,k) = Comput (p,s,n) by A3, Th5; ::_thesis: verum end; suppose k <= n ; ::_thesis: Comput (p,s,k) = Comput (p,s,n) hence Comput (p,s,k) = Comput (p,s,n) by A10, Th5; ::_thesis: verum end; end; end; hence Result (p,s) = Comput (p,s,k) by A3, Def9, A1; ::_thesis: verum end; theorem Th18: :: EXTPRO_1:18 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being NAT -defined the InstructionsF of b2 -valued Function for s being State of S for k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds Result (P,s) = Comput (P,s,k) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being NAT -defined the InstructionsF of b1 -valued Function for s being State of S for k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds Result (P,s) = Comput (P,s,k) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being NAT -defined the InstructionsF of S -valued Function for s being State of S for k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds Result (P,s) = Comput (P,s,k) let P be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S for k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds Result (P,s) = Comput (P,s,k) let s be State of S; ::_thesis: for k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds Result (P,s) = Comput (P,s,k) let k be Element of NAT ; ::_thesis: ( P halts_at IC (Comput (P,s,k)) implies Result (P,s) = Comput (P,s,k) ) assume A1: P halts_at IC (Comput (P,s,k)) ; ::_thesis: Result (P,s) = Comput (P,s,k) then P halts_on s by Th16; hence Result (P,s) = Comput (P,s,k) by A1, Th17; ::_thesis: verum end; theorem Th19: :: EXTPRO_1:19 for i, j being Element of NAT for N being non empty with_zero set st i <= j holds for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being NAT -defined the InstructionsF of b4 -valued Function for s being State of S st P halts_at IC (Comput (P,s,i)) holds P halts_at IC (Comput (P,s,j)) proof let i, j be Element of NAT ; ::_thesis: for N being non empty with_zero set st i <= j holds for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being NAT -defined the InstructionsF of b2 -valued Function for s being State of S st P halts_at IC (Comput (P,s,i)) holds P halts_at IC (Comput (P,s,j)) let N be non empty with_zero set ; ::_thesis: ( i <= j implies for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being NAT -defined the InstructionsF of b1 -valued Function for s being State of S st P halts_at IC (Comput (P,s,i)) holds P halts_at IC (Comput (P,s,j)) ) assume A1: i <= j ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being NAT -defined the InstructionsF of b1 -valued Function for s being State of S st P halts_at IC (Comput (P,s,i)) holds P halts_at IC (Comput (P,s,j)) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being NAT -defined the InstructionsF of S -valued Function for s being State of S st P halts_at IC (Comput (P,s,i)) holds P halts_at IC (Comput (P,s,j)) let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S st p halts_at IC (Comput (p,s,i)) holds p halts_at IC (Comput (p,s,j)) let s be State of S; ::_thesis: ( p halts_at IC (Comput (p,s,i)) implies p halts_at IC (Comput (p,s,j)) ) assume that A2: IC (Comput (p,s,i)) in dom p and A3: p . (IC (Comput (p,s,i))) = halt S ; :: according to COMPOS_1:def_12 ::_thesis: p halts_at IC (Comput (p,s,j)) A4: CurInstr (p,(Comput (p,s,i))) = halt S by A2, A3, PARTFUN1:def_6; hence IC (Comput (p,s,j)) in dom p by A2, A1, Th5; :: according to COMPOS_1:def_12 ::_thesis: p . (IC (Comput (p,s,j))) = halt S thus p . (IC (Comput (p,s,j))) = halt S by A1, A3, A4, Th5; ::_thesis: verum end; theorem :: EXTPRO_1:20 for i, j being Element of NAT for N being non empty with_zero set st i <= j holds for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being NAT -defined the InstructionsF of b4 -valued Function for s being State of S st P halts_at IC (Comput (P,s,i)) holds Comput (P,s,j) = Comput (P,s,i) proof let i, j be Element of NAT ; ::_thesis: for N being non empty with_zero set st i <= j holds for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being NAT -defined the InstructionsF of b2 -valued Function for s being State of S st P halts_at IC (Comput (P,s,i)) holds Comput (P,s,j) = Comput (P,s,i) let N be non empty with_zero set ; ::_thesis: ( i <= j implies for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being NAT -defined the InstructionsF of b1 -valued Function for s being State of S st P halts_at IC (Comput (P,s,i)) holds Comput (P,s,j) = Comput (P,s,i) ) assume A1: i <= j ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being NAT -defined the InstructionsF of b1 -valued Function for s being State of S st P halts_at IC (Comput (P,s,i)) holds Comput (P,s,j) = Comput (P,s,i) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being NAT -defined the InstructionsF of S -valued Function for s being State of S st P halts_at IC (Comput (P,s,i)) holds Comput (P,s,j) = Comput (P,s,i) let P be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S st P halts_at IC (Comput (P,s,i)) holds Comput (P,s,j) = Comput (P,s,i) let s be State of S; ::_thesis: ( P halts_at IC (Comput (P,s,i)) implies Comput (P,s,j) = Comput (P,s,i) ) assume A2: P halts_at IC (Comput (P,s,i)) ; ::_thesis: Comput (P,s,j) = Comput (P,s,i) then P halts_at IC (Comput (P,s,j)) by A1, Th19; hence Comput (P,s,j) = Result (P,s) by Th18 .= Comput (P,s,i) by A2, Th18 ; ::_thesis: verum end; theorem :: EXTPRO_1:21 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S st ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i))) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S st ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i))) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S for s being State of S st ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i))) let P be Instruction-Sequence of S; ::_thesis: for s being State of S st ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i))) let s be State of S; ::_thesis: ( ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) implies for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i))) ) given k being Element of NAT such that A1: P halts_at IC (Comput (P,s,k)) ; ::_thesis: for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i))) let i be Element of NAT ; ::_thesis: Result (P,s) = Result (P,(Comput (P,s,i))) P . (IC (Comput (P,s,k))) = halt S by A1, COMPOS_1:def_12; hence Result (P,s) = Result (P,(Comput (P,s,i))) by Th8; ::_thesis: verum end; definition let N be non empty with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; let p be NAT -defined the InstructionsF of S -valued Function; let s be State of S; assume X1: p halts_on s ; func LifeSpan (p,s) -> Element of NAT means :Def15: :: EXTPRO_1:def 15 ( CurInstr (p,(Comput (p,s,it))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds it <= k ) ); existence ex b1 being Element of NAT st ( CurInstr (p,(Comput (p,s,b1))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds b1 <= k ) ) proof defpred S1[ Nat] means CurInstr (p,(Comput (p,s,\$1))) = halt S; consider k being Nat such that IC (Comput (p,s,k)) in dom p and A1: CurInstr (p,(Comput (p,s,k))) = halt S by X1, Def8; A2: ex k being Nat st S1[k] by A1; consider k being Nat such that A3: ( S1[k] & ( for n being Nat st S1[n] holds k <= n ) ) from NAT_1:sch_5(A2); reconsider k = k as Element of NAT by ORDINAL1:def_12; take k ; ::_thesis: ( CurInstr (p,(Comput (p,s,k))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds k <= k ) ) thus ( CurInstr (p,(Comput (p,s,k))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds k <= k ) ) by A3; ::_thesis: verum end; uniqueness for b1, b2 being Element of NAT st CurInstr (p,(Comput (p,s,b1))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds b1 <= k ) & CurInstr (p,(Comput (p,s,b2))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds b2 <= k ) holds b1 = b2 proof let it1, it2 be Element of NAT ; ::_thesis: ( CurInstr (p,(Comput (p,s,it1))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds it1 <= k ) & CurInstr (p,(Comput (p,s,it2))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds it2 <= k ) implies it1 = it2 ) assume A4: ( CurInstr (p,(Comput (p,s,it1))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds it1 <= k ) & CurInstr (p,(Comput (p,s,it2))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds it2 <= k ) & not it1 = it2 ) ; ::_thesis: contradiction then ( it1 <= it2 & it2 <= it1 ) ; hence contradiction by A4, XXREAL_0:1; ::_thesis: verum end; end; :: deftheorem Def15 defines LifeSpan EXTPRO_1:def_15_:_ for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S st p halts_on s holds for b5 being Element of NAT holds ( b5 = LifeSpan (p,s) iff ( CurInstr (p,(Comput (p,s,b5))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds b5 <= k ) ) ); theorem Th22: :: EXTPRO_1:22 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S for m being Element of NAT holds ( p halts_on s iff p halts_on Comput (p,s,m) ) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b1 -valued Function for s being State of S for m being Element of NAT holds ( p halts_on s iff p halts_on Comput (p,s,m) ) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued Function for s being State of S for m being Element of NAT holds ( p halts_on s iff p halts_on Comput (p,s,m) ) let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S for m being Element of NAT holds ( p halts_on s iff p halts_on Comput (p,s,m) ) let s be State of S; ::_thesis: for m being Element of NAT holds ( p halts_on s iff p halts_on Comput (p,s,m) ) let m be Element of NAT ; ::_thesis: ( p halts_on s iff p halts_on Comput (p,s,m) ) hereby ::_thesis: ( p halts_on Comput (p,s,m) implies p halts_on s ) assume p halts_on s ; ::_thesis: p halts_on Comput (p,s,m) then consider n being Nat such that A1: IC (Comput (p,s,n)) in dom p and A2: CurInstr (p,(Comput (p,s,n))) = halt S by Def8; reconsider n = n as Element of NAT by ORDINAL1:def_12; percases ( n <= m or n >= m ) ; suppose n <= m ; ::_thesis: p halts_on Comput (p,s,m) then Comput (p,s,n) = Comput (p,s,(m + 0)) by A2, Th5 .= Comput (p,(Comput (p,s,m)),0) ; hence p halts_on Comput (p,s,m) by Def8, A2, A1; ::_thesis: verum end; suppose n >= m ; ::_thesis: p halts_on Comput (p,s,m) then reconsider k = n - m as Element of NAT by INT_1:5; Comput (p,(Comput (p,s,m)),k) = Comput (p,s,(m + k)) by Th4 .= Comput (p,s,n) ; hence p halts_on Comput (p,s,m) by Def8, A1, A2; ::_thesis: verum end; end; end; given n being Nat such that A3: IC (Comput (p,(Comput (p,s,m)),n)) in dom p and A4: CurInstr (p,(Comput (p,(Comput (p,s,m)),n))) = halt S ; :: according to EXTPRO_1:def_8 ::_thesis: p halts_on s reconsider nn = n as Element of NAT by ORDINAL1:def_12; take m + nn ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (p,s,(m + nn))) in dom p & CurInstr (p,(Comput (p,s,(m + nn)))) = halt S ) thus ( IC (Comput (p,s,(m + nn))) in dom p & CurInstr (p,(Comput (p,s,(m + nn)))) = halt S ) by A3, A4, Th4; ::_thesis: verum end; theorem :: EXTPRO_1:23 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S st p halts_on s holds Result (p,s) = Comput (p,s,(LifeSpan (p,s))) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b1 -valued Function for s being State of S st p halts_on s holds Result (p,s) = Comput (p,s,(LifeSpan (p,s))) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued Function for s being State of S st p halts_on s holds Result (p,s) = Comput (p,s,(LifeSpan (p,s))) let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S st p halts_on s holds Result (p,s) = Comput (p,s,(LifeSpan (p,s))) let s be State of S; ::_thesis: ( p halts_on s implies Result (p,s) = Comput (p,s,(LifeSpan (p,s))) ) assume A1: p halts_on s ; ::_thesis: Result (p,s) = Comput (p,s,(LifeSpan (p,s))) then A2: CurInstr (p,(Comput (p,s,(LifeSpan (p,s))))) = halt S by Def15; consider m being Element of NAT such that A3: Result (p,s) = Comput (p,s,m) and A4: CurInstr (p,(Result (p,s))) = halt S by A1, Def9; LifeSpan (p,s) <= m by A1, A3, A4, Def15; hence Result (p,s) = Comput (p,s,(LifeSpan (p,s))) by A2, A3, Th5; ::_thesis: verum end; theorem :: EXTPRO_1:24 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S holds Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S holds Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S for s being State of S for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S holds Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k) let P be Instruction-Sequence of S; ::_thesis: for s being State of S for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S holds Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k) let s be State of S; ::_thesis: for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S holds Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k) let k be Element of NAT ; ::_thesis: ( CurInstr (P,(Comput (P,s,k))) = halt S implies Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k) ) assume A1: CurInstr (P,(Comput (P,s,k))) = halt S ; ::_thesis: Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k) A2: dom P = NAT by PARTFUN1:def_2; A3: P halts_on s by Def8, A2, A1; set Ls = LifeSpan (P,s); A4: CurInstr (P,(Comput (P,s,(LifeSpan (P,s))))) = halt S by A3, Def15; LifeSpan (P,s) <= k by A1, A3, Def15; hence Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k) by A4, Th5; ::_thesis: verum end; theorem :: EXTPRO_1:25 for j being Element of NAT for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b3 -valued Function for s being State of S st LifeSpan (p,s) <= j & p halts_on s holds Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s))) proof let j be Element of NAT ; ::_thesis: for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S st LifeSpan (p,s) <= j & p halts_on s holds Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s))) let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b1 -valued Function for s being State of S st LifeSpan (p,s) <= j & p halts_on s holds Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s))) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued Function for s being State of S st LifeSpan (p,s) <= j & p halts_on s holds Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s))) let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S st LifeSpan (p,s) <= j & p halts_on s holds Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s))) let s be State of S; ::_thesis: ( LifeSpan (p,s) <= j & p halts_on s implies Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s))) ) assume that A1: LifeSpan (p,s) <= j and A2: p halts_on s ; ::_thesis: Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s))) CurInstr (p,(Comput (p,s,(LifeSpan (p,s))))) = halt S by A2, Def15; hence Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s))) by A1, Th5; ::_thesis: verum end; theorem :: EXTPRO_1:26 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for e being Nat for I being Instruction of S for t being b3 -started State of S for u being Instruction-Sequence of S st e .--> I c= u holds Following (u,t) = Exec (I,t) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for e being Nat for I being Instruction of S for t being b2 -started State of S for u being Instruction-Sequence of S st e .--> I c= u holds Following (u,t) = Exec (I,t) let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for e being Nat for I being Instruction of S for t being b1 -started State of S for u being Instruction-Sequence of S st e .--> I c= u holds Following (u,t) = Exec (I,t) let e be Nat; ::_thesis: for I being Instruction of S for t being e -started State of S for u being Instruction-Sequence of S st e .--> I c= u holds Following (u,t) = Exec (I,t) let I be Instruction of S; ::_thesis: for t being e -started State of S for u being Instruction-Sequence of S st e .--> I c= u holds Following (u,t) = Exec (I,t) let t be e -started State of S; ::_thesis: for u being Instruction-Sequence of S st e .--> I c= u holds Following (u,t) = Exec (I,t) let u be Instruction-Sequence of S; ::_thesis: ( e .--> I c= u implies Following (u,t) = Exec (I,t) ) assume A1: e .--> I c= u ; ::_thesis: Following (u,t) = Exec (I,t) dom (e .--> I) = {e} by FUNCOP_1:13; then A2: e in dom (e .--> I) by TARSKI:def_1; IC t = e by MEMSTR_0:def_11; then CurInstr (u,t) = u . e by PBOOLE:143 .= (e .--> I) . e by A1, A2, GRFUNC_1:2 .= I by FUNCOP_1:72 ; hence Following (u,t) = Exec (I,t) ; ::_thesis: verum end; theorem :: EXTPRO_1:27 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S st s = Following (P,s) holds for n being Element of NAT holds Comput (P,s,n) = s proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S st s = Following (P,s) holds for n being Element of NAT holds Comput (P,s,n) = s let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S for s being State of S st s = Following (P,s) holds for n being Element of NAT holds Comput (P,s,n) = s let P be Instruction-Sequence of S; ::_thesis: for s being State of S st s = Following (P,s) holds for n being Element of NAT holds Comput (P,s,n) = s let s be State of S; ::_thesis: ( s = Following (P,s) implies for n being Element of NAT holds Comput (P,s,n) = s ) defpred S1[ Element of NAT ] means Comput (P,s,\$1) = s; assume s = Following (P,s) ; ::_thesis: for n being Element of NAT holds Comput (P,s,n) = s then A1: for n being Element of NAT st S1[n] holds S1[n + 1] by Th3; A2: S1[ 0 ] ; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1); ::_thesis: verum end; theorem :: EXTPRO_1:28 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for P being Instruction-Sequence of S for s being State of S for i being Instruction of S holds (Exec ((P . (IC s)),s)) . (IC ) = IC (Following (P,s)) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for P being Instruction-Sequence of S for s being State of S for i being Instruction of S holds (Exec ((P . (IC s)),s)) . (IC ) = IC (Following (P,s)) let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S for s being State of S for i being Instruction of S holds (Exec ((P . (IC s)),s)) . (IC ) = IC (Following (P,s)) let P be Instruction-Sequence of S; ::_thesis: for s being State of S for i being Instruction of S holds (Exec ((P . (IC s)),s)) . (IC ) = IC (Following (P,s)) let s be State of S; ::_thesis: for i being Instruction of S holds (Exec ((P . (IC s)),s)) . (IC ) = IC (Following (P,s)) let i be Instruction of S; ::_thesis: (Exec ((P . (IC s)),s)) . (IC ) = IC (Following (P,s)) NAT = dom P by PARTFUN1:def_2; hence (Exec ((P . (IC s)),s)) . (IC ) = IC (Following (P,s)) by PARTFUN1:def_6; ::_thesis: verum end; theorem :: EXTPRO_1:29 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S holds ( P halts_on s iff ex k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S ) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S holds ( P halts_on s iff ex k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S ) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S for s being State of S holds ( P halts_on s iff ex k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S ) let P be Instruction-Sequence of S; ::_thesis: for s being State of S holds ( P halts_on s iff ex k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S ) let s be State of S; ::_thesis: ( P halts_on s iff ex k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S ) thus ( P halts_on s implies ex k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S ) ::_thesis: ( ex k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S implies P halts_on s ) proof given k being Nat such that IC (Comput (P,s,k)) in dom P and A1: CurInstr (P,(Comput (P,s,k))) = halt S ; :: according to EXTPRO_1:def_8 ::_thesis: ex k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S reconsider k = k as Element of NAT by ORDINAL1:def_12; take k ; ::_thesis: CurInstr (P,(Comput (P,s,k))) = halt S thus CurInstr (P,(Comput (P,s,k))) = halt S by A1; ::_thesis: verum end; given k being Element of NAT such that A2: CurInstr (P,(Comput (P,s,k))) = halt S ; ::_thesis: P halts_on s take k ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,k)) in dom P & CurInstr (P,(Comput (P,s,k))) = halt S ) IC (Comput (P,s,k)) in NAT ; hence IC (Comput (P,s,k)) in dom P by PARTFUN1:def_2; ::_thesis: CurInstr (P,(Comput (P,s,k))) = halt S thus CurInstr (P,(Comput (P,s,k))) = halt S by A2; ::_thesis: verum end; theorem Th30: :: EXTPRO_1:30 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for F being Instruction-Sequence of S for s being State of S st ex k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds F halts_on s proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for F being Instruction-Sequence of S for s being State of S st ex k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds F halts_on s let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for F being Instruction-Sequence of S for s being State of S st ex k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds F halts_on s let F be Instruction-Sequence of S; ::_thesis: for s being State of S st ex k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds F halts_on s let s be State of S; ::_thesis: ( ex k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S implies F halts_on s ) given k being Element of NAT such that A1: F . (IC (Comput (F,s,k))) = halt S ; ::_thesis: F halts_on s take k ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (F,s,k)) in dom F & CurInstr (F,(Comput (F,s,k))) = halt S ) A2: dom F = NAT by PARTFUN1:def_2; hence IC (Comput (F,s,k)) in dom F ; ::_thesis: CurInstr (F,(Comput (F,s,k))) = halt S thus CurInstr (F,(Comput (F,s,k))) = halt S by A1, A2, PARTFUN1:def_6; ::_thesis: verum end; theorem :: EXTPRO_1:31 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for F being Instruction-Sequence of S for s being State of S for k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds Result (F,s) = Comput (F,s,k) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for F being Instruction-Sequence of S for s being State of S for k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds Result (F,s) = Comput (F,s,k) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for F being Instruction-Sequence of S for s being State of S for k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds Result (F,s) = Comput (F,s,k) let F be Instruction-Sequence of S; ::_thesis: for s being State of S for k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds Result (F,s) = Comput (F,s,k) let s be State of S; ::_thesis: for k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds Result (F,s) = Comput (F,s,k) let k be Element of NAT ; ::_thesis: ( F . (IC (Comput (F,s,k))) = halt S implies Result (F,s) = Comput (F,s,k) ) assume A1: F . (IC (Comput (F,s,k))) = halt S ; ::_thesis: Result (F,s) = Comput (F,s,k) then A2: F halts_on s by Th30; dom F = NAT by PARTFUN1:def_2; then CurInstr (F,(Comput (F,s,k))) = halt S by A1, PARTFUN1:def_6; hence Result (F,s) = Comput (F,s,k) by A2, Def9; ::_thesis: verum end; theorem Th32: :: EXTPRO_1:32 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for F being Instruction-Sequence of S for s being State of S for k being Element of NAT holds ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 & F halts_on s ) ) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for F being Instruction-Sequence of S for s being State of S for k being Element of NAT holds ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 & F halts_on s ) ) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for F being Instruction-Sequence of S for s being State of S for k being Element of NAT holds ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 & F halts_on s ) ) let F be Instruction-Sequence of S; ::_thesis: for s being State of S for k being Element of NAT holds ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 & F halts_on s ) ) let s be State of S; ::_thesis: for k being Element of NAT holds ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 & F halts_on s ) ) let k be Element of NAT ; ::_thesis: ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 & F halts_on s ) ) A1: dom F = NAT by PARTFUN1:def_2; hereby ::_thesis: ( LifeSpan (F,s) = k + 1 & F halts_on s implies ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S ) ) assume that A2: F . (IC (Comput (F,s,k))) <> halt S and A3: F . (IC (Comput (F,s,(k + 1)))) = halt S ; ::_thesis: ( LifeSpan (F,s) = k + 1 & F halts_on s ) A4: CurInstr (F,(Comput (F,s,k))) <> halt S by A2, A1, PARTFUN1:def_6; A5: now__::_thesis:_for_i_being_Element_of_NAT_st_CurInstr_(F,(Comput_(F,s,i)))_=_halt_S_holds_ not_k_+_1_>_i let i be Element of NAT ; ::_thesis: ( CurInstr (F,(Comput (F,s,i))) = halt S implies not k + 1 > i ) assume that A6: CurInstr (F,(Comput (F,s,i))) = halt S and A7: k + 1 > i ; ::_thesis: contradiction i <= k by A7, NAT_1:13; hence contradiction by A4, A6, Th5; ::_thesis: verum end; A8: F halts_on s by A3, Th30; CurInstr (F,(Comput (F,s,(k + 1)))) = halt S by A3, A1, PARTFUN1:def_6; hence ( LifeSpan (F,s) = k + 1 & F halts_on s ) by A5, Def15, A8; ::_thesis: verum end; assume A9: ( LifeSpan (F,s) = k + 1 & F halts_on s ) ; ::_thesis: ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S ) A10: now__::_thesis:_not_CurInstr_(F,(Comput_(F,s,k)))_=_halt_S assume CurInstr (F,(Comput (F,s,k))) = halt S ; ::_thesis: contradiction then k + 1 <= k by A9, Def15; hence contradiction by NAT_1:13; ::_thesis: verum end; CurInstr (F,(Comput (F,s,(k + 1)))) = halt S by A9, Def15; hence ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S ) by A10, A1, PARTFUN1:def_6; ::_thesis: verum end; theorem :: EXTPRO_1:33 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for F being Instruction-Sequence of S for s being State of S for k being Element of NAT st IC (Comput (F,s,k)) <> IC (Comput (F,s,(k + 1))) & F . (IC (Comput (F,s,(k + 1)))) = halt S holds LifeSpan (F,s) = k + 1 proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for F being Instruction-Sequence of S for s being State of S for k being Element of NAT st IC (Comput (F,s,k)) <> IC (Comput (F,s,(k + 1))) & F . (IC (Comput (F,s,(k + 1)))) = halt S holds LifeSpan (F,s) = k + 1 let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for F being Instruction-Sequence of S for s being State of S for k being Element of NAT st IC (Comput (F,s,k)) <> IC (Comput (F,s,(k + 1))) & F . (IC (Comput (F,s,(k + 1)))) = halt S holds LifeSpan (F,s) = k + 1 let F be Instruction-Sequence of S; ::_thesis: for s being State of S for k being Element of NAT st IC (Comput (F,s,k)) <> IC (Comput (F,s,(k + 1))) & F . (IC (Comput (F,s,(k + 1)))) = halt S holds LifeSpan (F,s) = k + 1 let s be State of S; ::_thesis: for k being Element of NAT st IC (Comput (F,s,k)) <> IC (Comput (F,s,(k + 1))) & F . (IC (Comput (F,s,(k + 1)))) = halt S holds LifeSpan (F,s) = k + 1 let k be Element of NAT ; ::_thesis: ( IC (Comput (F,s,k)) <> IC (Comput (F,s,(k + 1))) & F . (IC (Comput (F,s,(k + 1)))) = halt S implies LifeSpan (F,s) = k + 1 ) assume that A1: IC (Comput (F,s,k)) <> IC (Comput (F,s,(k + 1))) and A2: F . (IC (Comput (F,s,(k + 1)))) = halt S ; ::_thesis: LifeSpan (F,s) = k + 1 A3: dom F = NAT by PARTFUN1:def_2; now__::_thesis:_not_F_._(IC_(Comput_(F,s,k)))_=_halt_S assume F . (IC (Comput (F,s,k))) = halt S ; ::_thesis: contradiction then CurInstr (F,(Comput (F,s,k))) = halt S by A3, PARTFUN1:def_6; hence contradiction by A1, Th5, NAT_1:11; ::_thesis: verum end; hence LifeSpan (F,s) = k + 1 by A2, Th32; ::_thesis: verum end; theorem :: EXTPRO_1:34 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for F being Instruction-Sequence of S for s being State of S for k being Element of NAT st F halts_on Comput (F,s,k) & 0 < LifeSpan (F,(Comput (F,s,k))) holds LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k)))) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for F being Instruction-Sequence of S for s being State of S for k being Element of NAT st F halts_on Comput (F,s,k) & 0 < LifeSpan (F,(Comput (F,s,k))) holds LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k)))) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for F being Instruction-Sequence of S for s being State of S for k being Element of NAT st F halts_on Comput (F,s,k) & 0 < LifeSpan (F,(Comput (F,s,k))) holds LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k)))) let F be Instruction-Sequence of S; ::_thesis: for s being State of S for k being Element of NAT st F halts_on Comput (F,s,k) & 0 < LifeSpan (F,(Comput (F,s,k))) holds LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k)))) let s be State of S; ::_thesis: for k being Element of NAT st F halts_on Comput (F,s,k) & 0 < LifeSpan (F,(Comput (F,s,k))) holds LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k)))) let k be Element of NAT ; ::_thesis: ( F halts_on Comput (F,s,k) & 0 < LifeSpan (F,(Comput (F,s,k))) implies LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k)))) ) set s2 = Comput (F,s,k); set c = LifeSpan (F,(Comput (F,s,k))); assume that A1: F halts_on Comput (F,s,k) and A2: 0 < LifeSpan (F,(Comput (F,s,k))) ; ::_thesis: LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k)))) consider l being Nat such that A3: LifeSpan (F,(Comput (F,s,k))) = l + 1 by A2, NAT_1:6; reconsider l = l as Element of NAT by ORDINAL1:def_12; F . (IC (Comput (F,(Comput (F,s,k)),(l + 1)))) = halt S by A1, A3, Th32; then A4: F . (IC (Comput (F,s,(k + (l + 1))))) = halt S by Th4; F . (IC (Comput (F,(Comput (F,s,k)),l))) <> halt S by A1, A3, Th32; then F . (IC (Comput (F,s,(k + l)))) <> halt S by Th4; hence LifeSpan (F,s) = (k + l) + 1 by A4, Th32 .= k + (LifeSpan (F,(Comput (F,s,k)))) by A3 ; ::_thesis: verum end; theorem :: EXTPRO_1:35 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for F being Instruction-Sequence of S for s being State of S for k being Element of NAT st F halts_on Comput (F,s,k) holds Result (F,(Comput (F,s,k))) = Result (F,s) proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for F being Instruction-Sequence of S for s being State of S for k being Element of NAT st F halts_on Comput (F,s,k) holds Result (F,(Comput (F,s,k))) = Result (F,s) let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for F being Instruction-Sequence of S for s being State of S for k being Element of NAT st F halts_on Comput (F,s,k) holds Result (F,(Comput (F,s,k))) = Result (F,s) let F be Instruction-Sequence of S; ::_thesis: for s being State of S for k being Element of NAT st F halts_on Comput (F,s,k) holds Result (F,(Comput (F,s,k))) = Result (F,s) let s be State of S; ::_thesis: for k being Element of NAT st F halts_on Comput (F,s,k) holds Result (F,(Comput (F,s,k))) = Result (F,s) let k be Element of NAT ; ::_thesis: ( F halts_on Comput (F,s,k) implies Result (F,(Comput (F,s,k))) = Result (F,s) ) set s2 = Comput (F,s,k); assume A1: F halts_on Comput (F,s,k) ; ::_thesis: Result (F,(Comput (F,s,k))) = Result (F,s) then consider l being Element of NAT such that A2: ( Result (F,(Comput (F,s,k))) = Comput (F,(Comput (F,s,k)),l) & CurInstr (F,(Result (F,(Comput (F,s,k))))) = halt S ) by Def9; A3: F halts_on s by A1, Th22; Comput (F,(Comput (F,s,k)),l) = Comput (F,s,(k + l)) by Th4; hence Result (F,(Comput (F,s,k))) = Result (F,s) by A3, A2, Def9; ::_thesis: verum end; theorem :: EXTPRO_1:36 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S st P halts_on s holds for k being Element of NAT st LifeSpan (P,s) <= k holds CurInstr (P,(Comput (P,s,k))) = halt S proof let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S st P halts_on s holds for k being Element of NAT st LifeSpan (P,s) <= k holds CurInstr (P,(Comput (P,s,k))) = halt S let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S for s being State of S st P halts_on s holds for k being Element of NAT st LifeSpan (P,s) <= k holds CurInstr (P,(Comput (P,s,k))) = halt S let P be Instruction-Sequence of S; ::_thesis: for s being State of S st P halts_on s holds for k being Element of NAT st LifeSpan (P,s) <= k holds CurInstr (P,(Comput (P,s,k))) = halt S let s be State of S; ::_thesis: ( P halts_on s implies for k being Element of NAT st LifeSpan (P,s) <= k holds CurInstr (P,(Comput (P,s,k))) = halt S ) assume P halts_on s ; ::_thesis: for k being Element of NAT st LifeSpan (P,s) <= k holds CurInstr (P,(Comput (P,s,k))) = halt S then A1: CurInstr (P,(Comput (P,s,(LifeSpan (P,s))))) = halt S by Def15; let k be Element of NAT ; ::_thesis: ( LifeSpan (P,s) <= k implies CurInstr (P,(Comput (P,s,k))) = halt S ) assume LifeSpan (P,s) <= k ; ::_thesis: CurInstr (P,(Comput (P,s,k))) = halt S hence CurInstr (P,(Comput (P,s,k))) = halt S by A1, Th5; ::_thesis: verum end;