let X be set ; for E being non empty set
for v, w being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds w -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ w) -succ_of (X,TS))}
let E be non empty set ; for v, w being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds w -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ w) -succ_of (X,TS))}
let v, w be Element of E ^omega ; for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds w -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ w) -succ_of (X,TS))}
let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; w -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ w) -succ_of (X,TS))}
defpred S1[ Nat] means for u being Element of E ^omega st len u <= $1 holds
for v being Element of E ^omega holds u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ u) -succ_of (X,TS))};
A1:
not <%> E in rng (dom the Tran of (_bool TS))
by Th8;
A2:
S1[ 0 ]
proof
let u be
Element of
E ^omega ;
( len u <= 0 implies for v being Element of E ^omega holds u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ u) -succ_of (X,TS))} )
assume
len u <= 0
;
for v being Element of E ^omega holds u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ u) -succ_of (X,TS))}
then A3:
u = <%> E
;
let v be
Element of
E ^omega ;
u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ u) -succ_of (X,TS))}
reconsider vso =
{(v -succ_of (X,TS))} as
Subset of
(_bool TS) by Def1;
u -succ_of (
vso,
(_bool TS))
= vso
by A1, A3, REWRITE3:104;
hence u -succ_of (
{(v -succ_of (X,TS))},
(_bool TS)) =
{((v ^ {}) -succ_of (X,TS))}
.=
{((v ^ {}) -succ_of (X,TS))}
.=
{((v ^ u) -succ_of (X,TS))}
by A3
;
verum
end;
A4:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A5:
S1[
k]
;
S1[k + 1]now for u being Element of E ^omega st len u <= k + 1 holds
for v being Element of E ^omega holds u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ u) -succ_of (X,TS))}let u be
Element of
E ^omega ;
( len u <= k + 1 implies for v being Element of E ^omega holds b2 -succ_of ({(b3 -succ_of (X,TS))},(_bool TS)) = {((b3 ^ b2) -succ_of (X,TS))} )assume A6:
len u <= k + 1
;
for v being Element of E ^omega holds b2 -succ_of ({(b3 -succ_of (X,TS))},(_bool TS)) = {((b3 ^ b2) -succ_of (X,TS))}let v be
Element of
E ^omega ;
b1 -succ_of ({(b2 -succ_of (X,TS))},(_bool TS)) = {((b2 ^ b1) -succ_of (X,TS))}per cases
( k = 0 or k <> 0 )
;
suppose A7:
k = 0
;
b1 -succ_of ({(b2 -succ_of (X,TS))},(_bool TS)) = {((b2 ^ b1) -succ_of (X,TS))}per cases
( len u = 0 or len u = 1 )
by A6, A7, NAT_1:25;
suppose A8:
len u = 1
;
b1 -succ_of ({(b2 -succ_of (X,TS))},(_bool TS)) = {((b2 ^ b1) -succ_of (X,TS))}A9:
now for x being object st x in {((v ^ u) -succ_of (X,TS))} holds
x in u -succ_of ({(v -succ_of (X,TS))},(_bool TS))let x be
object ;
( x in {((v ^ u) -succ_of (X,TS))} implies x in u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) )assume A10:
x in {((v ^ u) -succ_of (X,TS))}
;
x in u -succ_of ({(v -succ_of (X,TS))},(_bool TS))then reconsider P =
x as
Element of
(_bool TS) by Def1;
x = (v ^ u) -succ_of (
X,
TS)
by A10, TARSKI:def 1;
then
x = u -succ_of (
(v -succ_of (X,TS)),
TS)
by Th29;
then A11:
v -succ_of (
X,
TS),
u ==>* x,
_bool TS
by A8, Th13;
(
v -succ_of (
X,
TS) is
Element of
(_bool TS) &
v -succ_of (
X,
TS)
in {(v -succ_of (X,TS))} )
by Def1, TARSKI:def 1;
then
P in u -succ_of (
{(v -succ_of (X,TS))},
(_bool TS))
by A11, REWRITE3:103;
hence
x in u -succ_of (
{(v -succ_of (X,TS))},
(_bool TS))
;
verum end; now for x being object st x in u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) holds
x in {((v ^ u) -succ_of (X,TS))}let x be
object ;
( x in u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) implies x in {((v ^ u) -succ_of (X,TS))} )assume A12:
x in u -succ_of (
{(v -succ_of (X,TS))},
(_bool TS))
;
x in {((v ^ u) -succ_of (X,TS))}then reconsider P =
x as
Element of
(_bool TS) ;
consider Q being
Element of
(_bool TS) such that A13:
(
Q in {(v -succ_of (X,TS))} &
Q,
u ==>* P,
_bool TS )
by A12, REWRITE3:103;
(
Q = v -succ_of (
X,
TS) &
P = u -succ_of (
Q,
TS) )
by A8, A13, Th13, TARSKI:def 1;
then
P = (v ^ u) -succ_of (
X,
TS)
by Th29;
hence
x in {((v ^ u) -succ_of (X,TS))}
by TARSKI:def 1;
verum end; hence
u -succ_of (
{(v -succ_of (X,TS))},
(_bool TS))
= {((v ^ u) -succ_of (X,TS))}
by A9, TARSKI:2;
verum end; end; end; suppose A14:
k <> 0
;
b1 -succ_of ({(b2 -succ_of (X,TS))},(_bool TS)) = {((b2 ^ b1) -succ_of (X,TS))}reconsider bTS =
_bool TS as non
empty transition-system over
(Lex E) \/ {(<%> E)} by Th30;
consider v1,
v2 being
Element of
E ^omega such that A15:
len v1 <= k
and A16:
len v2 <= k
and A17:
u = v1 ^ v2
by A6, A14, Th5;
A18:
v1 -succ_of (
{(v -succ_of (X,TS))},
(_bool TS))
= {((v ^ v1) -succ_of (X,TS))}
by A5, A15;
A19:
the
Tran of
bTS = the
Tran of
(_bool TS)
;
then (v1 ^ v2) -succ_of (
{(v -succ_of (X,TS))},
(_bool TS)) =
(v1 ^ v2) -succ_of (
{(v -succ_of (X,TS))},
bTS)
by REWRITE3:105
.=
v2 -succ_of (
(v1 -succ_of ({(v -succ_of (X,TS))},bTS)),
bTS)
by Th29
.=
v2 -succ_of (
(v1 -succ_of ({(v -succ_of (X,TS))},(_bool TS))),
bTS)
by A19, REWRITE3:105
.=
v2 -succ_of (
(v1 -succ_of ({(v -succ_of (X,TS))},(_bool TS))),
(_bool TS))
by A19, REWRITE3:105
.=
{(((v ^ v1) ^ v2) -succ_of (X,TS))}
by A5, A16, A18
.=
{((v ^ (v1 ^ v2)) -succ_of (X,TS))}
by AFINSQ_1:27
;
hence
u -succ_of (
{(v -succ_of (X,TS))},
(_bool TS))
= {((v ^ u) -succ_of (X,TS))}
by A17;
verum end; end; end; hence
S1[
k + 1]
;
verum end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A2, A4);
then
( len w <= len w implies w -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ w) -succ_of (X,TS))} )
;
hence
w -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ w) -succ_of (X,TS))}
; verum