:: by Grzegorz Bancerek and Piotr Rudnicki

::

:: Received December 30, 1993

:: Copyright (c) 1993-2019 Association of Mizar Users

Lm1: 1 = { n where n is Nat : n < 1 }

by AXIOMS:4;

Lm2: 5 = { n where n is Nat : n < 5 }

by AXIOMS:4;

definition

ex b_{1} being non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr st

( Terminals b_{1} = SCM-Data-Loc & NonTerminals b_{1} = [:1,5:] & ( for x, y, z being Symbol of b_{1} holds

( x ==> <*y,z*> iff x in [:1,5:] ) ) )

for b_{1}, b_{2} being non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr st Terminals b_{1} = SCM-Data-Loc & NonTerminals b_{1} = [:1,5:] & ( for x, y, z being Symbol of b_{1} holds

( x ==> <*y,z*> iff x in [:1,5:] ) ) & Terminals b_{2} = SCM-Data-Loc & NonTerminals b_{2} = [:1,5:] & ( for x, y, z being Symbol of b_{2} holds

( x ==> <*y,z*> iff x in [:1,5:] ) ) holds

b_{1} = b_{2}
end;

func SCM-AE -> non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr means :Def1: :: SCM_COMP:def 1

( Terminals it = SCM-Data-Loc & NonTerminals it = [:1,5:] & ( for x, y, z being Symbol of it holds

( x ==> <*y,z*> iff x in [:1,5:] ) ) );

existence ( Terminals it = SCM-Data-Loc & NonTerminals it = [:1,5:] & ( for x, y, z being Symbol of it holds

( x ==> <*y,z*> iff x in [:1,5:] ) ) );

ex b

( Terminals b

( x ==> <*y,z*> iff x in [:1,5:] ) ) )

proof end;

uniqueness for b

( x ==> <*y,z*> iff x in [:1,5:] ) ) & Terminals b

( x ==> <*y,z*> iff x in [:1,5:] ) ) holds

b

proof end;

:: deftheorem Def1 defines SCM-AE SCM_COMP:def 1 :

for b_{1} being non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr holds

( b_{1} = SCM-AE iff ( Terminals b_{1} = SCM-Data-Loc & NonTerminals b_{1} = [:1,5:] & ( for x, y, z being Symbol of b_{1} holds

( x ==> <*y,z*> iff x in [:1,5:] ) ) ) );

for b

( b

( x ==> <*y,z*> iff x in [:1,5:] ) ) ) );

Lm3: NonTerminals SCM-AE = [:1,5:]

by Def1;

definition

let nt be NonTerminal of SCM-AE;

let tl, tr be bin-term;

:: original: -tree

redefine func nt -tree (tl,tr) -> bin-term;

coherence

nt -tree (tl,tr) is bin-term

end;
let tl, tr be bin-term;

:: original: -tree

redefine func nt -tree (tl,tr) -> bin-term;

coherence

nt -tree (tl,tr) is bin-term

proof end;

definition

let t be Terminal of SCM-AE;

:: original: root-tree

redefine func root-tree t -> bin-term;

coherence

root-tree t is bin-term by DTCONSTR:def 1;

end;
:: original: root-tree

redefine func root-tree t -> bin-term;

coherence

root-tree t is bin-term by DTCONSTR:def 1;

then reconsider nt0 = [0,0], nt1 = [0,1], nt2 = [0,2], nt3 = [0,3], nt4 = [0,4] as NonTerminal of SCM-AE ;

definition

let t1, t2 be bin-term;

coherence

[0,0] -tree (t1,t2) is bin-term

[0,1] -tree (t1,t2) is bin-term

[0,2] -tree (t1,t2) is bin-term

[0,3] -tree (t1,t2) is bin-term

[0,4] -tree (t1,t2) is bin-term

end;
coherence

[0,0] -tree (t1,t2) is bin-term

proof end;

coherence [0,1] -tree (t1,t2) is bin-term

proof end;

coherence [0,2] -tree (t1,t2) is bin-term

proof end;

coherence [0,3] -tree (t1,t2) is bin-term

proof end;

coherence [0,4] -tree (t1,t2) is bin-term

proof end;

:: deftheorem defines + SCM_COMP:def 3 :

for t1, t2 being bin-term holds t1 + t2 = [0,0] -tree (t1,t2);

for t1, t2 being bin-term holds t1 + t2 = [0,0] -tree (t1,t2);

:: deftheorem defines - SCM_COMP:def 4 :

for t1, t2 being bin-term holds t1 - t2 = [0,1] -tree (t1,t2);

for t1, t2 being bin-term holds t1 - t2 = [0,1] -tree (t1,t2);

:: deftheorem defines * SCM_COMP:def 5 :

for t1, t2 being bin-term holds t1 * t2 = [0,2] -tree (t1,t2);

for t1, t2 being bin-term holds t1 * t2 = [0,2] -tree (t1,t2);

:: deftheorem defines div SCM_COMP:def 6 :

for t1, t2 being bin-term holds t1 div t2 = [0,3] -tree (t1,t2);

for t1, t2 being bin-term holds t1 div t2 = [0,3] -tree (t1,t2);

:: deftheorem defines mod SCM_COMP:def 7 :

for t1, t2 being bin-term holds t1 mod t2 = [0,4] -tree (t1,t2);

for t1, t2 being bin-term holds t1 mod t2 = [0,4] -tree (t1,t2);

theorem :: SCM_COMP:3

for term being bin-term holds

( ex t being Terminal of SCM-AE st term = root-tree t or ex tl, tr being bin-term st

( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) )

( ex t being Terminal of SCM-AE st term = root-tree t or ex tl, tr being bin-term st

( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) )

proof end;

definition

let o be NonTerminal of SCM-AE;

let i, j be Integer;

( ( o = [0,0] implies i + j is Integer ) & ( o = [0,1] implies i - j is Integer ) & ( o = [0,2] implies i * j is Integer ) & ( o = [0,3] implies i div j is Integer ) & ( o = [0,4] implies i mod j is Integer ) ) ;

consistency

for b_{1} being Integer holds

( ( o = [0,0] & o = [0,1] implies ( b_{1} = i + j iff b_{1} = i - j ) ) & ( o = [0,0] & o = [0,2] implies ( b_{1} = i + j iff b_{1} = i * j ) ) & ( o = [0,0] & o = [0,3] implies ( b_{1} = i + j iff b_{1} = i div j ) ) & ( o = [0,0] & o = [0,4] implies ( b_{1} = i + j iff b_{1} = i mod j ) ) & ( o = [0,1] & o = [0,2] implies ( b_{1} = i - j iff b_{1} = i * j ) ) & ( o = [0,1] & o = [0,3] implies ( b_{1} = i - j iff b_{1} = i div j ) ) & ( o = [0,1] & o = [0,4] implies ( b_{1} = i - j iff b_{1} = i mod j ) ) & ( o = [0,2] & o = [0,3] implies ( b_{1} = i * j iff b_{1} = i div j ) ) & ( o = [0,2] & o = [0,4] implies ( b_{1} = i * j iff b_{1} = i mod j ) ) & ( o = [0,3] & o = [0,4] implies ( b_{1} = i div j iff b_{1} = i mod j ) ) )

end;
let i, j be Integer;

func o -Meaning_on (i,j) -> Integer equals :Def8: :: SCM_COMP:def 8

i + j if o = [0,0]

i - j if o = [0,1]

i * j if o = [0,2]

i div j if o = [0,3]

i mod j if o = [0,4]

;

coherence i + j if o = [0,0]

i - j if o = [0,1]

i * j if o = [0,2]

i div j if o = [0,3]

i mod j if o = [0,4]

;

( ( o = [0,0] implies i + j is Integer ) & ( o = [0,1] implies i - j is Integer ) & ( o = [0,2] implies i * j is Integer ) & ( o = [0,3] implies i div j is Integer ) & ( o = [0,4] implies i mod j is Integer ) ) ;

consistency

for b

( ( o = [0,0] & o = [0,1] implies ( b

proof end;

:: deftheorem Def8 defines -Meaning_on SCM_COMP:def 8 :

for o being NonTerminal of SCM-AE

for i, j being Integer holds

( ( o = [0,0] implies o -Meaning_on (i,j) = i + j ) & ( o = [0,1] implies o -Meaning_on (i,j) = i - j ) & ( o = [0,2] implies o -Meaning_on (i,j) = i * j ) & ( o = [0,3] implies o -Meaning_on (i,j) = i div j ) & ( o = [0,4] implies o -Meaning_on (i,j) = i mod j ) );

for o being NonTerminal of SCM-AE

for i, j being Integer holds

( ( o = [0,0] implies o -Meaning_on (i,j) = i + j ) & ( o = [0,1] implies o -Meaning_on (i,j) = i - j ) & ( o = [0,2] implies o -Meaning_on (i,j) = i * j ) & ( o = [0,3] implies o -Meaning_on (i,j) = i div j ) & ( o = [0,4] implies o -Meaning_on (i,j) = i mod j ) );

registration
end;

definition

let D be non empty set ;

let f be Function of INT,D;

let x be Integer;

:: original: .

redefine func f . x -> Element of D;

coherence

f . x is Element of D

end;
let f be Function of INT,D;

let x be Integer;

:: original: .

redefine func f . x -> Element of D;

coherence

f . x is Element of D

proof end;

set i2i = id INT;

deffunc H

definition

let s be State of SCM;

let term be bin-term;

ex b_{1} being Integer ex f being Function of (TS SCM-AE),INT st

( b_{1} = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) )

for b_{1}, b_{2} being Integer st ex f being Function of (TS SCM-AE),INT st

( b_{1} = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) ) & ex f being Function of (TS SCM-AE),INT st

( b_{2} = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) ) holds

b_{1} = b_{2}

end;
let term be bin-term;

func term @ s -> Integer means :Def9: :: SCM_COMP:def 9

ex f being Function of (TS SCM-AE),INT st

( it = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) );

existence ex f being Function of (TS SCM-AE),INT st

( it = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) );

ex b

( b

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) )

proof end;

uniqueness for b

( b

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) ) & ex f being Function of (TS SCM-AE),INT st

( b

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) ) holds

b

proof end;

:: deftheorem Def9 defines @ SCM_COMP:def 9 :

for s being State of SCM

for term being bin-term

for b_{3} being Integer holds

( b_{3} = term @ s iff ex f being Function of (TS SCM-AE),INT st

( b_{3} = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) ) );

for s being State of SCM

for term being bin-term

for b

( b

( b

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) ) );

theorem Th5: :: SCM_COMP:5

for s being State of SCM

for nt being NonTerminal of SCM-AE

for tl, tr being bin-term holds (nt -tree (tl,tr)) @ s = nt -Meaning_on ((tl @ s),(tr @ s))

for nt being NonTerminal of SCM-AE

for tl, tr being bin-term holds (nt -tree (tl,tr)) @ s = nt -Meaning_on ((tl @ s),(tr @ s))

proof end;

theorem :: SCM_COMP:6

for s being State of SCM

for tl, tr being bin-term holds

( (tl + tr) @ s = (tl @ s) + (tr @ s) & (tl - tr) @ s = (tl @ s) - (tr @ s) & (tl * tr) @ s = (tl @ s) * (tr @ s) & (tl div tr) @ s = (tl @ s) div (tr @ s) & (tl mod tr) @ s = (tl @ s) mod (tr @ s) )

for tl, tr being bin-term holds

( (tl + tr) @ s = (tl @ s) + (tr @ s) & (tl - tr) @ s = (tl @ s) - (tr @ s) & (tl * tr) @ s = (tl @ s) * (tr @ s) & (tl div tr) @ s = (tl @ s) div (tr @ s) & (tl mod tr) @ s = (tl @ s) mod (tr @ s) )

proof end;

definition

let nt be NonTerminal of SCM-AE;

let n be Nat;

( ( nt = [0,0] implies <%(AddTo ((dl. n),(dl. (n + 1))))%> is XFinSequence of the InstructionsF of SCM ) & ( nt = [0,1] implies <%(SubFrom ((dl. n),(dl. (n + 1))))%> is XFinSequence of the InstructionsF of SCM ) & ( nt = [0,2] implies <%(MultBy ((dl. n),(dl. (n + 1))))%> is XFinSequence of the InstructionsF of SCM ) & ( nt = [0,3] implies <%(Divide ((dl. n),(dl. (n + 1))))%> is XFinSequence of the InstructionsF of SCM ) & ( nt = [0,4] implies <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> is XFinSequence of the InstructionsF of SCM ) ) ;

consistency

for b_{1} being XFinSequence of the InstructionsF of SCM holds

( ( nt = [0,0] & nt = [0,1] implies ( b_{1} = <%(AddTo ((dl. n),(dl. (n + 1))))%> iff b_{1} = <%(SubFrom ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,0] & nt = [0,2] implies ( b_{1} = <%(AddTo ((dl. n),(dl. (n + 1))))%> iff b_{1} = <%(MultBy ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,0] & nt = [0,3] implies ( b_{1} = <%(AddTo ((dl. n),(dl. (n + 1))))%> iff b_{1} = <%(Divide ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,0] & nt = [0,4] implies ( b_{1} = <%(AddTo ((dl. n),(dl. (n + 1))))%> iff b_{1} = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) ) & ( nt = [0,1] & nt = [0,2] implies ( b_{1} = <%(SubFrom ((dl. n),(dl. (n + 1))))%> iff b_{1} = <%(MultBy ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,1] & nt = [0,3] implies ( b_{1} = <%(SubFrom ((dl. n),(dl. (n + 1))))%> iff b_{1} = <%(Divide ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,1] & nt = [0,4] implies ( b_{1} = <%(SubFrom ((dl. n),(dl. (n + 1))))%> iff b_{1} = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) ) & ( nt = [0,2] & nt = [0,3] implies ( b_{1} = <%(MultBy ((dl. n),(dl. (n + 1))))%> iff b_{1} = <%(Divide ((dl. n),(dl. (n + 1))))%> ) ) & ( nt = [0,2] & nt = [0,4] implies ( b_{1} = <%(MultBy ((dl. n),(dl. (n + 1))))%> iff b_{1} = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) ) & ( nt = [0,3] & nt = [0,4] implies ( b_{1} = <%(Divide ((dl. n),(dl. (n + 1))))%> iff b_{1} = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) ) )

end;
let n be Nat;

func Selfwork (nt,n) -> XFinSequence of the InstructionsF of SCM equals :Def10: :: SCM_COMP:def 10

<%(AddTo ((dl. n),(dl. (n + 1))))%> if nt = [0,0]

<%(SubFrom ((dl. n),(dl. (n + 1))))%> if nt = [0,1]

<%(MultBy ((dl. n),(dl. (n + 1))))%> if nt = [0,2]

<%(Divide ((dl. n),(dl. (n + 1))))%> if nt = [0,3]

<%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> if nt = [0,4]

;

coherence <%(AddTo ((dl. n),(dl. (n + 1))))%> if nt = [0,0]

<%(SubFrom ((dl. n),(dl. (n + 1))))%> if nt = [0,1]

<%(MultBy ((dl. n),(dl. (n + 1))))%> if nt = [0,2]

<%(Divide ((dl. n),(dl. (n + 1))))%> if nt = [0,3]

<%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> if nt = [0,4]

;

( ( nt = [0,0] implies <%(AddTo ((dl. n),(dl. (n + 1))))%> is XFinSequence of the InstructionsF of SCM ) & ( nt = [0,1] implies <%(SubFrom ((dl. n),(dl. (n + 1))))%> is XFinSequence of the InstructionsF of SCM ) & ( nt = [0,2] implies <%(MultBy ((dl. n),(dl. (n + 1))))%> is XFinSequence of the InstructionsF of SCM ) & ( nt = [0,3] implies <%(Divide ((dl. n),(dl. (n + 1))))%> is XFinSequence of the InstructionsF of SCM ) & ( nt = [0,4] implies <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> is XFinSequence of the InstructionsF of SCM ) ) ;

consistency

for b

( ( nt = [0,0] & nt = [0,1] implies ( b

proof end;

:: deftheorem Def10 defines Selfwork SCM_COMP:def 10 :

for nt being NonTerminal of SCM-AE

for n being Nat holds

( ( nt = [0,0] implies Selfwork (nt,n) = <%(AddTo ((dl. n),(dl. (n + 1))))%> ) & ( nt = [0,1] implies Selfwork (nt,n) = <%(SubFrom ((dl. n),(dl. (n + 1))))%> ) & ( nt = [0,2] implies Selfwork (nt,n) = <%(MultBy ((dl. n),(dl. (n + 1))))%> ) & ( nt = [0,3] implies Selfwork (nt,n) = <%(Divide ((dl. n),(dl. (n + 1))))%> ) & ( nt = [0,4] implies Selfwork (nt,n) = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) );

for nt being NonTerminal of SCM-AE

for n being Nat holds

( ( nt = [0,0] implies Selfwork (nt,n) = <%(AddTo ((dl. n),(dl. (n + 1))))%> ) & ( nt = [0,1] implies Selfwork (nt,n) = <%(SubFrom ((dl. n),(dl. (n + 1))))%> ) & ( nt = [0,2] implies Selfwork (nt,n) = <%(MultBy ((dl. n),(dl. (n + 1))))%> ) & ( nt = [0,3] implies Selfwork (nt,n) = <%(Divide ((dl. n),(dl. (n + 1))))%> ) & ( nt = [0,4] implies Selfwork (nt,n) = <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> ) );

definition

deffunc H_{2}( NonTerminal of SCM-AE, sequence of ( the InstructionsF of SCM ^omega), sequence of ( the InstructionsF of SCM ^omega), Nat) -> Element of the InstructionsF of SCM ^omega = (($2 . (In ($4,NAT))) ^ ($3 . (In (($4 + 1),NAT)))) ^ (Down (Selfwork ($1,$4)));

deffunc H_{3}( Terminal of SCM-AE, Nat) -> Element of the InstructionsF of SCM ^omega = Down <%((dl. $2) := (@ $1))%>;

ex b_{1} being Function of (TS SCM-AE),(Funcs (NAT,( the InstructionsF of SCM ^omega))) st

( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = b_{1} . (root-tree t) & ( for n being Nat holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE

for t1, t2 being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = b_{1} . (nt -tree (t1,t2)) & f1 = b_{1} . t1 & f2 = b_{1} . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) )

for b_{1}, b_{2} being Function of (TS SCM-AE),(Funcs (NAT,( the InstructionsF of SCM ^omega))) st ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = b_{1} . (root-tree t) & ( for n being Nat holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE

for t1, t2 being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = b_{1} . (nt -tree (t1,t2)) & f1 = b_{1} . t1 & f2 = b_{1} . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) & ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = b_{2} . (root-tree t) & ( for n being Nat holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE

for t1, t2 being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = b_{2} . (nt -tree (t1,t2)) & f1 = b_{2} . t1 & f2 = b_{2} . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) holds

b_{1} = b_{2}

end;
deffunc H

func SCM-Compile -> Function of (TS SCM-AE),(Funcs (NAT,( the InstructionsF of SCM ^omega))) means :Def11: :: SCM_COMP:def 11

( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = it . (root-tree t) & ( for n being Nat holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE

for t1, t2 being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = it . (nt -tree (t1,t2)) & f1 = it . t1 & f2 = it . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) );

existence ( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = it . (root-tree t) & ( for n being Nat holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE

for t1, t2 being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = it . (nt -tree (t1,t2)) & f1 = it . t1 & f2 = it . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) );

ex b

( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = b

for t1, t2 being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = b

proof end;

uniqueness for b

( g = b

for t1, t2 being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = b

( g = b

for t1, t2 being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = b

b

proof end;

:: deftheorem Def11 defines SCM-Compile SCM_COMP:def 11 :

for b_{1} being Function of (TS SCM-AE),(Funcs (NAT,( the InstructionsF of SCM ^omega))) holds

( b_{1} = SCM-Compile iff ( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = b_{1} . (root-tree t) & ( for n being Nat holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE

for t1, t2 being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = b_{1} . (nt -tree (t1,t2)) & f1 = b_{1} . t1 & f2 = b_{1} . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) ) );

for b

( b

( g = b

for t1, t2 being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = b

definition

let term be bin-term;

let aux be Nat;

(SCM-Compile . term) . aux is XFinSequence of the InstructionsF of SCM

end;
let aux be Nat;

func SCM-Compile (term,aux) -> XFinSequence of the InstructionsF of SCM equals :: SCM_COMP:def 12

(SCM-Compile . term) . aux;

coherence (SCM-Compile . term) . aux;

(SCM-Compile . term) . aux is XFinSequence of the InstructionsF of SCM

proof end;

:: deftheorem defines SCM-Compile SCM_COMP:def 12 :

for term being bin-term

for aux being Nat holds SCM-Compile (term,aux) = (SCM-Compile . term) . aux;

for term being bin-term

for aux being Nat holds SCM-Compile (term,aux) = (SCM-Compile . term) . aux;

theorem Th7: :: SCM_COMP:7

for t being Terminal of SCM-AE

for n being Element of NAT holds SCM-Compile ((root-tree t),n) = <%((dl. n) := (@ t))%>

for n being Element of NAT holds SCM-Compile ((root-tree t),n) = <%((dl. n) := (@ t))%>

proof end;

theorem Th8: :: SCM_COMP:8

for nt being NonTerminal of SCM-AE

for t1, t2 being bin-term

for n being Element of NAT

for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

SCM-Compile ((nt -tree (t1,t2)),n) = ((SCM-Compile (t1,n)) ^ (SCM-Compile (t2,(n + 1)))) ^ (Selfwork (nt,n))

for t1, t2 being bin-term

for n being Element of NAT

for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

SCM-Compile ((nt -tree (t1,t2)),n) = ((SCM-Compile (t1,n)) ^ (SCM-Compile (t2,(n + 1)))) ^ (Selfwork (nt,n))

proof end;

definition

let t be Terminal of SCM-AE;

existence

ex b_{1} being Element of NAT st dl. b_{1} = t

for b_{1}, b_{2} being Element of NAT st dl. b_{1} = t & dl. b_{2} = t holds

b_{1} = b_{2}
by AMI_3:10;

end;
existence

ex b

proof end;

uniqueness for b

b

:: deftheorem Def13 defines d". SCM_COMP:def 13 :

for t being Terminal of SCM-AE

for b_{2} being Element of NAT holds

( b_{2} = d". t iff dl. b_{2} = t );

for t being Terminal of SCM-AE

for b

( b

definition

deffunc H_{2}( Terminal of SCM-AE) -> Element of NAT = d". $1;

deffunc H_{3}( NonTerminal of SCM-AE, set , set , Element of NAT , Element of NAT ) -> Element of NAT = max ($4,$5);

let term be bin-term;

ex b_{1} being Element of NAT ex f being Function of (TS SCM-AE),NAT st

( b_{1} = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = max (xl,xr) ) )

for b_{1}, b_{2} being Element of NAT st ex f being Function of (TS SCM-AE),NAT st

( b_{1} = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = max (xl,xr) ) ) & ex f being Function of (TS SCM-AE),NAT st

( b_{2} = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = max (xl,xr) ) ) holds

b_{1} = b_{2}

end;
deffunc H

let term be bin-term;

func max_Data-Loc_in term -> Element of NAT means :Def14: :: SCM_COMP:def 14

ex f being Function of (TS SCM-AE),NAT st

( it = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = max (xl,xr) ) );

existence ex f being Function of (TS SCM-AE),NAT st

( it = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = max (xl,xr) ) );

ex b

( b

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = max (xl,xr) ) )

proof end;

uniqueness for b

( b

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = max (xl,xr) ) ) & ex f being Function of (TS SCM-AE),NAT st

( b

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = max (xl,xr) ) ) holds

b

proof end;

:: deftheorem Def14 defines max_Data-Loc_in SCM_COMP:def 14 :

for term being bin-term

for b_{2} being Element of NAT holds

( b_{2} = max_Data-Loc_in term iff ex f being Function of (TS SCM-AE),NAT st

( b_{2} = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = max (xl,xr) ) ) );

for term being bin-term

for b

( b

( b

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = max (xl,xr) ) ) );

set Term = the bin-term;

consider f being Function of (TS SCM-AE),NAT such that

max_Data-Loc_in the bin-term = f . the bin-term and

Lm4: for t being Terminal of SCM-AE holds f . (root-tree t) = d". t and

Lm5: for nt being NonTerminal of SCM-AE

for tl, tr being bin-term

for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = max (xl,xr) by Def14;

Lm6: NonTerminals SCM-AE = [:1,5:]

by Def1;

theorem Th10: :: SCM_COMP:10

for nt being NonTerminal of SCM-AE

for tl, tr being bin-term holds max_Data-Loc_in (nt -tree (tl,tr)) = max ((max_Data-Loc_in tl),(max_Data-Loc_in tr))

for tl, tr being bin-term holds max_Data-Loc_in (nt -tree (tl,tr)) = max ((max_Data-Loc_in tl),(max_Data-Loc_in tr))

proof end;

defpred S

s1 . (dl. dn) = s2 . (dl. dn) ) holds

$1 @ s1 = $1 @ s2;

Lm7: now :: thesis: for s being Terminal of SCM-AE holds S_{1}[ root-tree s]

let s be Terminal of SCM-AE; :: thesis: S_{1}[ root-tree s]

thus S_{1}[ root-tree s]
:: thesis: verum

end;
thus S

proof

let s1, s2 be State of SCM; :: thesis: ( ( for dn being Element of NAT st dn <= max_Data-Loc_in (root-tree s) holds

s1 . (dl. dn) = s2 . (dl. dn) ) implies (root-tree s) @ s1 = (root-tree s) @ s2 )

assume A1: for dn being Element of NAT st dn <= max_Data-Loc_in (root-tree s) holds

s1 . (dl. dn) = s2 . (dl. dn) ; :: thesis: (root-tree s) @ s1 = (root-tree s) @ s2

d". s <= max_Data-Loc_in (root-tree s) by Th9;

then A2: s1 . (dl. (d". s)) = s2 . (dl. (d". s)) by A1;

A3: (root-tree s) @ s1 = s1 . s by Th4;

( s1 . s = s1 . (dl. (d". s)) & s2 . s = s2 . (dl. (d". s)) ) by Def13;

hence (root-tree s) @ s1 = (root-tree s) @ s2 by A2, A3, Th4; :: thesis: verum

end;
s1 . (dl. dn) = s2 . (dl. dn) ) implies (root-tree s) @ s1 = (root-tree s) @ s2 )

assume A1: for dn being Element of NAT st dn <= max_Data-Loc_in (root-tree s) holds

s1 . (dl. dn) = s2 . (dl. dn) ; :: thesis: (root-tree s) @ s1 = (root-tree s) @ s2

d". s <= max_Data-Loc_in (root-tree s) by Th9;

then A2: s1 . (dl. (d". s)) = s2 . (dl. (d". s)) by A1;

A3: (root-tree s) @ s1 = s1 . s by Th4;

( s1 . s = s1 . (dl. (d". s)) & s2 . s = s2 . (dl. (d". s)) ) by Def13;

hence (root-tree s) @ s1 = (root-tree s) @ s2 by A2, A3, Th4; :: thesis: verum

Lm8: now :: thesis: for nt being NonTerminal of SCM-AE

for tl, tr being Element of TS SCM-AE st nt ==> <*(root-label tl),(root-label tr)*> & S_{1}[tl] & S_{1}[tr] holds

S_{1}[nt -tree (tl,tr)]

for tl, tr being Element of TS SCM-AE st nt ==> <*(root-label tl),(root-label tr)*> & S

S

let nt be NonTerminal of SCM-AE; :: thesis: for tl, tr being Element of TS SCM-AE st nt ==> <*(root-label tl),(root-label tr)*> & S_{1}[tl] & S_{1}[tr] holds

S_{1}[nt -tree (tl,tr)]

let tl, tr be Element of TS SCM-AE; :: thesis: ( nt ==> <*(root-label tl),(root-label tr)*> & S_{1}[tl] & S_{1}[tr] implies S_{1}[nt -tree (tl,tr)] )

assume that

nt ==> <*(root-label tl),(root-label tr)*> and

A1: S_{1}[tl]
and

A2: S_{1}[tr]
; :: thesis: S_{1}[nt -tree (tl,tr)]

thus S_{1}[nt -tree (tl,tr)]
:: thesis: verum

end;
S

let tl, tr be Element of TS SCM-AE; :: thesis: ( nt ==> <*(root-label tl),(root-label tr)*> & S

assume that

nt ==> <*(root-label tl),(root-label tr)*> and

A1: S

A2: S

thus S

proof

let s1, s2 be State of SCM; :: thesis: ( ( for dn being Element of NAT st dn <= max_Data-Loc_in (nt -tree (tl,tr)) holds

s1 . (dl. dn) = s2 . (dl. dn) ) implies (nt -tree (tl,tr)) @ s1 = (nt -tree (tl,tr)) @ s2 )

assume A3: for dn being Element of NAT st dn <= max_Data-Loc_in (nt -tree (tl,tr)) holds

s1 . (dl. dn) = s2 . (dl. dn) ; :: thesis: (nt -tree (tl,tr)) @ s1 = (nt -tree (tl,tr)) @ s2

(nt -tree (tl,tr)) @ s1 = nt -Meaning_on ((tl @ s1),(tr @ s1)) by Th5;

hence (nt -tree (tl,tr)) @ s1 = (nt -tree (tl,tr)) @ s2 by A5, A7, Th5; :: thesis: verum

end;
s1 . (dl. dn) = s2 . (dl. dn) ) implies (nt -tree (tl,tr)) @ s1 = (nt -tree (tl,tr)) @ s2 )

assume A3: for dn being Element of NAT st dn <= max_Data-Loc_in (nt -tree (tl,tr)) holds

s1 . (dl. dn) = s2 . (dl. dn) ; :: thesis: (nt -tree (tl,tr)) @ s1 = (nt -tree (tl,tr)) @ s2

now :: thesis: for dn being Element of NAT st dn <= max_Data-Loc_in tl holds

s1 . (dl. dn) = s2 . (dl. dn)

then A5:
tl @ s1 = tl @ s2
by A1;s1 . (dl. dn) = s2 . (dl. dn)

set ml = max_Data-Loc_in tl;

set mr = max_Data-Loc_in tr;

let dn be Element of NAT ; :: thesis: ( dn <= max_Data-Loc_in tl implies s1 . (dl. dn) = s2 . (dl. dn) )

A4: max_Data-Loc_in tl <= max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) by XXREAL_0:25;

assume dn <= max_Data-Loc_in tl ; :: thesis: s1 . (dl. dn) = s2 . (dl. dn)

then dn <= max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) by A4, XXREAL_0:2;

then dn <= max_Data-Loc_in (nt -tree (tl,tr)) by Th10;

hence s1 . (dl. dn) = s2 . (dl. dn) by A3; :: thesis: verum

end;
set mr = max_Data-Loc_in tr;

let dn be Element of NAT ; :: thesis: ( dn <= max_Data-Loc_in tl implies s1 . (dl. dn) = s2 . (dl. dn) )

A4: max_Data-Loc_in tl <= max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) by XXREAL_0:25;

assume dn <= max_Data-Loc_in tl ; :: thesis: s1 . (dl. dn) = s2 . (dl. dn)

then dn <= max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) by A4, XXREAL_0:2;

then dn <= max_Data-Loc_in (nt -tree (tl,tr)) by Th10;

hence s1 . (dl. dn) = s2 . (dl. dn) by A3; :: thesis: verum

now :: thesis: for dn being Element of NAT st dn <= max_Data-Loc_in tr holds

s1 . (dl. dn) = s2 . (dl. dn)

then A7:
tr @ s1 = tr @ s2
by A2;s1 . (dl. dn) = s2 . (dl. dn)

set ml = max_Data-Loc_in tl;

set mr = max_Data-Loc_in tr;

let dn be Element of NAT ; :: thesis: ( dn <= max_Data-Loc_in tr implies s1 . (dl. dn) = s2 . (dl. dn) )

A6: max_Data-Loc_in tr <= max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) by XXREAL_0:25;

assume dn <= max_Data-Loc_in tr ; :: thesis: s1 . (dl. dn) = s2 . (dl. dn)

then dn <= max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) by A6, XXREAL_0:2;

then dn <= max_Data-Loc_in (nt -tree (tl,tr)) by Th10;

hence s1 . (dl. dn) = s2 . (dl. dn) by A3; :: thesis: verum

end;
set mr = max_Data-Loc_in tr;

let dn be Element of NAT ; :: thesis: ( dn <= max_Data-Loc_in tr implies s1 . (dl. dn) = s2 . (dl. dn) )

A6: max_Data-Loc_in tr <= max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) by XXREAL_0:25;

assume dn <= max_Data-Loc_in tr ; :: thesis: s1 . (dl. dn) = s2 . (dl. dn)

then dn <= max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) by A6, XXREAL_0:2;

then dn <= max_Data-Loc_in (nt -tree (tl,tr)) by Th10;

hence s1 . (dl. dn) = s2 . (dl. dn) by A3; :: thesis: verum

(nt -tree (tl,tr)) @ s1 = nt -Meaning_on ((tl @ s1),(tr @ s1)) by Th5;

hence (nt -tree (tl,tr)) @ s1 = (nt -tree (tl,tr)) @ s2 by A5, A7, Th5; :: thesis: verum

theorem Th11: :: SCM_COMP:11

for term being bin-term

for s1, s2 being State of SCM st ( for dn being Element of NAT st dn <= max_Data-Loc_in term holds

s1 . (dl. dn) = s2 . (dl. dn) ) holds

term @ s1 = term @ s2

for s1, s2 being State of SCM st ( for dn being Element of NAT st dn <= max_Data-Loc_in term holds

s1 . (dl. dn) = s2 . (dl. dn) ) holds

term @ s1 = term @ s2

proof end;

defpred S

for aux, n being Element of NAT st Shift ((SCM-Compile ($1,aux)),n) c= F holds

for s being b

ex i being Element of NAT ex u being State of SCM st

( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ($1,aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = $1 @ s & ( for dn being Element of NAT st dn < aux holds

s . (dl. dn) = u . (dl. dn) ) );

theorem Th12: :: SCM_COMP:12

for F being Instruction-Sequence of SCM

for term being bin-term

for aux, n being Element of NAT st Shift ((SCM-Compile (term,aux)),n) c= F holds

for s being b_{4} -started State of SCM st aux > max_Data-Loc_in term holds

ex i being Element of NAT ex u being State of SCM st

( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile (term,aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = term @ s & ( for dn being Element of NAT st dn < aux holds

s . (dl. dn) = u . (dl. dn) ) )

for term being bin-term

for aux, n being Element of NAT st Shift ((SCM-Compile (term,aux)),n) c= F holds

for s being b

ex i being Element of NAT ex u being State of SCM st

( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile (term,aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = term @ s & ( for dn being Element of NAT st dn < aux holds

s . (dl. dn) = u . (dl. dn) ) )

proof end;

theorem :: SCM_COMP:13

for F being Instruction-Sequence of SCM

for term being bin-term

for aux, n being Element of NAT st Shift (((SCM-Compile (term,aux)) ^ <%(halt SCM)%>),n) c= F holds

for s being b_{4} -started State of SCM st aux > max_Data-Loc_in term holds

( F halts_on s & (Result (F,s)) . (dl. aux) = term @ s & LifeSpan (F,s) = len (SCM-Compile (term,aux)) )

for term being bin-term

for aux, n being Element of NAT st Shift (((SCM-Compile (term,aux)) ^ <%(halt SCM)%>),n) c= F holds

for s being b

( F halts_on s & (Result (F,s)) . (dl. aux) = term @ s & LifeSpan (F,s) = len (SCM-Compile (term,aux)) )

proof end;