let S be non empty set ; for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g, h being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S holds
( s |= h iff s |= Foax (g,f,h) ) ) holds
for s being Element of S st s |= f EU g holds
s |= h
let R be total Relation of S,S; for BASSIGN being non empty Subset of (ModelSP S)
for f, g, h being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S holds
( s |= h iff s |= Foax (g,f,h) ) ) holds
for s being Element of S st s |= f EU g holds
s |= h
let BASSIGN be non empty Subset of (ModelSP S); for f, g, h being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S holds
( s |= h iff s |= Foax (g,f,h) ) ) holds
for s being Element of S st s |= f EU g holds
s |= h
let f, g, h be Assign of (BASSModel (R,BASSIGN)); ( ( for s being Element of S holds
( s |= h iff s |= Foax (g,f,h) ) ) implies for s being Element of S st s |= f EU g holds
s |= h )
assume A1:
for s being Element of S holds
( s |= h iff s |= Foax (g,f,h) )
; for s being Element of S st s |= f EU g holds
s |= h
let s0 be Element of S; ( s0 |= f EU g implies s0 |= h )
assume
s0 |= f EU g
; s0 |= h
then consider pai being inf_path of R such that
A2:
pai . 0 = s0
and
A3:
ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j |= f ) & pai . m |= g )
by Th16;
consider m being Element of NAT such that
A4:
for j being Element of NAT st j < m holds
pai . j |= f
and
A5:
pai . m |= g
by A3;
for j being Element of NAT st j <= m holds
pai . (k_nat (m - j)) |= h
proof
defpred S1[
Nat]
means ( $1
<= m implies
pai . (k_nat (m - $1)) |= h );
A6:
for
j being
Nat st
S1[
j] holds
S1[
j + 1]
proof
let j be
Nat;
( S1[j] implies S1[j + 1] )
assume A7:
S1[
j]
;
S1[j + 1]
set j1 =
j + 1;
(
j + 1
<= m implies
pai . (k_nat (m - (j + 1))) |= h )
proof
set k =
m - (j + 1);
assume A8:
j + 1
<= m
;
pai . (k_nat (m - (j + 1))) |= h
then reconsider k =
m - (j + 1) as
Element of
NAT by NAT_1:21;
set pai1 =
PathShift (
pai,
k);
A9:
(PathShift (pai,k)) . 0 =
pai . (k + 0)
by Def67
.=
pai . k
;
k <= k + j
by NAT_1:12;
then
k < (k + j) + 1
by NAT_1:13;
then A10:
pai . k |= f
by A4;
A11:
(PathShift (pai,k)) . 1
= pai . (k + 1)
by Def67;
pai . (k + 1) |= h
by A7, A8, Def2, NAT_1:13;
then
pai . k |= EX h
by A9, A11, Th14;
then
pai . k |= Fax (
f,
h)
by A10, Th13;
then A12:
pai . k |= Foax (
g,
f,
h)
by Th17;
k_nat k = k
by Def2;
hence
pai . (k_nat (m - (j + 1))) |= h
by A1, A12;
verum
end;
hence
S1[
j + 1]
;
verum
end;
A13:
S1[
0 ]
for
j being
Nat holds
S1[
j]
from NAT_1:sch 2(A13, A6);
hence
for
j being
Element of
NAT st
j <= m holds
pai . (k_nat (m - j)) |= h
;
verum
end;
then
pai . (k_nat (m - m)) |= h
;
hence
s0 |= h
by A2, Def2; verum