:: SCM_COMP semantic presentation

theorem Th1: :: SCM_COMP:1
for b1, b2 being FinSequence of the Instructions of SCM
for b3 being FinSequence of INT
for b4, b5, b6 being Nat
for b7 being State-consisting of b4,b5,b6,b1 ^ b2,b3 holds
( b7 is State-consisting of b4,b5,b6,b1,b3 & b7 is State-consisting of b4,b5 + (len b1),b6,b2,b3 )
proof end;

theorem Th2: :: SCM_COMP:2
for b1, b2 being FinSequence of the Instructions of SCM
for b3, b4, b5, b6, b7 being Nat
for b8 being State-consisting of b3,b4,b5,b1 ^ b2, <*> INT
for b9 being State of SCM st b9 = (Computation b8) . b6 & il. b7 = IC b9 holds
b9 is State-consisting of b7,b4 + (len b1),b5,b2, <*> INT
proof end;

Lemma3: 1 = { b1 where B is Nat : b1 < 1 }
by AXIOMS:30;

Lemma4: 5 = { b1 where B is Nat : b1 < 5 }
by AXIOMS:30;

definition
func SCM-AE -> non empty strict binary with_terminals with_nonterminals with_useful_nonterminals DTConstrStr means :Def1: :: SCM_COMP:def 1
( Terminals a1 = SCM-Data-Loc & NonTerminals a1 = [:1,5:] & ( for b1, b2, b3 being Symbol of a1 holds
( b1 ==> <*b2,b3*> iff b1 in [:1,5:] ) ) );
existence
ex b1 being non empty strict binary with_terminals with_nonterminals with_useful_nonterminals DTConstrStr st
( Terminals b1 = SCM-Data-Loc & NonTerminals b1 = [:1,5:] & ( for b2, b3, b4 being Symbol of b1 holds
( b2 ==> <*b3,b4*> iff b2 in [:1,5:] ) ) )
proof end;
uniqueness
for b1, b2 being non empty strict binary with_terminals with_nonterminals with_useful_nonterminals DTConstrStr st Terminals b1 = SCM-Data-Loc & NonTerminals b1 = [:1,5:] & ( for b3, b4, b5 being Symbol of b1 holds
( b3 ==> <*b4,b5*> iff b3 in [:1,5:] ) ) & Terminals b2 = SCM-Data-Loc & NonTerminals b2 = [:1,5:] & ( for b3, b4, b5 being Symbol of b2 holds
( b3 ==> <*b4,b5*> iff b3 in [:1,5:] ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines SCM-AE SCM_COMP:def 1 :
for b1 being non empty strict binary with_terminals with_nonterminals with_useful_nonterminals DTConstrStr holds
( b1 = SCM-AE iff ( Terminals b1 = SCM-Data-Loc & NonTerminals b1 = [:1,5:] & ( for b2, b3, b4 being Symbol of b1 holds
( b2 ==> <*b3,b4*> iff b2 in [:1,5:] ) ) ) );

definition
mode bin-term is Element of TS SCM-AE ;
end;

Lemma6: NonTerminals SCM-AE = [:1,5:]
by Def1;

definition
let c1 be NonTerminal of SCM-AE ;
let c2, c3 be bin-term;
redefine func -tree as c1 -tree c2,c3 -> bin-term;
coherence
c1 -tree c2,c3 is bin-term
proof end;
end;

definition
let c1 be Terminal of SCM-AE ;
redefine func root-tree as root-tree c1 -> bin-term;
coherence
root-tree c1 is bin-term by DTCONSTR:def 4;
end;

definition
let c1 be Terminal of SCM-AE ;
func @ c1 -> Data-Location equals :: SCM_COMP:def 2
a1;
coherence
c1 is Data-Location
proof end;
end;

:: deftheorem Def2 defines @ SCM_COMP:def 2 :
for b1 being Terminal of SCM-AE holds @ b1 = b1;

theorem Th3: :: SCM_COMP:3
for b1 being NonTerminal of SCM-AE holds
( b1 = [0,0] or b1 = [0,1] or b1 = [0,2] or b1 = [0,3] or b1 = [0,4] )
proof end;

theorem Th4: :: SCM_COMP:4
( [0,0] is NonTerminal of SCM-AE & [0,1] is NonTerminal of SCM-AE & [0,2] is NonTerminal of SCM-AE & [0,3] is NonTerminal of SCM-AE & [0,4] is NonTerminal of SCM-AE )
proof end;

then reconsider c1 = [0,0], c2 = [0,1], c3 = [0,2], c4 = [0,3], c5 = [0,4] as NonTerminal of SCM-AE ;

definition
let c6, c7 be bin-term;
func c1 + c2 -> bin-term equals :: SCM_COMP:def 3
[0,0] -tree a1,a2;
coherence
[0,0] -tree c6,c7 is bin-term
proof end;
func c1 - c2 -> bin-term equals :: SCM_COMP:def 4
[0,1] -tree a1,a2;
coherence
[0,1] -tree c6,c7 is bin-term
proof end;
func c1 * c2 -> bin-term equals :: SCM_COMP:def 5
[0,2] -tree a1,a2;
coherence
[0,2] -tree c6,c7 is bin-term
proof end;
func c1 div c2 -> bin-term equals :: SCM_COMP:def 6
[0,3] -tree a1,a2;
coherence
[0,3] -tree c6,c7 is bin-term
proof end;
func c1 mod c2 -> bin-term equals :: SCM_COMP:def 7
[0,4] -tree a1,a2;
coherence
[0,4] -tree c6,c7 is bin-term
proof end;
end;

:: deftheorem Def3 defines + SCM_COMP:def 3 :
for b1, b2 being bin-term holds b1 + b2 = [0,0] -tree b1,b2;

:: deftheorem Def4 defines - SCM_COMP:def 4 :
for b1, b2 being bin-term holds b1 - b2 = [0,1] -tree b1,b2;

:: deftheorem Def5 defines * SCM_COMP:def 5 :
for b1, b2 being bin-term holds b1 * b2 = [0,2] -tree b1,b2;

:: deftheorem Def6 defines div SCM_COMP:def 6 :
for b1, b2 being bin-term holds b1 div b2 = [0,3] -tree b1,b2;

:: deftheorem Def7 defines mod SCM_COMP:def 7 :
for b1, b2 being bin-term holds b1 mod b2 = [0,4] -tree b1,b2;

theorem Th5: :: SCM_COMP:5
for b1 being bin-term holds
( ex b2 being Terminal of SCM-AE st b1 = root-tree b2 or ex b2, b3 being bin-term st
( b1 = b2 + b3 or b1 = b2 - b3 or b1 = b2 * b3 or b1 = b2 div b3 or b1 = b2 mod b3 ) )
proof end;

definition
let c6 be NonTerminal of SCM-AE ;
let c7, c8 be Integer;
func c1 -Meaning_on c2,c3 -> Integer equals :Def8: :: SCM_COMP:def 8
a2 + a3 if a1 = [0,0]
a2 - a3 if a1 = [0,1]
a2 * a3 if a1 = [0,2]
a2 div a3 if a1 = [0,3]
a2 mod a3 if a1 = [0,4]
;
coherence
( ( c6 = [0,0] implies c7 + c8 is Integer ) & ( c6 = [0,1] implies c7 - c8 is Integer ) & ( c6 = [0,2] implies c7 * c8 is Integer ) & ( c6 = [0,3] implies c7 div c8 is Integer ) & ( c6 = [0,4] implies c7 mod c8 is Integer ) ) ;
consistency
for b1 being Integer holds
( ( c6 = [0,0] & c6 = [0,1] implies ( b1 = c7 + c8 iff b1 = c7 - c8 ) ) & ( c6 = [0,0] & c6 = [0,2] implies ( b1 = c7 + c8 iff b1 = c7 * c8 ) ) & ( c6 = [0,0] & c6 = [0,3] implies ( b1 = c7 + c8 iff b1 = c7 div c8 ) ) & ( c6 = [0,0] & c6 = [0,4] implies ( b1 = c7 + c8 iff b1 = c7 mod c8 ) ) & ( c6 = [0,1] & c6 = [0,2] implies ( b1 = c7 - c8 iff b1 = c7 * c8 ) ) & ( c6 = [0,1] & c6 = [0,3] implies ( b1 = c7 - c8 iff b1 = c7 div c8 ) ) & ( c6 = [0,1] & c6 = [0,4] implies ( b1 = c7 - c8 iff b1 = c7 mod c8 ) ) & ( c6 = [0,2] & c6 = [0,3] implies ( b1 = c7 * c8 iff b1 = c7 div c8 ) ) & ( c6 = [0,2] & c6 = [0,4] implies ( b1 = c7 * c8 iff b1 = c7 mod c8 ) ) & ( c6 = [0,3] & c6 = [0,4] implies ( b1 = c7 div c8 iff b1 = c7 mod c8 ) ) )
proof end;
end;

:: deftheorem Def8 defines -Meaning_on SCM_COMP:def 8 :
for b1 being NonTerminal of SCM-AE
for b2, b3 being Integer holds
( ( b1 = [0,0] implies b1 -Meaning_on b2,b3 = b2 + b3 ) & ( b1 = [0,1] implies b1 -Meaning_on b2,b3 = b2 - b3 ) & ( b1 = [0,2] implies b1 -Meaning_on b2,b3 = b2 * b3 ) & ( b1 = [0,3] implies b1 -Meaning_on b2,b3 = b2 div b3 ) & ( b1 = [0,4] implies b1 -Meaning_on b2,b3 = b2 mod b3 ) );

definition
let c6 be State of SCM ;
let c7 be Terminal of SCM-AE ;
redefine func . as c1 . c2 -> Integer;
coherence
c6 . c7 is Integer
proof end;
end;

definition
let c6 be non empty set ;
let c7 be Function of INT ,c6;
let c8 be Integer;
redefine func . as c2 . c3 -> Element of a1;
coherence
c7 . c8 is Element of c6
proof end;
end;

set c6 = id INT ;

definition
let c7 be State of SCM ;
let c8 be bin-term;
deffunc H1( NonTerminal of SCM-AE , set , set , Integer, Integer) -> Element of INT = (id INT ) . (a1 -Meaning_on a4,a5);
deffunc H2( Terminal of SCM-AE ) -> Element of INT = (id INT ) . (c7 . a1);
func c2 @ c1 -> Integer means :Def9: :: SCM_COMP:def 9
ex b1 being Function of TS SCM-AE , INT st
( a3 = b1 . a2 & ( for b2 being Terminal of SCM-AE holds b1 . (root-tree b2) = a1 . b2 ) & ( for b2 being NonTerminal of SCM-AE
for b3, b4 being bin-term
for b5, b6 being Symbol of SCM-AE st b5 = root-label b3 & b6 = root-label b4 & b2 ==> <*b5,b6*> holds
for b7, b8 being Element of INT st b7 = b1 . b3 & b8 = b1 . b4 holds
b1 . (b2 -tree b3,b4) = b2 -Meaning_on b7,b8 ) );
existence
ex b1 being Integerex b2 being Function of TS SCM-AE , INT st
( b1 = b2 . c8 & ( for b3 being Terminal of SCM-AE holds b2 . (root-tree b3) = c7 . b3 ) & ( for b3 being NonTerminal of SCM-AE
for b4, b5 being bin-term
for b6, b7 being Symbol of SCM-AE st b6 = root-label b4 & b7 = root-label b5 & b3 ==> <*b6,b7*> holds
for b8, b9 being Element of INT st b8 = b2 . b4 & b9 = b2 . b5 holds
b2 . (b3 -tree b4,b5) = b3 -Meaning_on b8,b9 ) )
proof end;
uniqueness
for b1, b2 being Integer st ex b3 being Function of TS SCM-AE , INT st
( b1 = b3 . c8 & ( for b4 being Terminal of SCM-AE holds b3 . (root-tree b4) = c7 . b4 ) & ( for b4 being NonTerminal of SCM-AE
for b5, b6 being bin-term
for b7, b8 being Symbol of SCM-AE st b7 = root-label b5 & b8 = root-label b6 & b4 ==> <*b7,b8*> holds
for b9, b10 being Element of INT st b9 = b3 . b5 & b10 = b3 . b6 holds
b3 . (b4 -tree b5,b6) = b4 -Meaning_on b9,b10 ) ) & ex b3 being Function of TS SCM-AE , INT st
( b2 = b3 . c8 & ( for b4 being Terminal of SCM-AE holds b3 . (root-tree b4) = c7 . b4 ) & ( for b4 being NonTerminal of SCM-AE
for b5, b6 being bin-term
for b7, b8 being Symbol of SCM-AE st b7 = root-label b5 & b8 = root-label b6 & b4 ==> <*b7,b8*> holds
for b9, b10 being Element of INT st b9 = b3 . b5 & b10 = b3 . b6 holds
b3 . (b4 -tree b5,b6) = b4 -Meaning_on b9,b10 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines @ SCM_COMP:def 9 :
for b1 being State of SCM
for b2 being bin-term
for b3 being Integer holds
( b3 = b2 @ b1 iff ex b4 being Function of TS SCM-AE , INT st
( b3 = b4 . b2 & ( for b5 being Terminal of SCM-AE holds b4 . (root-tree b5) = b1 . b5 ) & ( for b5 being NonTerminal of SCM-AE
for b6, b7 being bin-term
for b8, b9 being Symbol of SCM-AE st b8 = root-label b6 & b9 = root-label b7 & b5 ==> <*b8,b9*> holds
for b10, b11 being Element of INT st b10 = b4 . b6 & b11 = b4 . b7 holds
b4 . (b5 -tree b6,b7) = b5 -Meaning_on b10,b11 ) ) );

theorem Th6: :: SCM_COMP:6
for b1 being State of SCM
for b2 being Terminal of SCM-AE holds (root-tree b2) @ b1 = b1 . b2
proof end;

theorem Th7: :: SCM_COMP:7
for b1 being State of SCM
for b2 being NonTerminal of SCM-AE
for b3, b4 being bin-term holds (b2 -tree b3,b4) @ b1 = b2 -Meaning_on (b3 @ b1),(b4 @ b1)
proof end;

theorem Th8: :: SCM_COMP:8
for b1 being State of SCM
for b2, b3 being bin-term holds
( (b2 + b3) @ b1 = (b2 @ b1) + (b3 @ b1) & (b2 - b3) @ b1 = (b2 @ b1) - (b3 @ b1) & (b2 * b3) @ b1 = (b2 @ b1) * (b3 @ b1) & (b2 div b3) @ b1 = (b2 @ b1) div (b3 @ b1) & (b2 mod b3) @ b1 = (b2 @ b1) mod (b3 @ b1) )
proof end;

definition
let c7 be NonTerminal of SCM-AE ;
let c8 be Nat;
func Selfwork c1,c2 -> Element of the Instructions of SCM * equals :Def10: :: SCM_COMP:def 10
<*(AddTo (dl. a2),(dl. (a2 + 1)))*> if a1 = [0,0]
<*(SubFrom (dl. a2),(dl. (a2 + 1)))*> if a1 = [0,1]
<*(MultBy (dl. a2),(dl. (a2 + 1)))*> if a1 = [0,2]
<*(Divide (dl. a2),(dl. (a2 + 1)))*> if a1 = [0,3]
<*(Divide (dl. a2),(dl. (a2 + 1))),((dl. a2) := (dl. (a2 + 1)))*> if a1 = [0,4]
;
coherence
( ( c7 = [0,0] implies <*(AddTo (dl. c8),(dl. (c8 + 1)))*> is Element of the Instructions of SCM * ) & ( c7 = [0,1] implies <*(SubFrom (dl. c8),(dl. (c8 + 1)))*> is Element of the Instructions of SCM * ) & ( c7 = [0,2] implies <*(MultBy (dl. c8),(dl. (c8 + 1)))*> is Element of the Instructions of SCM * ) & ( c7 = [0,3] implies <*(Divide (dl. c8),(dl. (c8 + 1)))*> is Element of the Instructions of SCM * ) & ( c7 = [0,4] implies <*(Divide (dl. c8),(dl. (c8 + 1))),((dl. c8) := (dl. (c8 + 1)))*> is Element of the Instructions of SCM * ) ) ;
consistency
for b1 being Element of the Instructions of SCM * holds
( ( c7 = [0,0] & c7 = [0,1] implies ( b1 = <*(AddTo (dl. c8),(dl. (c8 + 1)))*> iff b1 = <*(SubFrom (dl. c8),(dl. (c8 + 1)))*> ) ) & ( c7 = [0,0] & c7 = [0,2] implies ( b1 = <*(AddTo (dl. c8),(dl. (c8 + 1)))*> iff b1 = <*(MultBy (dl. c8),(dl. (c8 + 1)))*> ) ) & ( c7 = [0,0] & c7 = [0,3] implies ( b1 = <*(AddTo (dl. c8),(dl. (c8 + 1)))*> iff b1 = <*(Divide (dl. c8),(dl. (c8 + 1)))*> ) ) & ( c7 = [0,0] & c7 = [0,4] implies ( b1 = <*(AddTo (dl. c8),(dl. (c8 + 1)))*> iff b1 = <*(Divide (dl. c8),(dl. (c8 + 1))),((dl. c8) := (dl. (c8 + 1)))*> ) ) & ( c7 = [0,1] & c7 = [0,2] implies ( b1 = <*(SubFrom (dl. c8),(dl. (c8 + 1)))*> iff b1 = <*(MultBy (dl. c8),(dl. (c8 + 1)))*> ) ) & ( c7 = [0,1] & c7 = [0,3] implies ( b1 = <*(SubFrom (dl. c8),(dl. (c8 + 1)))*> iff b1 = <*(Divide (dl. c8),(dl. (c8 + 1)))*> ) ) & ( c7 = [0,1] & c7 = [0,4] implies ( b1 = <*(SubFrom (dl. c8),(dl. (c8 + 1)))*> iff b1 = <*(Divide (dl. c8),(dl. (c8 + 1))),((dl. c8) := (dl. (c8 + 1)))*> ) ) & ( c7 = [0,2] & c7 = [0,3] implies ( b1 = <*(MultBy (dl. c8),(dl. (c8 + 1)))*> iff b1 = <*(Divide (dl. c8),(dl. (c8 + 1)))*> ) ) & ( c7 = [0,2] & c7 = [0,4] implies ( b1 = <*(MultBy (dl. c8),(dl. (c8 + 1)))*> iff b1 = <*(Divide (dl. c8),(dl. (c8 + 1))),((dl. c8) := (dl. (c8 + 1)))*> ) ) & ( c7 = [0,3] & c7 = [0,4] implies ( b1 = <*(Divide (dl. c8),(dl. (c8 + 1)))*> iff b1 = <*(Divide (dl. c8),(dl. (c8 + 1))),((dl. c8) := (dl. (c8 + 1)))*> ) ) )
proof end;
end;

:: deftheorem Def10 defines Selfwork SCM_COMP:def 10 :
for b1 being NonTerminal of SCM-AE
for b2 being Nat holds
( ( b1 = [0,0] implies Selfwork b1,b2 = <*(AddTo (dl. b2),(dl. (b2 + 1)))*> ) & ( b1 = [0,1] implies Selfwork b1,b2 = <*(SubFrom (dl. b2),(dl. (b2 + 1)))*> ) & ( b1 = [0,2] implies Selfwork b1,b2 = <*(MultBy (dl. b2),(dl. (b2 + 1)))*> ) & ( b1 = [0,3] implies Selfwork b1,b2 = <*(Divide (dl. b2),(dl. (b2 + 1)))*> ) & ( b1 = [0,4] implies Selfwork b1,b2 = <*(Divide (dl. b2),(dl. (b2 + 1))),((dl. b2) := (dl. (b2 + 1)))*> ) );

definition
let c7 be bin-term;
let c8 be Nat;
deffunc H1( Terminal of SCM-AE , Nat) -> Element of the Instructions of SCM * = <*((dl. a2) := (@ a1))*>;
deffunc H2( NonTerminal of SCM-AE , Function of NAT ,the Instructions of SCM * , Function of NAT ,the Instructions of SCM * , Nat) -> Element of the Instructions of SCM * = ((a2 . a4) ^ (a3 . (a4 + 1))) ^ (Selfwork a1,a4);
func SCM-Compile c1,c2 -> FinSequence of the Instructions of SCM means :Def11: :: SCM_COMP:def 11
ex b1 being Function of TS SCM-AE , Funcs NAT ,(the Instructions of SCM * ) st
( a3 = (b1 . a1) . a2 & ( for b2 being Terminal of SCM-AE ex b3 being Function of NAT ,the Instructions of SCM * st
( b3 = b1 . (root-tree b2) & ( for b4 being Nat holds b3 . b4 = <*((dl. b4) := (@ b2))*> ) ) ) & ( for b2 being NonTerminal of SCM-AE
for b3, b4 being bin-term
for b5, b6 being Symbol of SCM-AE st b5 = root-label b3 & b6 = root-label b4 & b2 ==> <*b5,b6*> holds
ex b7, b8, b9 being Function of NAT ,the Instructions of SCM * st
( b7 = b1 . (b2 -tree b3,b4) & b8 = b1 . b3 & b9 = b1 . b4 & ( for b10 being Nat holds b7 . b10 = ((b8 . b10) ^ (b9 . (b10 + 1))) ^ (Selfwork b2,b10) ) ) ) );
existence
ex b1 being FinSequence of the Instructions of SCM ex b2 being Function of TS SCM-AE , Funcs NAT ,(the Instructions of SCM * ) st
( b1 = (b2 . c7) . c8 & ( for b3 being Terminal of SCM-AE ex b4 being Function of NAT ,the Instructions of SCM * st
( b4 = b2 . (root-tree b3) & ( for b5 being Nat holds b4 . b5 = <*((dl. b5) := (@ b3))*> ) ) ) & ( for b3 being NonTerminal of SCM-AE
for b4, b5 being bin-term
for b6, b7 being Symbol of SCM-AE st b6 = root-label b4 & b7 = root-label b5 & b3 ==> <*b6,b7*> holds
ex b8, b9, b10 being Function of NAT ,the Instructions of SCM * st
( b8 = b2 . (b3 -tree b4,b5) & b9 = b2 . b4 & b10 = b2 . b5 & ( for b11 being Nat holds b8 . b11 = ((b9 . b11) ^ (b10 . (b11 + 1))) ^ (Selfwork b3,b11) ) ) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the Instructions of SCM st ex b3 being Function of TS SCM-AE , Funcs NAT ,(the Instructions of SCM * ) st
( b1 = (b3 . c7) . c8 & ( for b4 being Terminal of SCM-AE ex b5 being Function of NAT ,the Instructions of SCM * st
( b5 = b3 . (root-tree b4) & ( for b6 being Nat holds b5 . b6 = <*((dl. b6) := (@ b4))*> ) ) ) & ( for b4 being NonTerminal of SCM-AE
for b5, b6 being bin-term
for b7, b8 being Symbol of SCM-AE st b7 = root-label b5 & b8 = root-label b6 & b4 ==> <*b7,b8*> holds
ex b9, b10, b11 being Function of NAT ,the Instructions of SCM * st
( b9 = b3 . (b4 -tree b5,b6) & b10 = b3 . b5 & b11 = b3 . b6 & ( for b12 being Nat holds b9 . b12 = ((b10 . b12) ^ (b11 . (b12 + 1))) ^ (Selfwork b4,b12) ) ) ) ) & ex b3 being Function of TS SCM-AE , Funcs NAT ,(the Instructions of SCM * ) st
( b2 = (b3 . c7) . c8 & ( for b4 being Terminal of SCM-AE ex b5 being Function of NAT ,the Instructions of SCM * st
( b5 = b3 . (root-tree b4) & ( for b6 being Nat holds b5 . b6 = <*((dl. b6) := (@ b4))*> ) ) ) & ( for b4 being NonTerminal of SCM-AE
for b5, b6 being bin-term
for b7, b8 being Symbol of SCM-AE st b7 = root-label b5 & b8 = root-label b6 & b4 ==> <*b7,b8*> holds
ex b9, b10, b11 being Function of NAT ,the Instructions of SCM * st
( b9 = b3 . (b4 -tree b5,b6) & b10 = b3 . b5 & b11 = b3 . b6 & ( for b12 being Nat holds b9 . b12 = ((b10 . b12) ^ (b11 . (b12 + 1))) ^ (Selfwork b4,b12) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines SCM-Compile SCM_COMP:def 11 :
for b1 being bin-term
for b2 being Nat
for b3 being FinSequence of the Instructions of SCM holds
( b3 = SCM-Compile b1,b2 iff ex b4 being Function of TS SCM-AE , Funcs NAT ,(the Instructions of SCM * ) st
( b3 = (b4 . b1) . b2 & ( for b5 being Terminal of SCM-AE ex b6 being Function of NAT ,the Instructions of SCM * st
( b6 = b4 . (root-tree b5) & ( for b7 being Nat holds b6 . b7 = <*((dl. b7) := (@ b5))*> ) ) ) & ( for b5 being NonTerminal of SCM-AE
for b6, b7 being bin-term
for b8, b9 being Symbol of SCM-AE st b8 = root-label b6 & b9 = root-label b7 & b5 ==> <*b8,b9*> holds
ex b10, b11, b12 being Function of NAT ,the Instructions of SCM * st
( b10 = b4 . (b5 -tree b6,b7) & b11 = b4 . b6 & b12 = b4 . b7 & ( for b13 being Nat holds b10 . b13 = ((b11 . b13) ^ (b12 . (b13 + 1))) ^ (Selfwork b5,b13) ) ) ) ) );

consider c7 being bin-term, c8 being Nat;

consider c9 being Function of TS SCM-AE , Funcs NAT ,(the Instructions of SCM * ) such that
SCM-Compile c7,c8 = (c9 . c7) . c8 and
Lemma14: ( ( for b1 being Terminal of SCM-AE ex b2 being Function of NAT ,the Instructions of SCM * st
( b2 = c9 . (root-tree b1) & ( for b3 being Nat holds b2 . b3 = <*((dl. b3) := (@ b1))*> ) ) ) & ( for b1 being NonTerminal of SCM-AE
for b2, b3 being bin-term
for b4, b5 being Symbol of SCM-AE st b4 = root-label b2 & b5 = root-label b3 & b1 ==> <*b4,b5*> holds
ex b6, b7, b8 being Function of NAT ,the Instructions of SCM * st
( b6 = c9 . (b1 -tree b2,b3) & b7 = c9 . b2 & b8 = c9 . b3 & ( for b9 being Nat holds b6 . b9 = ((b7 . b9) ^ (b8 . (b9 + 1))) ^ (Selfwork b1,b9) ) ) ) ) by Def11;

theorem Th9: :: SCM_COMP:9
for b1 being Terminal of SCM-AE
for b2 being Nat holds SCM-Compile (root-tree b1),b2 = <*((dl. b2) := (@ b1))*>
proof end;

theorem Th10: :: SCM_COMP:10
for b1 being NonTerminal of SCM-AE
for b2, b3 being bin-term
for b4 being Nat
for b5, b6 being Symbol of SCM-AE st b5 = root-label b2 & b6 = root-label b3 & b1 ==> <*b5,b6*> holds
SCM-Compile (b1 -tree b2,b3),b4 = ((SCM-Compile b2,b4) ^ (SCM-Compile b3,(b4 + 1))) ^ (Selfwork b1,b4)
proof end;

definition
let c10 be Terminal of SCM-AE ;
func d". c1 -> Nat means :Def12: :: SCM_COMP:def 12
 dl. a2 = a1;
existence
ex b1 being Nat st dl. b1 = c10
proof end;
uniqueness
for b1, b2 being Nat st dl. b1 = c10 & dl. b2 = c10 holds
b1 = b2 by AMI_3:52;
end;

:: deftheorem Def12 defines d". SCM_COMP:def 12 :
for b1 being Terminal of SCM-AE
for b2 being Nat holds
( b2 = d". b1 iff dl. b2 = b1 );

definition
let c10 be bin-term;
deffunc H1( NonTerminal of SCM-AE , set , set , Nat, Nat) -> Element of NAT = max a4,a5;
deffunc H2( Terminal of SCM-AE ) -> Nat = d". a1;
func max_Data-Loc_in c1 -> Nat means :Def13: :: SCM_COMP:def 13
ex b1 being Function of TS SCM-AE , NAT st
( a2 = b1 . a1 & ( for b2 being Terminal of SCM-AE holds b1 . (root-tree b2) = d". b2 ) & ( for b2 being NonTerminal of SCM-AE
for b3, b4 being bin-term
for b5, b6 being Symbol of SCM-AE st b5 = root-label b3 & b6 = root-label b4 & b2 ==> <*b5,b6*> holds
for b7, b8 being Nat st b7 = b1 . b3 & b8 = b1 . b4 holds
b1 . (b2 -tree b3,b4) = max b7,b8 ) );
existence
ex b1 being Natex b2 being Function of TS SCM-AE , NAT st
( b1 = b2 . c10 & ( for b3 being Terminal of SCM-AE holds b2 . (root-tree b3) = d". b3 ) & ( for b3 being NonTerminal of SCM-AE
for b4, b5 being bin-term
for b6, b7 being Symbol of SCM-AE st b6 = root-label b4 & b7 = root-label b5 & b3 ==> <*b6,b7*> holds
for b8, b9 being Nat st b8 = b2 . b4 & b9 = b2 . b5 holds
b2 . (b3 -tree b4,b5) = max b8,b9 ) )
proof end;
uniqueness
for b1, b2 being Nat st ex b3 being Function of TS SCM-AE , NAT st
( b1 = b3 . c10 & ( for b4 being Terminal of SCM-AE holds b3 . (root-tree b4) = d". b4 ) & ( for b4 being NonTerminal of SCM-AE
for b5, b6 being bin-term
for b7, b8 being Symbol of SCM-AE st b7 = root-label b5 & b8 = root-label b6 & b4 ==> <*b7,b8*> holds
for b9, b10 being Nat st b9 = b3 . b5 & b10 = b3 . b6 holds
b3 . (b4 -tree b5,b6) = max b9,b10 ) ) & ex b3 being Function of TS SCM-AE , NAT st
( b2 = b3 . c10 & ( for b4 being Terminal of SCM-AE holds b3 . (root-tree b4) = d". b4 ) & ( for b4 being NonTerminal of SCM-AE
for b5, b6 being bin-term
for b7, b8 being Symbol of SCM-AE st b7 = root-label b5 & b8 = root-label b6 & b4 ==> <*b7,b8*> holds
for b9, b10 being Nat st b9 = b3 . b5 & b10 = b3 . b6 holds
b3 . (b4 -tree b5,b6) = max b9,b10 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines max_Data-Loc_in SCM_COMP:def 13 :
for b1 being bin-term
for b2 being Nat holds
( b2 = max_Data-Loc_in b1 iff ex b3 being Function of TS SCM-AE , NAT st
( b2 = b3 . b1 & ( for b4 being Terminal of SCM-AE holds b3 . (root-tree b4) = d". b4 ) & ( for b4 being NonTerminal of SCM-AE
for b5, b6 being bin-term
for b7, b8 being Symbol of SCM-AE st b7 = root-label b5 & b8 = root-label b6 & b4 ==> <*b7,b8*> holds
for b9, b10 being Nat st b9 = b3 . b5 & b10 = b3 . b6 holds
b3 . (b4 -tree b5,b6) = max b9,b10 ) ) );

consider c10 being bin-term;

consider c11 being Function of TS SCM-AE , NAT such that
max_Data-Loc_in c10 = c11 . c10 and
Lemma19: ( ( for b1 being Terminal of SCM-AE holds c11 . (root-tree b1) = d". b1 ) & ( for b1 being NonTerminal of SCM-AE
for b2, b3 being bin-term
for b4, b5 being Symbol of SCM-AE st b4 = root-label b2 & b5 = root-label b3 & b1 ==> <*b4,b5*> holds
for b6, b7 being Nat st b6 = c11 . b2 & b7 = c11 . b3 holds
c11 . (b1 -tree b2,b3) = max b6,b7 ) ) by Def13;

theorem Th11: :: SCM_COMP:11
for b1 being Terminal of SCM-AE holds max_Data-Loc_in (root-tree b1) = d". b1
proof end;

Lemma21: NonTerminals SCM-AE = [:1,5:]
by Def1;

theorem Th12: :: SCM_COMP:12
for b1 being NonTerminal of SCM-AE
for b2, b3 being bin-term holds max_Data-Loc_in (b1 -tree b2,b3) = max (max_Data-Loc_in b2),(max_Data-Loc_in b3)
proof end;

defpred S1[ bin-term] means for b1, b2 being State of SCM st ( for b3 being Nat st b3 <= max_Data-Loc_in a1 holds
b1 . (dl. b3) = b2 . (dl. b3) ) holds
a1 @ b1 = a1 @ b2;

E23: now
let c12 be Terminal of SCM-AE ;
thus S1[ root-tree c12]
proof
let c13, c14 be State of SCM ;
assume E24: for b1 being Nat st b1 <= max_Data-Loc_in (root-tree c12) holds
c13 . (dl. b1) = c14 . (dl. b1) ;
d". c12 <= max_Data-Loc_in (root-tree c12) by Th11;
then E25: ( c13 . (dl. (d". c12)) = c14 . (dl. (d". c12)) & c13 . c12 = c13 . (dl. (d". c12)) & c14 . c12 = c14 . (dl. (d". c12)) ) by E24, Def12;
(root-tree c12) @ c13 = c13 . c12 by Th6;
hence (root-tree c12) @ c13 = (root-tree c12) @ c14 by E25, Th6;
end;
end;

E24: now
let c12 be NonTerminal of SCM-AE ;
let c13, c14 be Element of TS SCM-AE ;
assume E25: ( c12 ==> <*(root-label c13),(root-label c14)*> & S1[c13] & S1[c14] ) ;
thus S1[c12 -tree c13,c14]
proof
let c15, c16 be State of SCM ;
assume E26: for b1 being Nat st b1 <= max_Data-Loc_in (c12 -tree c13,c14) holds
c15 . (dl. b1) = c16 . (dl. b1) ;
now
let c17 be Nat;
assume E27: c17 <= max_Data-Loc_in c13 ;
set c18 = max_Data-Loc_in c13;
set c19 = max_Data-Loc_in c14;
max_Data-Loc_in c13 <= max (max_Data-Loc_in c13),(max_Data-Loc_in c14) by SQUARE_1:46;
then c17 <= max (max_Data-Loc_in c13),(max_Data-Loc_in c14) by E27, XREAL_1:2;
then c17 <= max_Data-Loc_in (c12 -tree c13,c14) by Th12;
hence c15 . (dl. c17) = c16 . (dl. c17) by E26;
end;
then E27: c13 @ c15 = c13 @ c16 by E25;
now
let c17 be Nat;
assume E28: c17 <= max_Data-Loc_in c14 ;
set c18 = max_Data-Loc_in c13;
set c19 = max_Data-Loc_in c14;
max_Data-Loc_in c14 <= max (max_Data-Loc_in c13),(max_Data-Loc_in c14) by SQUARE_1:46;
then c17 <= max (max_Data-Loc_in c13),(max_Data-Loc_in c14) by E28, XREAL_1:2;
then c17 <= max_Data-Loc_in (c12 -tree c13,c14) by Th12;
hence c15 . (dl. c17) = c16 . (dl. c17) by E26;
end;
then E28: c14 @ c15 = c14 @ c16 by E25;
(c12 -tree c13,c14) @ c15 = c12 -Meaning_on (c13 @ c15),(c14 @ c15) by Th7;
hence (c12 -tree c13,c14) @ c15 = (c12 -tree c13,c14) @ c16 by E27, E28, Th7;
end;
end;

theorem Th13: :: SCM_COMP:13
for b1 being bin-term
for b2, b3 being State of SCM st ( for b4 being Nat st b4 <= max_Data-Loc_in b1 holds
b2 . (dl. b4) = b3 . (dl. b4) ) holds
b1 @ b2 = b1 @ b3
proof end;

set c12 = <*> INT ;

defpred S2[ bin-term] means for b1, b2, b3 being Nat
for b4 being State-consisting of b2,b2,b3, SCM-Compile a1,b1, <*> INT st b1 > max_Data-Loc_in a1 holds
ex b5 being Natex b6 being State of SCM st
( b6 = (Computation b4) . (b5 + 1) & b5 + 1 = len (SCM-Compile a1,b1) & IC ((Computation b4) . b5) = il. (b2 + b5) & IC b6 = il. (b2 + (b5 + 1)) & b6 . (dl. b1) = a1 @ b4 & ( for b7 being Nat st b7 < b1 holds
b4 . (dl. b7) = b6 . (dl. b7) ) );

theorem Th14: :: SCM_COMP:14
for b1 being bin-term
for b2, b3, b4 being Nat
for b5 being State-consisting of b3,b3,b4, SCM-Compile b1,b2, <*> INT st b2 > max_Data-Loc_in b1 holds
ex b6 being Natex b7 being State of SCM st
( b7 = (Computation b5) . (b6 + 1) & b6 + 1 = len (SCM-Compile b1,b2) & IC ((Computation b5) . b6) = il. (b3 + b6) & IC b7 = il. (b3 + (b6 + 1)) & b7 . (dl. b2) = b1 @ b5 & ( for b8 being Nat st b8 < b2 holds
b5 . (dl. b8) = b7 . (dl. b8) ) )
proof end;

theorem Th15: :: SCM_COMP:15
for b1 being bin-term
for b2, b3, b4 being Nat
for b5 being State-consisting of b3,b3,b4,(SCM-Compile b1,b2) ^ <*(halt SCM )*>, <*> INT st b2 > max_Data-Loc_in b1 holds
( b5 is halting & (Result b5) . (dl. b2) = b1 @ b5 & Complexity b5 = len (SCM-Compile b1,b2) )
proof end;