let v1, v2 be Function of [:NAT,LTLB_WFF:],BOOLEAN; :: thesis: ( ( for n being Element of NAT holds

( v1 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( v1 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds

( v1 . [n,(p => q)] = (v1 . [n,p]) => (v1 . [n,q]) & ( v1 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v1 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v1 . [(n + j),p] = 1 ) ) implies v1 . [n,(p 'U' q)] = 1 ) ) ) ) ) & ( for n being Element of NAT holds

( v2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( v2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds

( v2 . [n,(p => q)] = (v2 . [n,p]) => (v2 . [n,q]) & ( v2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v2 . [(n + j),p] = 1 ) ) implies v2 . [n,(p 'U' q)] = 1 ) ) ) ) ) implies v1 = v2 )

assume A65: for n being Element of NAT holds

( v1 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( v1 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds

( v1 . [n,(p => q)] = (v1 . [n,p]) => (v1 . [n,q]) & ( v1 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v1 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v1 . [(n + j),p] = 1 ) ) implies v1 . [n,(p 'U' q)] = 1 ) ) ) ) ; :: thesis: ( ex n being Element of NAT st

( v2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( v2 . [n,(prop k)] = 1 iff prop k in M . n ) ) implies ex p, q being Element of LTLB_WFF st

( v2 . [n,(p => q)] = (v2 . [n,p]) => (v2 . [n,q]) & ( v2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v2 . [(n + j),p] = 1 ) ) ) implies ( ex i being Element of NAT st

( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v2 . [(n + j),p] = 1 ) ) & not v2 . [n,(p 'U' q)] = 1 ) ) ) or v1 = v2 )

assume A66: for n being Element of NAT holds

( v2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( v2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds

( v2 . [n,(p => q)] = (v2 . [n,p]) => (v2 . [n,q]) & ( v2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v2 . [(n + j),p] = 1 ) ) implies v2 . [n,(p 'U' q)] = 1 ) ) ) ) ; :: thesis: v1 = v2

thus v1 = v2 :: thesis: verum

( v1 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( v1 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds

( v1 . [n,(p => q)] = (v1 . [n,p]) => (v1 . [n,q]) & ( v1 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v1 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v1 . [(n + j),p] = 1 ) ) implies v1 . [n,(p 'U' q)] = 1 ) ) ) ) ) & ( for n being Element of NAT holds

( v2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( v2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds

( v2 . [n,(p => q)] = (v2 . [n,p]) => (v2 . [n,q]) & ( v2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v2 . [(n + j),p] = 1 ) ) implies v2 . [n,(p 'U' q)] = 1 ) ) ) ) ) implies v1 = v2 )

assume A65: for n being Element of NAT holds

( v1 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( v1 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds

( v1 . [n,(p => q)] = (v1 . [n,p]) => (v1 . [n,q]) & ( v1 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v1 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v1 . [(n + j),p] = 1 ) ) implies v1 . [n,(p 'U' q)] = 1 ) ) ) ) ; :: thesis: ( ex n being Element of NAT st

( v2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( v2 . [n,(prop k)] = 1 iff prop k in M . n ) ) implies ex p, q being Element of LTLB_WFF st

( v2 . [n,(p => q)] = (v2 . [n,p]) => (v2 . [n,q]) & ( v2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v2 . [(n + j),p] = 1 ) ) ) implies ( ex i being Element of NAT st

( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v2 . [(n + j),p] = 1 ) ) & not v2 . [n,(p 'U' q)] = 1 ) ) ) or v1 = v2 )

assume A66: for n being Element of NAT holds

( v2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( v2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds

( v2 . [n,(p => q)] = (v2 . [n,p]) => (v2 . [n,q]) & ( v2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v2 . [(n + j),p] = 1 ) ) implies v2 . [n,(p 'U' q)] = 1 ) ) ) ) ; :: thesis: v1 = v2

thus v1 = v2 :: thesis: verum

proof

defpred S_{1}[ Element of LTLB_WFF ] means for n being Element of NAT holds v1 . [n,$1] = v2 . [n,$1];

A67: for n being Element of NAT holds S_{1}[ prop n]
_{1}[p] & S_{1}[q] holds

( S_{1}[p 'U' q] & S_{1}[p => q] )
_{1}[ TFALSUM ]
;

A84: for A being Element of LTLB_WFF holds S_{1}[A]
from HILBERT2:sch 2(A83, A67, A70);

A85: for x being Element of [:NAT,LTLB_WFF:] st x in dom v1 holds

v1 . x = v2 . x

.= dom v2 by FUNCT_2:def 1 ;

hence v1 = v2 by A85, PARTFUN1:5; :: thesis: verum

end;A67: for n being Element of NAT holds S

proof

A70:
for p, q being Element of LTLB_WFF st S
let k be Element of NAT ; :: thesis: S_{1}[ prop k]

_{1}[ prop k]
; :: thesis: verum

end;now :: thesis: for n being Element of NAT holds v1 . [n,(prop k)] = v2 . [n,(prop k)]

hence
Slet n be Element of NAT ; :: thesis: v1 . [b_{1},(prop k)] = v2 . [b_{1},(prop k)]

end;( S

proof

let p, q be Element of LTLB_WFF ; :: thesis: ( S_{1}[p] & S_{1}[q] implies ( S_{1}[p 'U' q] & S_{1}[p => q] ) )

assume that

A71: S_{1}[p]
and

A72: S_{1}[q]
; :: thesis: ( S_{1}[p 'U' q] & S_{1}[p => q] )

thus S_{1}[p 'U' q]
:: thesis: S_{1}[p => q]_{1}[p => q]
:: thesis: verum

end;assume that

A71: S

A72: S

thus S

proof

thus
S
let n be Element of NAT ; :: thesis: v1 . [n,(p 'U' q)] = v2 . [n,(p 'U' q)]

end;per cases
( ex i being Element of NAT st

( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v1 . [(n + j),p] = 1 ) ) or for i being Element of NAT holds

( not 0 < i or not v1 . [(n + i),q] = 1 or ex j being Element of NAT st

( 1 <= j & j < i & not v1 . [(n + j),p] = 1 ) ) ) ;

end;

( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v1 . [(n + j),p] = 1 ) ) or for i being Element of NAT holds

( not 0 < i or not v1 . [(n + i),q] = 1 or ex j being Element of NAT st

( 1 <= j & j < i & not v1 . [(n + j),p] = 1 ) ) ) ;

suppose A73:
ex i being Element of NAT st

( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v1 . [(n + j),p] = 1 ) ) ; :: thesis: v1 . [n,(p 'U' q)] = v2 . [n,(p 'U' q)]

( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

v1 . [(n + j),p] = 1 ) ) ; :: thesis: v1 . [n,(p 'U' q)] = v2 . [n,(p 'U' q)]

then consider i being Element of NAT such that

A74: 0 < i and

A75: v1 . [(n + i),q] = 1 and

A76: for j being Element of NAT st 1 <= j & j < i holds

v1 . [(n + j),p] = 1 ;

A77: v2 . [(n + i),q] = 1 by A72, A75;

.= v2 . [n,(p 'U' q)] by A66, A74, A77, A78 ; :: thesis: verum

end;A74: 0 < i and

A75: v1 . [(n + i),q] = 1 and

A76: for j being Element of NAT st 1 <= j & j < i holds

v1 . [(n + j),p] = 1 ;

A77: v2 . [(n + i),q] = 1 by A72, A75;

A78: now :: thesis: for j being Element of NAT st 1 <= j & j < i holds

v2 . [(n + j),p] = 1

thus v1 . [n,(p 'U' q)] =
1
by A65, A73
v2 . [(n + j),p] = 1

let j be Element of NAT ; :: thesis: ( 1 <= j & j < i implies v2 . [(n + j),p] = 1 )

assume ( 1 <= j & j < i ) ; :: thesis: v2 . [(n + j),p] = 1

then v1 . [(n + j),p] = 1 by A76;

hence v2 . [(n + j),p] = 1 by A71; :: thesis: verum

end;assume ( 1 <= j & j < i ) ; :: thesis: v2 . [(n + j),p] = 1

then v1 . [(n + j),p] = 1 by A76;

hence v2 . [(n + j),p] = 1 by A71; :: thesis: verum

.= v2 . [n,(p 'U' q)] by A66, A74, A77, A78 ; :: thesis: verum

suppose A79:
for i being Element of NAT holds

( not 0 < i or not v1 . [(n + i),q] = 1 or ex j being Element of NAT st

( 1 <= j & j < i & not v1 . [(n + j),p] = 1 ) ) ; :: thesis: v1 . [n,(p 'U' q)] = v2 . [n,(p 'U' q)]

hence v1 . [n,(p 'U' q)] = v2 . [n,(p 'U' q)] by A66, XBOOLEAN:def 3, A80; :: thesis: verum

end;

( not 0 < i or not v1 . [(n + i),q] = 1 or ex j being Element of NAT st

( 1 <= j & j < i & not v1 . [(n + j),p] = 1 ) ) ; :: thesis: v1 . [n,(p 'U' q)] = v2 . [n,(p 'U' q)]

A80: now :: thesis: for i being Element of NAT holds

( not 0 < i or not v2 . [(n + i),q] = 1 or ex j being Element of NAT st

( 1 <= j & j < i & not v2 . [(n + j),p] = 1 ) )

v1 . [n,(p 'U' q)] = 0
by XBOOLEAN:def 3, A65, A79;( not 0 < i or not v2 . [(n + i),q] = 1 or ex j being Element of NAT st

( 1 <= j & j < i & not v2 . [(n + j),p] = 1 ) )

let i be Element of NAT ; :: thesis: ( not 0 < b_{1} or not v2 . [(n + b_{1}),q] = 1 or ex j being Element of NAT st

( 1 <= b_{2} & b_{2} < j & not v2 . [(n + b_{2}),p] = 1 ) )

end;( 1 <= b

per cases
( not 0 < i or not v1 . [(n + i),q] = 1 or ex j being Element of NAT st

( 1 <= j & j < i & not v1 . [(n + j),p] = 1 ) ) by A79;

end;

( 1 <= j & j < i & not v1 . [(n + j),p] = 1 ) ) by A79;

suppose
not 0 < i
; :: thesis: ( not 0 < b_{1} or not v2 . [(n + b_{1}),q] = 1 or ex j being Element of NAT st

( 1 <= b_{2} & b_{2} < j & not v2 . [(n + b_{2}),p] = 1 ) )

( 1 <= b

hence
( not 0 < i or not v2 . [(n + i),q] = 1 or ex j being Element of NAT st

( 1 <= j & j < i & not v2 . [(n + j),p] = 1 ) ) ; :: thesis: verum

end;( 1 <= j & j < i & not v2 . [(n + j),p] = 1 ) ) ; :: thesis: verum

suppose
not v1 . [(n + i),q] = 1
; :: thesis: ( not 0 < b_{1} or not v2 . [(n + b_{1}),q] = 1 or ex j being Element of NAT st

( 1 <= b_{2} & b_{2} < j & not v2 . [(n + b_{2}),p] = 1 ) )

( 1 <= b

hence
( not 0 < i or not v2 . [(n + i),q] = 1 or ex j being Element of NAT st

( 1 <= j & j < i & not v2 . [(n + j),p] = 1 ) ) by A72; :: thesis: verum

end;( 1 <= j & j < i & not v2 . [(n + j),p] = 1 ) ) by A72; :: thesis: verum

suppose
ex j being Element of NAT st

( 1 <= j & j < i & not v1 . [(n + j),p] = 1 ) ; :: thesis: ( not 0 < b_{1} or not v2 . [(n + b_{1}),q] = 1 or ex j being Element of NAT st

( 1 <= b_{2} & b_{2} < j & not v2 . [(n + b_{2}),p] = 1 ) )

( 1 <= j & j < i & not v1 . [(n + j),p] = 1 ) ; :: thesis: ( not 0 < b

( 1 <= b

then consider j being Element of NAT such that

A81: ( 1 <= j & j < i ) and

A82: not v1 . [(n + j),p] = 1 ;

not v2 . [(n + j),p] = 1 by A71, A82;

hence ( not 0 < i or not v2 . [(n + i),q] = 1 or ex j being Element of NAT st

( 1 <= j & j < i & not v2 . [(n + j),p] = 1 ) ) by A81; :: thesis: verum

end;A81: ( 1 <= j & j < i ) and

A82: not v1 . [(n + j),p] = 1 ;

not v2 . [(n + j),p] = 1 by A71, A82;

hence ( not 0 < i or not v2 . [(n + i),q] = 1 or ex j being Element of NAT st

( 1 <= j & j < i & not v2 . [(n + j),p] = 1 ) ) by A81; :: thesis: verum

hence v1 . [n,(p 'U' q)] = v2 . [n,(p 'U' q)] by A66, XBOOLEAN:def 3, A80; :: thesis: verum

now :: thesis: for n being Element of NAT holds v1 . [n,TFALSUM] = v2 . [n,TFALSUM]

then A83:
Slet n be Element of NAT ; :: thesis: v1 . [n,TFALSUM] = v2 . [n,TFALSUM]

thus v1 . [n,TFALSUM] = 0 by A65

.= v2 . [n,TFALSUM] by A66 ; :: thesis: verum

end;thus v1 . [n,TFALSUM] = 0 by A65

.= v2 . [n,TFALSUM] by A66 ; :: thesis: verum

A84: for A being Element of LTLB_WFF holds S

A85: for x being Element of [:NAT,LTLB_WFF:] st x in dom v1 holds

v1 . x = v2 . x

proof

dom v1 =
[:NAT,LTLB_WFF:]
by FUNCT_2:def 1
let x be Element of [:NAT,LTLB_WFF:]; :: thesis: ( x in dom v1 implies v1 . x = v2 . x )

consider y, z being object such that

A86: y in NAT and

A87: z in LTLB_WFF and

A88: x = [y,z] by ZFMISC_1:def 2;

reconsider y1 = y as Element of NAT by A86;

assume x in dom v1 ; :: thesis: v1 . x = v2 . x

thus v1 . x = v2 . x by A84, A86, A87, A88; :: thesis: verum

reconsider z1 = z as Element of LTLB_WFF by A87;

end;consider y, z being object such that

A86: y in NAT and

A87: z in LTLB_WFF and

A88: x = [y,z] by ZFMISC_1:def 2;

reconsider y1 = y as Element of NAT by A86;

assume x in dom v1 ; :: thesis: v1 . x = v2 . x

thus v1 . x = v2 . x by A84, A86, A87, A88; :: thesis: verum

reconsider z1 = z as Element of LTLB_WFF by A87;

.= dom v2 by FUNCT_2:def 1 ;

hence v1 = v2 by A85, PARTFUN1:5; :: thesis: verum