let i be Instruction of SCM+FSA ; :: thesis: for s1, s2 being State of SCM+FSA st s1,s2 equal_outside NAT holds
Exec i,s1, Exec i,s2 equal_outside NAT
let s1, s2 be State of SCM+FSA ; :: thesis: ( s1,s2 equal_outside NAT implies Exec i,s1, Exec i,s2 equal_outside NAT )
assume A1: s1,s2 equal_outside NAT ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT
A2: ( not InsCode i <= 9 + 1 or InsCode i <= 8 + 1 or InsCode i = 10 ) by NAT_1:8;
A3: ( not InsCode i <= 10 + 1 or InsCode i <= 10 or InsCode i = 11 ) by NAT_1:8;
A4: InsCode i <= 11 + 1 by SCMFSA_2:35;

per cases ( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by A4, A3, A2, NAT_1:8, NAT_1:33;

suppose InsCode i = 0 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT

then A5: i = halt SCM+FSA by SCMFSA_2:122;
then Exec i,s1 = s1 by AMI_1:def 8;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A1, A5, AMI_1:def 8; :: thesis: verum

end;

suppose InsCode i = 1 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT

then consider da, db being Int-Location such that
A6: i = da := db by SCMFSA_2:54;

A7: now

let c be Int-Location ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

per cases ( c = da or c <> da ) ;

suppose A8: c = da ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

hence (Exec i,s1) . c = s1 . db by A6, SCMFSA_2:89
.= s2 . db by A1, SCMFSA10:92
.= (Exec i,s2) . c by A6, A8, SCMFSA_2:89 ;
:: thesis: verum

end;

suppose A9: c <> da ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

hence (Exec i,s1) . c = s1 . c by A6, SCMFSA_2:89
.= s2 . c by A1, SCMFSA10:92
.= (Exec i,s2) . c by A6, A9, SCMFSA_2:89 ;
:: thesis: verum

end;

end;

end;

A10: now

let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A6, SCMFSA_2:89
.= s2 . f by A1, SCMFSA10:93
.= (Exec i,s2) . f by A6, SCMFSA_2:89 ; :: thesis: verum

end;

IC (Exec i,s1) = succ (IC s1) by A6, SCMFSA_2:89
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec i,s2) by A6, SCMFSA_2:89 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A7, A10, SCMFSA10:91; :: thesis: verum

end;

suppose InsCode i = 2 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT

then consider da, db being Int-Location such that
A11: i = AddTo da,db by SCMFSA_2:55;

A12: now

let c be Int-Location ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

per cases ( c = da or c <> da ) ;

suppose A13: c = da ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, SCMFSA10:92;
hence (Exec i,s1) . c = (s2 . da) + (s2 . db) by A11, A13, SCMFSA_2:90
.= (Exec i,s2) . c by A11, A13, SCMFSA_2:90 ;
:: thesis: verum

end;

suppose A14: c <> da ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

hence (Exec i,s1) . c = s1 . c by A11, SCMFSA_2:90
.= s2 . c by A1, SCMFSA10:92
.= (Exec i,s2) . c by A11, A14, SCMFSA_2:90 ;
:: thesis: verum

end;

end;

end;

A15: now

let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A11, SCMFSA_2:90
.= s2 . f by A1, SCMFSA10:93
.= (Exec i,s2) . f by A11, SCMFSA_2:90 ; :: thesis: verum

end;

IC (Exec i,s1) = succ (IC s1) by A11, SCMFSA_2:90
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec i,s2) by A11, SCMFSA_2:90 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A12, A15, SCMFSA10:91; :: thesis: verum

end;

suppose InsCode i = 3 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT

then consider da, db being Int-Location such that
A16: i = SubFrom da,db by SCMFSA_2:56;

A17: now

let c be Int-Location ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

per cases ( c = da or c <> da ) ;

suppose A18: c = da ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, SCMFSA10:92;
hence (Exec i,s1) . c = (s2 . da) - (s2 . db) by A16, A18, SCMFSA_2:91
.= (Exec i,s2) . c by A16, A18, SCMFSA_2:91 ;
:: thesis: verum

end;

suppose A19: c <> da ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

hence (Exec i,s1) . c = s1 . c by A16, SCMFSA_2:91
.= s2 . c by A1, SCMFSA10:92
.= (Exec i,s2) . c by A16, A19, SCMFSA_2:91 ;
:: thesis: verum

end;

end;

end;

A20: now

let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A16, SCMFSA_2:91
.= s2 . f by A1, SCMFSA10:93
.= (Exec i,s2) . f by A16, SCMFSA_2:91 ; :: thesis: verum

end;

IC (Exec i,s1) = succ (IC s1) by A16, SCMFSA_2:91
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec i,s2) by A16, SCMFSA_2:91 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A17, A20, SCMFSA10:91; :: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT

then consider da, db being Int-Location such that
A21: i = MultBy da,db by SCMFSA_2:57;

A22: now

let c be Int-Location ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

per cases ( c = da or c <> da ) ;

suppose A23: c = da ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, SCMFSA10:92;
hence (Exec i,s1) . c = (s2 . da) * (s2 . db) by A21, A23, SCMFSA_2:92
.= (Exec i,s2) . c by A21, A23, SCMFSA_2:92 ;
:: thesis: verum

end;

suppose A24: c <> da ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

hence (Exec i,s1) . c = s1 . c by A21, SCMFSA_2:92
.= s2 . c by A1, SCMFSA10:92
.= (Exec i,s2) . c by A21, A24, SCMFSA_2:92 ;
:: thesis: verum

end;

end;

end;

A25: now

let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A21, SCMFSA_2:92
.= s2 . f by A1, SCMFSA10:93
.= (Exec i,s2) . f by A21, SCMFSA_2:92 ; :: thesis: verum

end;

IC (Exec i,s1) = succ (IC s1) by A21, SCMFSA_2:92
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec i,s2) by A21, SCMFSA_2:92 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A22, A25, SCMFSA10:91; :: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT

then consider da, db being Int-Location such that
A26: i = Divide da,db by SCMFSA_2:58;

A27: now

let c be Int-Location ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

per cases ( c = db or ( c = da & c <> db ) or ( c <> da & c <> db ) ) ;

suppose A28: c = db ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, SCMFSA10:92;
hence (Exec i,s1) . c = (s2 . da) mod (s2 . db) by A26, A28, SCMFSA_2:93
.= (Exec i,s2) . c by A26, A28, SCMFSA_2:93 ;
:: thesis: verum

end;

suppose A29: ( c = da & c <> db ) ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, SCMFSA10:92;
hence (Exec i,s1) . c = (s2 . da) div (s2 . db) by A26, A29, SCMFSA_2:93
.= (Exec i,s2) . c by A26, A29, SCMFSA_2:93 ;
:: thesis: verum

end;

suppose A30: ( c <> da & c <> db ) ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

hence (Exec i,s1) . c = s1 . c by A26, SCMFSA_2:93
.= s2 . c by A1, SCMFSA10:92
.= (Exec i,s2) . c by A26, A30, SCMFSA_2:93 ;
:: thesis: verum

end;

end;

end;

A31: now

let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A26, SCMFSA_2:93
.= s2 . f by A1, SCMFSA10:93
.= (Exec i,s2) . f by A26, SCMFSA_2:93 ; :: thesis: verum

end;

IC (Exec i,s1) = succ (IC s1) by A26, SCMFSA_2:93
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec i,s2) by A26, SCMFSA_2:93 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A27, A31, SCMFSA10:91; :: thesis: verum

end;

suppose InsCode i = 6 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT

then consider loc being Element of NAT such that
A32: i = goto loc by SCMFSA_2:59;

A33: now

let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A32, SCMFSA_2:95
.= s2 . f by A1, SCMFSA10:93
.= (Exec i,s2) . f by A32, SCMFSA_2:95 ; :: thesis: verum

end;

A34: now

let c be Int-Location ; :: thesis: (Exec i,s1) . c = (Exec i,s2) . c
thus (Exec i,s1) . c = s1 . c by A32, SCMFSA_2:95
.= s2 . c by A1, SCMFSA10:92
.= (Exec i,s2) . c by A32, SCMFSA_2:95 ; :: thesis: verum

end;

IC (Exec i,s1) = loc by A32, SCMFSA_2:95
.= IC (Exec i,s2) by A32, SCMFSA_2:95 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A34, A33, SCMFSA10:91; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT

then consider loc being Element of NAT , da being Int-Location such that
A35: i = da =0_goto loc by SCMFSA_2:60;

A36: now

per cases ( s1 . da = 0 or s1 . da <> 0 ) ;

suppose A37: s1 . da = 0 ; :: thesis: IC (Exec i,s1) = IC (Exec i,s2)

then A38: s2 . da = 0 by A1, SCMFSA10:92;
thus IC (Exec i,s1) = loc by A35, A37, SCMFSA_2:96
.= IC (Exec i,s2) by A35, A38, SCMFSA_2:96 ; :: thesis: verum

end;

suppose A39: s1 . da <> 0 ; :: thesis: IC (Exec i,s1) = IC (Exec i,s2)

then A40: s2 . da <> 0 by A1, SCMFSA10:92;
thus IC (Exec i,s1) = succ (IC s1) by A35, A39, SCMFSA_2:96
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec i,s2) by A35, A40, SCMFSA_2:96 ; :: thesis: verum

end;

end;

end;

A41: now

let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A35, SCMFSA_2:96
.= s2 . f by A1, SCMFSA10:93
.= (Exec i,s2) . f by A35, SCMFSA_2:96 ; :: thesis: verum

end;

now

let c be Int-Location ; :: thesis: (Exec i,s1) . c = (Exec i,s2) . c
thus (Exec i,s1) . c = s1 . c by A35, SCMFSA_2:96
.= s2 . c by A1, SCMFSA10:92
.= (Exec i,s2) . c by A35, SCMFSA_2:96 ; :: thesis: verum

end;

hence Exec i,s1, Exec i,s2 equal_outside NAT by A41, A36, SCMFSA10:91; :: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT

then consider loc being Element of NAT , da being Int-Location such that
A42: i = da >0_goto loc by SCMFSA_2:61;

A43: now

per cases ( s1 . da > 0 or s1 . da <= 0 ) ;

suppose A44: s1 . da > 0 ; :: thesis: IC (Exec i,s1) = IC (Exec i,s2)

then A45: s2 . da > 0 by A1, SCMFSA10:92;
thus IC (Exec i,s1) = loc by A42, A44, SCMFSA_2:97
.= IC (Exec i,s2) by A42, A45, SCMFSA_2:97 ; :: thesis: verum

end;

suppose A46: s1 . da <= 0 ; :: thesis: IC (Exec i,s1) = IC (Exec i,s2)

then A47: s2 . da <= 0 by A1, SCMFSA10:92;
thus IC (Exec i,s1) = succ (IC s1) by A42, A46, SCMFSA_2:97
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec i,s2) by A42, A47, SCMFSA_2:97 ; :: thesis: verum

end;

end;

end;

A48: now

let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A42, SCMFSA_2:97
.= s2 . f by A1, SCMFSA10:93
.= (Exec i,s2) . f by A42, SCMFSA_2:97 ; :: thesis: verum

end;

now

let c be Int-Location ; :: thesis: (Exec i,s1) . c = (Exec i,s2) . c
thus (Exec i,s1) . c = s1 . c by A42, SCMFSA_2:97
.= s2 . c by A1, SCMFSA10:92
.= (Exec i,s2) . c by A42, SCMFSA_2:97 ; :: thesis: verum

end;

hence Exec i,s1, Exec i,s2 equal_outside NAT by A48, A43, SCMFSA10:91; :: thesis: verum

end;

suppose InsCode i = 9 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT

then consider db, da being Int-Location , f being FinSeq-Location such that
A49: i = da := f,db by SCMFSA_2:62;

A50: now

let c be Int-Location ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

per cases ( c = da or c <> da ) ;

suppose A51: c = da ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then consider n being Element of NAT such that
A52: n = abs (s2 . db) and
A53: (Exec (da := f,db),s2) . c = (s2 . f) /. n by SCMFSA_2:98;
consider m being Element of NAT such that
A54: m = abs (s1 . db) and
A55: (Exec (da := f,db),s1) . c = (s1 . f) /. m by A51, SCMFSA_2:98;
m = n by A1, A54, A52, SCMFSA10:92;
hence (Exec i,s1) . c = (Exec i,s2) . c by A1, A49, A55, A53, SCMFSA10:93; :: thesis: verum

end;

suppose A56: c <> da ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

hence (Exec i,s1) . c = s1 . c by A49, SCMFSA_2:98
.= s2 . c by A1, SCMFSA10:92
.= (Exec i,s2) . c by A49, A56, SCMFSA_2:98 ;
:: thesis: verum

end;

end;

end;

A57: now

let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A49, SCMFSA_2:98
.= s2 . f by A1, SCMFSA10:93
.= (Exec i,s2) . f by A49, SCMFSA_2:98 ; :: thesis: verum

end;

IC (Exec i,s1) = succ (IC s1) by A49, SCMFSA_2:98
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec i,s2) by A49, SCMFSA_2:98 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A50, A57, SCMFSA10:91; :: thesis: verum

end;

suppose InsCode i = 10 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT

then consider db, da being Int-Location , f being FinSeq-Location such that
A58: i = f,db := da by SCMFSA_2:63;

A59: now

let g be FinSeq-Location ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

per cases ( g = f or g <> f ) ;

suppose A60: g = f ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

A61: s1 . da = s2 . da by A1, SCMFSA10:92;
consider n being Element of NAT such that
A62: n = abs (s2 . db) and
A63: (Exec (f,db := da),s2) . f = (s2 . f) +* n,(s2 . da) by SCMFSA_2:99;
consider m being Element of NAT such that
A64: m = abs (s1 . db) and
A65: (Exec (f,db := da),s1) . f = (s1 . f) +* m,(s1 . da) by SCMFSA_2:99;
m = n by A1, A64, A62, SCMFSA10:92;
hence (Exec i,s1) . g = (Exec i,s2) . g by A1, A58, A60, A65, A63, A61, SCMFSA10:93; :: thesis: verum

end;

suppose A66: g <> f ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

hence (Exec i,s1) . g = s1 . g by A58, SCMFSA_2:99
.= s2 . g by A1, SCMFSA10:93
.= (Exec i,s2) . g by A58, A66, SCMFSA_2:99 ;
:: thesis: verum

end;

end;

end;

A67: now

let c be Int-Location ; :: thesis: (Exec i,s1) . c = (Exec i,s2) . c
thus (Exec i,s1) . c = s1 . c by A58, SCMFSA_2:99
.= s2 . c by A1, SCMFSA10:92
.= (Exec i,s2) . c by A58, SCMFSA_2:99 ; :: thesis: verum

end;

IC (Exec i,s1) = succ (IC s1) by A58, SCMFSA_2:99
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec i,s2) by A58, SCMFSA_2:99 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A67, A59, SCMFSA10:91; :: thesis: verum

end;

suppose InsCode i = 11 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT

then consider da being Int-Location , f being FinSeq-Location such that
A68: i = da :=len f by SCMFSA_2:64;

A69: now

let c be Int-Location ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

per cases ( c = da or c <> da ) ;

suppose A70: c = da ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

hence (Exec i,s1) . c = len (s1 . f) by A68, SCMFSA_2:100
.= len (s2 . f) by A1, SCMFSA10:93
.= (Exec i,s2) . c by A68, A70, SCMFSA_2:100 ;
:: thesis: verum

end;

suppose A71: c <> da ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

hence (Exec i,s1) . c = s1 . c by A68, SCMFSA_2:100
.= s2 . c by A1, SCMFSA10:92
.= (Exec i,s2) . c by A68, A71, SCMFSA_2:100 ;
:: thesis: verum

end;

end;

end;

A72: now

let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A68, SCMFSA_2:100
.= s2 . f by A1, SCMFSA10:93
.= (Exec i,s2) . f by A68, SCMFSA_2:100 ; :: thesis: verum

end;

IC (Exec i,s1) = succ (IC s1) by A68, SCMFSA_2:100
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec i,s2) by A68, SCMFSA_2:100 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A69, A72, SCMFSA10:91; :: thesis: verum

end;

suppose InsCode i = 12 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT

then consider da being Int-Location , f being FinSeq-Location such that
A73: i = f :=<0,...,0> da by SCMFSA_2:65;

A74: now

let g be FinSeq-Location ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

per cases ( g = f or g <> f ) ;

suppose A75: g = f ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

( ex m being Element of NAT st
( m = abs (s1 . da) & (Exec (f :=<0,...,0> da),s1) . f = m |-> 0 ) & ex n being Element of NAT st
( n = abs (s2 . da) & (Exec (f :=<0,...,0> da),s2) . f = n |-> 0 ) ) by SCMFSA_2:101;
hence (Exec i,s1) . g = (Exec i,s2) . g by A1, A73, A75, SCMFSA10:92; :: thesis: verum

end;

suppose A76: g <> f ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

hence (Exec i,s1) . g = s1 . g by A73, SCMFSA_2:101
.= s2 . g by A1, SCMFSA10:93
.= (Exec i,s2) . g by A73, A76, SCMFSA_2:101 ;
:: thesis: verum

end;

end;

end;

A77: now

let c be Int-Location ; :: thesis: (Exec i,s1) . c = (Exec i,s2) . c
thus (Exec i,s1) . c = s1 . c by A73, SCMFSA_2:101
.= s2 . c by A1, SCMFSA10:92
.= (Exec i,s2) . c by A73, SCMFSA_2:101 ; :: thesis: verum

end;

IC (Exec i,s1) = succ (IC s1) by A73, SCMFSA_2:101
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec i,s2) by A73, SCMFSA_2:101 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A77, A74, SCMFSA10:91; :: thesis: verum

end;

end;