let Al be QC-alphabet ; :: thesis: for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A)

for f being FinSequence of CQC-WFF Al st len f > 0 holds

( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )

let A be non empty set ; :: thesis: for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A)

for f being FinSequence of CQC-WFF Al st len f > 0 holds

( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )

let J be interpretation of Al,A; :: thesis: for v being Element of Valuations_in (Al,A)

for f being FinSequence of CQC-WFF Al st len f > 0 holds

( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )

let v be Element of Valuations_in (Al,A); :: thesis: for f being FinSequence of CQC-WFF Al st len f > 0 holds

( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )

let f be FinSequence of CQC-WFF Al; :: thesis: ( len f > 0 implies ( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f ) )

assume A1: len f > 0 ; :: thesis: ( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )

thus ( J,v |= Ant f & J,v |= Suc f implies J,v |= f ) :: thesis: ( J,v |= f implies ( J,v |= Ant f & J,v |= Suc f ) )

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A)

for f being FinSequence of CQC-WFF Al st len f > 0 holds

( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )

let A be non empty set ; :: thesis: for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A)

for f being FinSequence of CQC-WFF Al st len f > 0 holds

( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )

let J be interpretation of Al,A; :: thesis: for v being Element of Valuations_in (Al,A)

for f being FinSequence of CQC-WFF Al st len f > 0 holds

( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )

let v be Element of Valuations_in (Al,A); :: thesis: for f being FinSequence of CQC-WFF Al st len f > 0 holds

( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )

let f be FinSequence of CQC-WFF Al; :: thesis: ( len f > 0 implies ( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f ) )

assume A1: len f > 0 ; :: thesis: ( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )

thus ( J,v |= Ant f & J,v |= Suc f implies J,v |= f ) :: thesis: ( J,v |= f implies ( J,v |= Ant f & J,v |= Suc f ) )

proof

thus
( J,v |= f implies ( J,v |= Ant f & J,v |= Suc f ) )
:: thesis: verum
assume that

A2: J,v |= Ant f and

A3: J,v |= Suc f ; :: thesis: J,v |= f

let p be Element of CQC-WFF Al; :: according to CALCUL_1:def 11,CALCUL_1:def 14 :: thesis: ( p in rng f implies J,v |= p )

assume p in rng f ; :: thesis: J,v |= p

then p in (rng (Ant f)) \/ {(Suc f)} by A1, Th3;

then A4: ( p in rng (Ant f) or p in {(Suc f)} ) by XBOOLE_0:def 3;

J,v |= rng (Ant f) by A2;

hence J,v |= p by A3, A4, TARSKI:def 1; :: thesis: verum

end;A2: J,v |= Ant f and

A3: J,v |= Suc f ; :: thesis: J,v |= f

let p be Element of CQC-WFF Al; :: according to CALCUL_1:def 11,CALCUL_1:def 14 :: thesis: ( p in rng f implies J,v |= p )

assume p in rng f ; :: thesis: J,v |= p

then p in (rng (Ant f)) \/ {(Suc f)} by A1, Th3;

then A4: ( p in rng (Ant f) or p in {(Suc f)} ) by XBOOLE_0:def 3;

J,v |= rng (Ant f) by A2;

hence J,v |= p by A3, A4, TARSKI:def 1; :: thesis: verum

proof

assume A5:
J,v |= rng f
; :: according to CALCUL_1:def 14 :: thesis: ( J,v |= Ant f & J,v |= Suc f )

thus J,v |= rng (Ant f) :: according to CALCUL_1:def 14 :: thesis: J,v |= Suc f

then A7: len f in dom f by FINSEQ_3:25;

Suc f = f . (len f) by A1, Def2;

then Suc f in rng f by A7, FUNCT_1:3;

hence J,v |= Suc f by A5; :: thesis: verum

end;thus J,v |= rng (Ant f) :: according to CALCUL_1:def 14 :: thesis: J,v |= Suc f

proof

0 + 1 <= len f
by A1, NAT_1:13;
A6:
rng (Ant f) c= (rng (Ant f)) \/ {(Suc f)}
by XBOOLE_1:7;

let p be Element of CQC-WFF Al; :: according to CALCUL_1:def 11 :: thesis: ( p in rng (Ant f) implies J,v |= p )

assume p in rng (Ant f) ; :: thesis: J,v |= p

then p in (rng (Ant f)) \/ {(Suc f)} by A6;

then p in rng f by A1, Th3;

hence J,v |= p by A5; :: thesis: verum

end;let p be Element of CQC-WFF Al; :: according to CALCUL_1:def 11 :: thesis: ( p in rng (Ant f) implies J,v |= p )

assume p in rng (Ant f) ; :: thesis: J,v |= p

then p in (rng (Ant f)) \/ {(Suc f)} by A6;

then p in rng f by A1, Th3;

hence J,v |= p by A5; :: thesis: verum

then A7: len f in dom f by FINSEQ_3:25;

Suc f = f . (len f) by A1, Def2;

then Suc f in rng f by A7, FUNCT_1:3;

hence J,v |= Suc f by A5; :: thesis: verum