let f, f1 be FinSequence of LTLB_WFF ; :: thesis: for g being Function of LTLB_WFF,BOOLEAN holds (VAL g) . ((con (f ^ f1)) /. (len (con (f ^ f1)))) = ((VAL g) . ((con f) /. (len (con f)))) '&' ((VAL g) . ((con f1) /. (len (con f1))))
let g be Function of LTLB_WFF,BOOLEAN; :: thesis: (VAL g) . ((con (f ^ f1)) /. (len (con (f ^ f1)))) = ((VAL g) . ((con f) /. (len (con f)))) '&' ((VAL g) . ((con f1) /. (len (con f1))))
set fp = (f ^ f1) | (len f);
set fk = (f ^ f1) /^ (len f);
set v = VAL g;
A1: (f ^ f1) /^ (len f) = f1 by FINSEQ_5:37;
A2: for n being Element of NAT
for f being FinSequence of LTLB_WFF holds (VAL g) . H2(f) = ((VAL g) . H2(f | n)) '&' ((VAL g) . H2(f /^ n))
proof
let n be Element of NAT ; :: thesis: for f being FinSequence of LTLB_WFF holds (VAL g) . H2(f) = ((VAL g) . H2(f | n)) '&' ((VAL g) . H2(f /^ n))
let f be FinSequence of LTLB_WFF ; :: thesis: (VAL g) . H2(f) = ((VAL g) . H2(f | n)) '&' ((VAL g) . H2(f /^ n))
defpred S1[ Nat] means (VAL g) . H2(f) = ((VAL g) . H2(f | $1)) '&' ((VAL g) . H2(f /^ $1));
len (f | 0) = 0 ;
then A3: con (f | 0) = <*TVERUM*> by Def2;
then len (con (f | 0)) = 1 by FINSEQ_1:39;
then A4: (con (f | 0)) /. (len (con (f | 0))) = TVERUM by FINSEQ_4:16, A3;
A5: for f being FinSequence of LTLB_WFF
for g being Function of LTLB_WFF,BOOLEAN holds (VAL g) . H2(f) = ((VAL g) . H2(f | 1)) '&' ((VAL g) . H2(f /^ 1))
proof
let f be FinSequence of LTLB_WFF ; :: thesis: for g being Function of LTLB_WFF,BOOLEAN holds (VAL g) . H2(f) = ((VAL g) . H2(f | 1)) '&' ((VAL g) . H2(f /^ 1))
let g be Function of LTLB_WFF,BOOLEAN; :: thesis: (VAL g) . H2(f) = ((VAL g) . H2(f | 1)) '&' ((VAL g) . H2(f /^ 1))
defpred S2[ Nat] means for f being FinSequence of LTLB_WFF st len f = $1 holds
(VAL g) . H2(f) = ((VAL g) . H2(f | 1)) '&' ((VAL g) . H2(f /^ 1));
A6: len f = len f ;
A7: now :: thesis: for n being Nat st S2[n] holds
S2[n + 1]
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A8: S2[n] ; :: thesis: S2[n + 1]
thus S2[n + 1] :: thesis: verum
proof
let f be FinSequence of LTLB_WFF ; :: thesis: ( len f = n + 1 implies (VAL g) . H2(f) = ((VAL g) . H2(f | 1)) '&' ((VAL g) . H2(f /^ 1)) )
set v = VAL g;
set fp1 = f | 1;
set fk1 = f /^ 1;
set fn = f | n;
set fn1 = f | (n + 1);
assume A9: len f = n + 1 ; :: thesis: (VAL g) . H2(f) = ((VAL g) . H2(f | 1)) '&' ((VAL g) . H2(f /^ 1))
then A10: n < len f by NAT_1:13;
A11: len (con f) = n + 1 by Def2, A9;
A12: 1 <= len f by A9, NAT_1:25;
then A13: len (f /^ 1) = (len f) - 1 by RFINSEQ:def 1
.= n by A9 ;
len (f | 1) = 1 by A12, FINSEQ_1:59;
then A14: len (con (f | 1)) = 1 by Def2;
A15: n <= len f by A9, NAT_1:13;
then A16: len (f | n) = n by FINSEQ_1:59;
A17: len (f | (n + 1)) = n + 1 by FINSEQ_1:59, A9;
then A18: 1 <= len (f | (n + 1)) by NAT_1:11;
A19: 1 <= n + 1 by NAT_1:11;
then A20: len ((f | (n + 1)) /^ 1) = (len (f | (n + 1))) - 1 by A17, RFINSEQ:def 1
.= n by A17 ;
per cases ( n = 0 or n > 0 ) ;
suppose A21: n = 0 ; :: thesis: (VAL g) . H2(f) = ((VAL g) . H2(f | 1)) '&' ((VAL g) . H2(f /^ 1))
then A22: f /^ 1 = {} by A13;
len (con f) = 1 by A21, A9, Def2;
hence (VAL g) . H2(f) = ((VAL g) . ((con (f | 1)) /. 1)) '&' TRUE by Th13, A21, A9
.= ((VAL g) . H2(f | 1)) '&' ((VAL g) . H2(f /^ 1)) by A14, A22, Th10, Th4 ;
:: thesis: verum
end;
suppose A23: n > 0 ; :: thesis: (VAL g) . H2(f) = ((VAL g) . H2(f | 1)) '&' ((VAL g) . H2(f /^ 1))
then A24: 1 <= len (f | n) by NAT_1:25, A16;
A25: 1 <= n by A23, NAT_1:25;
len (con (f | n)) = len (f | n) by A23, A16, Def2;
then (con f) /. n = H2(f | n) by A16, Th13, A25, A15;
then H2(f) = H2(f | n) '&&' (f /. (n + 1)) by Th7, A25, A10, A11;
then A26: (VAL g) . H2(f) = ((VAL g) . H2(f | n)) '&' ((VAL g) . (f /. (n + 1))) by LTLAXIO1:31
.= (((VAL g) . H2((f | n) | 1)) '&' ((VAL g) . H2((f | n) /^ 1))) '&' ((VAL g) . (f /. (n + 1))) by A8, A16
.= (((VAL g) . ((con (f | 1)) /. (len (con ((f | n) | 1))))) '&' ((VAL g) . H2((f | n) /^ 1))) '&' ((VAL g) . (f /. (n + 1))) by A25, FINSEQ_1:82
.= (((VAL g) . H2(f | 1)) '&' ((VAL g) . H2((f | n) /^ 1))) '&' ((VAL g) . (f /. (n + 1))) by A25, FINSEQ_1:82
.= ((VAL g) . H2(f | 1)) '&' (((VAL g) . H2((f | n) /^ 1)) '&' ((VAL g) . (f /. (n + 1))))
.= ((VAL g) . H2(f | 1)) '&' ((VAL g) . (H2((f | n) /^ 1) '&&' (f /. (n + 1)))) by LTLAXIO1:31 ;
per cases ( n = 1 or 1 < n ) by A23, NAT_1:25;
suppose A27: n = 1 ; :: thesis: (VAL g) . H2(f) = ((VAL g) . H2(f | 1)) '&' ((VAL g) . H2(f /^ 1))
then A28: 1 in dom (f /^ 1) by A13, FINSEQ_3:25;
A29: len (con (f /^ 1)) = 1 by Def2, A13, A27;
thus (VAL g) . H2(f) = (VAL g) . (((con f) /. 1) '&&' (f /. (1 + 1))) by Th7, A27, A9, A11
.= (VAL g) . (((con (f | 1)) /. 1) '&&' (f /. (1 + 1))) by Th13, A27, A9
.= ((VAL g) . ((con (f | 1)) /. 1)) '&' ((VAL g) . (f /. (1 + 1))) by LTLAXIO1:31
.= ((VAL g) . ((con (f | 1)) /. 1)) '&' ((VAL g) . ((f /^ 1) /. 1)) by FINSEQ_5:27, A28
.= ((VAL g) . H2(f | 1)) '&' ((VAL g) . H2(f /^ 1)) by A14, A29, Th6, A27, A13 ; :: thesis: verum
end;
suppose A30: 1 < n ; :: thesis: (VAL g) . H2(f) = ((VAL g) . H2(f | 1)) '&' ((VAL g) . H2(f /^ 1))
A31: (f | (n + 1)) /^ 1 = (f /^ 1) | n
proof
set f1 = (f /^ 1) | n;
set g = (f | (n + 1)) /^ 1;
A32: len ((f /^ 1) | n) = len ((f | (n + 1)) /^ 1) by A20, FINSEQ_1:59, A13;
now :: thesis: for x being Nat st x in dom ((f /^ 1) | n) holds
((f /^ 1) | n) . x = ((f | (n + 1)) /^ 1) . x
let x be Nat; :: thesis: ( x in dom ((f /^ 1) | n) implies ((f /^ 1) | n) . x = ((f | (n + 1)) /^ 1) . x )
A33: dom ((f /^ 1) | n) c= dom (f /^ 1) by FINSEQ_5:18;
assume A34: x in dom ((f /^ 1) | n) ; :: thesis: ((f /^ 1) | n) . x = ((f | (n + 1)) /^ 1) . x
then A35: x in dom ((f | (n + 1)) /^ 1) by FINSEQ_3:29, A32;
x <= len ((f /^ 1) | n) by A34, FINSEQ_3:25;
then A36: x <= n by FINSEQ_1:59, A13;
hence ((f /^ 1) | n) . x = (f /^ 1) . x by FINSEQ_3:112
.= f . (x + 1) by RFINSEQ:def 1, A33, A34, A12
.= (f | (n + 1)) . (x + 1) by FINSEQ_3:112, A36, XREAL_1:6
.= ((f | (n + 1)) /^ 1) . x by RFINSEQ:def 1, A18, A35 ;
:: thesis: verum
end;
hence (f | (n + 1)) /^ 1 = (f /^ 1) | n by FINSEQ_2:9, A32; :: thesis: verum
end;
A37: n + (- 1) > 1 + (- 1) by A30, XREAL_1:8;
then A38: (n -' 1) + 1 = (n - 1) + 1 by XREAL_0:def 2
.= n ;
len (con (f /^ 1)) = len (f /^ 1) by A13, A30, Def2;
then A39: len (con (f /^ 1)) = (len f) -' 1 by RFINSEQ:29
.= n by NAT_D:34, A9 ;
A40: n in dom ((f | (n + 1)) /^ 1) by FINSEQ_3:25, A30, A20;
A41: n - 1 > 0 by A37;
then n -' 1 > 0 by XREAL_0:def 2;
then A42: 1 <= n -' 1 by NAT_1:25;
A43: f /. (n + 1) = f . (n + 1) by A19, A9, FINSEQ_4:15
.= (f | (n + 1)) . (n + 1) by FINSEQ_3:112
.= ((f | (n + 1)) /^ 1) . n by RFINSEQ:def 1, A40, A19, A17
.= ((f | (n + 1)) /^ 1) /. ((n -' 1) + 1) by A38, PARTFUN1:def 6, A40 ;
A44: (- 1) + n < n by XREAL_1:30;
then A45: n -' 1 < len ((f | (n + 1)) /^ 1) by A20, XREAL_0:def 2, A41;
A46: len ((f | n) /^ 1) = n - 1 by RFINSEQ:def 1, A24, A16;
then A47: len (con ((f | n) /^ 1)) = len ((f | n) /^ 1) by A37, Def2
.= n -' 1 by XREAL_0:def 2, A46 ;
then len (con ((f | n) /^ 1)) = n - 1 by A46, XREAL_0:def 2;
then A48: 1 <= len (con ((f | n) /^ 1)) by A37, NAT_1:25;
A49: len ((f | n) /^ 1) = n -' 1 by XREAL_0:def 2, A46;
A50: ((f | (n + 1)) /^ 1) | (n -' 1) = (f | n) /^ 1
proof
set f1 = ((f | (n + 1)) /^ 1) | (n -' 1);
set g = (f | n) /^ 1;
A51: len (((f | (n + 1)) /^ 1) | (n -' 1)) = len ((f | n) /^ 1) by A49, FINSEQ_1:59, A45;
now :: thesis: for x being Nat st x in dom (((f | (n + 1)) /^ 1) | (n -' 1)) holds
(((f | (n + 1)) /^ 1) | (n -' 1)) . x = ((f | n) /^ 1) . x
A52: dom (((f | (n + 1)) /^ 1) | (n -' 1)) c= dom ((f | (n + 1)) /^ 1) by FINSEQ_5:18;
let x be Nat; :: thesis: ( x in dom (((f | (n + 1)) /^ 1) | (n -' 1)) implies (((f | (n + 1)) /^ 1) | (n -' 1)) . x = ((f | n) /^ 1) . x )
A53: n <= n + 1 by XREAL_1:31;
assume A54: x in dom (((f | (n + 1)) /^ 1) | (n -' 1)) ; :: thesis: (((f | (n + 1)) /^ 1) | (n -' 1)) . x = ((f | n) /^ 1) . x
then A55: x in dom ((f | n) /^ 1) by FINSEQ_3:29, A51;
x <= len (((f | (n + 1)) /^ 1) | (n -' 1)) by A54, FINSEQ_3:25;
then A56: x <= n -' 1 by FINSEQ_1:59, A45;
then A57: x + 1 <= n by XREAL_1:6, A38;
thus (((f | (n + 1)) /^ 1) | (n -' 1)) . x = ((f | (n + 1)) /^ 1) . x by FINSEQ_3:112, A56
.= (f | (n + 1)) . (x + 1) by RFINSEQ:def 1, A52, A54, A18
.= f . (x + 1) by FINSEQ_3:112, A53, XXREAL_0:2, A57
.= (f | n) . (x + 1) by FINSEQ_3:112, A56, XREAL_1:6, A38
.= ((f | n) /^ 1) . x by RFINSEQ:def 1, A25, A16, A55 ; :: thesis: verum
end;
hence ((f | (n + 1)) /^ 1) | (n -' 1) = (f | n) /^ 1 by FINSEQ_2:9, A51; :: thesis: verum
end;
len (con ((f | n) /^ 1)) = len ((f | n) /^ 1) by A46, A37, Def2;
then H2((f | n) /^ 1) '&&' (f /. (n + 1)) = ((con ((f | (n + 1)) /^ 1)) /. (n -' 1)) '&&' (f /. (n + 1)) by A47, Th13, A48, A46, A44, A20, A50
.= (con ((f | (n + 1)) /^ 1)) /. ((n -' 1) + 1) by Th7, A45, A42, A43
.= (con (f /^ 1)) /. (len (con (f /^ 1))) by A39, A13, A25, Th13, A31, A38 ;
hence (VAL g) . H2(f) = ((VAL g) . H2(f | 1)) '&' ((VAL g) . H2(f /^ 1)) by A26; :: thesis: verum
end;
end;
end;
end;
end;
end;
A58: S2[ 0 ]
proof
let f be FinSequence of LTLB_WFF ; :: thesis: ( len f = 0 implies (VAL g) . H2(f) = ((VAL g) . H2(f | 1)) '&' ((VAL g) . H2(f /^ 1)) )
set v = VAL g;
set fp1 = f | 1;
set fk1 = f /^ 1;
assume A59: len f = 0 ; :: thesis: (VAL g) . H2(f) = ((VAL g) . H2(f | 1)) '&' ((VAL g) . H2(f /^ 1))
then len (f /^ 1) = 0 by Th2;
then A60: f /^ 1 = {} ;
( f = {} & f | 1 = f ) by A59, FINSEQ_1:58;
hence (VAL g) . H2(f) = ((VAL g) . H2(f | 1)) '&' ((VAL g) . H2(f /^ 1)) by A60; :: thesis: verum
end;
for n being Nat holds S2[n] from NAT_1:sch 2(A58, A7);
 hence (VAL g) . H2(f) = ((VAL g) . H2(f | 1)) '&' ((VAL g) . H2(f /^ 1)) by A6; :: thesis: verum
end;
A61: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A62: S1[n] ; :: thesis: S1[n + 1]
set v = VAL g;
set fe = f /^ n;
set fs1 = f | (n + 1);
set fs = f | n;
set fe1 = f /^ (n + 1);
per cases ( len f = 0 or len f > 0 ) ;
suppose A63: len f = 0 ; :: thesis: S1[n + 1]
then A64: f /^ (n + 1) = f by Th2;
A65: f = {} by A63;
then f | (n + 1) = {} by FINSEQ_1:58, A63;
hence (VAL g) . H2(f) = ((VAL g) . H2(f | (n + 1))) '&' ((VAL g) . H2(f /^ (n + 1))) by A64, A65; :: thesis: verum
end;
suppose A66: len f > 0 ; :: thesis: S1[n + 1]
then len f >= 1 by NAT_1:25;
then A67: len (f | 1) = 1 by FINSEQ_1:59;
then A68: 1 in dom (f | 1) by FINSEQ_3:25;
A69: len (f | (n + 1)) > 0 by A66, Th1;
then len (f | (n + 1)) >= 1 by NAT_1:25;
then A70: 1 in dom (f | (n + 1)) by FINSEQ_3:25;
A71: len (con (f | 1)) = 1 by A67, Def2;
A72: 1 <= n + 1 by XREAL_1:31;
per cases ( len (f | (n + 1)) = 1 or len (f | (n + 1)) > 1 ) by A69, NAT_1:25;
suppose A73: len (f | (n + 1)) = 1 ; :: thesis: S1[n + 1]
then len (con (f | (n + 1))) = 1 by Def2;
then A74: H2(f | (n + 1)) = (f | (n + 1)) /. 1 by Th6, A69
.= f /. 1 by FINSEQ_4:70, A70
.= (f | 1) /. 1 by FINSEQ_4:70, A68
.= H2(f | 1) by A71, Th6, A67 ;
per cases ( n + 1 <= len f or n + 1 > len f ) ;
suppose n + 1 <= len f ; :: thesis: S1[n + 1]
then len (f | (n + 1)) = n + 1 by FINSEQ_1:59;
hence (VAL g) . H2(f) = ((VAL g) . H2(f | (n + 1))) '&' ((VAL g) . H2(f /^ (n + 1))) by A73, A5; :: thesis: verum
end;
suppose n + 1 > len f ; :: thesis: S1[n + 1]
then A75: f /^ (n + 1) = {} by RFINSEQ:def 1;
then A76: len (f /^ (n + 1)) = 0 ;
f = (f | (n + 1)) ^ (f /^ (n + 1)) by RFINSEQ:8;
then len f = (len (f | (n + 1))) + (len (f /^ (n + 1))) by FINSEQ_1:22
.= 1 by A73, A76 ;
then f | 1 = f by FINSEQ_1:58;
hence (VAL g) . H2(f) = ((VAL g) . H2(f | 1)) '&' TRUE
.= ((VAL g) . H2(f | (n + 1))) '&' ((VAL g) . H2(f /^ (n + 1))) by A74, Th10, A75, Th4 ;
:: thesis: verum
end;
end;
end;
suppose A77: len (f | (n + 1)) > 1 ; :: thesis: S1[n + 1]
per cases ( n + 1 > len f or n + 1 <= len f ) ;
suppose A78: n + 1 > len f ; :: thesis: S1[n + 1]
then A79: f /^ (n + 1) = 0 by RFINSEQ:def 1;
f | (n + 1) = f by FINSEQ_1:58, A78;
hence (VAL g) . H2(f) = ((VAL g) . H2(f | (n + 1))) '&' TRUE
.= ((VAL g) . H2(f | (n + 1))) '&' ((VAL g) . H2(f /^ (n + 1))) by A79, Th10, Th4 ;
:: thesis: verum
end;
suppose A80: n + 1 <= len f ; :: thesis: S1[n + 1]
then A81: len (f | (n + 1)) = n + 1 by FINSEQ_1:59;
then A82: n + 1 in dom (f | (n + 1)) by FINSEQ_3:25, A72;
A83: ( n + 1 = len (con (f | (n + 1))) & n < len (f | (n + 1)) ) by A81, Def2, XREAL_1:145;
A84: (n + 1) + (- n) <= (len f) + (- n) by A80, XREAL_1:6;
A85: len (f /^ n) = (len f) -' n by RFINSEQ:29
.= (len f) - n by XREAL_0:def 2, A84 ;
then A86: len ((f /^ n) | 1) = 1 by A84, FINSEQ_1:59;
then A87: 1 in dom ((f /^ n) | 1) by FINSEQ_3:25;
A88: 1 in dom (f /^ n) by A85, A84, FINSEQ_3:25;
len (con ((f /^ n) | 1)) = 1 by A86, Def2;
then A89: H2((f /^ n) | 1) = ((f /^ n) | 1) /. 1 by Th6, A86
.= (f /^ n) /. 1 by A87, FINSEQ_4:70
.= f /. (n + 1) by FINSEQ_5:27, A88
.= (f | (n + 1)) /. (n + 1) by FINSEQ_4:70, A82 ;
A90: (f /^ n) /^ 1 = f /^ (n + 1) by FINSEQ_6:81;
A91: (n + 1) + (- 1) > 1 + (- 1) by A77, A81, XREAL_1:8;
then A92: n >= 1 by NAT_1:25;
A93: n <= n + 1 by XREAL_1:31;
then len (f | n) = n by XXREAL_0:2, A80, FINSEQ_1:59;
then A94: len (con (f | n)) = n by Def2, A91;
A95: H2(f | n) = (con ((f | (n + 1)) | n)) /. (len (con (f | n))) by FINSEQ_5:77, A93
.= (con (f | (n + 1))) /. n by A94, Th13, A93, A81, A92 ;
A96: 1 <= n by NAT_1:25, A91;
thus (VAL g) . H2(f) = ((VAL g) . H2(f | n)) '&' (((VAL g) . H2((f /^ n) | 1)) '&' ((VAL g) . H2((f /^ n) /^ 1))) by A5, A62
.= (((VAL g) . H2(f | n)) '&' ((VAL g) . H2((f /^ n) | 1))) '&' ((VAL g) . H2(f /^ (n + 1))) by A90
.= ((VAL g) . (H2(f | n) '&&' H2((f /^ n) | 1))) '&' ((VAL g) . H2(f /^ (n + 1))) by LTLAXIO1:31
.= ((VAL g) . H2(f | (n + 1))) '&' ((VAL g) . H2(f /^ (n + 1))) by A83, Th7, A96, A95, A89 ; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
f /^ 0 = f by FINSEQ_5:28;
then (VAL g) . H2(f) = TRUE '&' ((VAL g) . H2(f /^ 0))
.= ((VAL g) . H2(f | 0)) '&' ((VAL g) . H2(f /^ 0)) by A4, Th4 ;
then A97: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A97, A61);
 hence (VAL g) . H2(f) = ((VAL g) . H2(f | n)) '&' ((VAL g) . H2(f /^ n)) ; :: thesis: verum
end;
Seg (len f) c= dom f by FINSEQ_1:def 3;
then (f ^ f1) | (len f) = f | (len f) by FINSEQ_6:11
.= f by FINSEQ_1:58 ;
hence (VAL g) . H2(f ^ f1) = ((VAL g) . H2(f)) '&' ((VAL g) . H2(f1)) by A1, A2; :: thesis: verum