let Al be QC-alphabet ; :: thesis: for f, g being FinSequence of CQC-WFF Al st len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & Ant f |= Suc f & Ant g |= Suc g holds

Ant (Ant f) |= Suc f

let f, g be FinSequence of CQC-WFF Al; :: thesis: ( len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & Ant f |= Suc f & Ant g |= Suc g implies Ant (Ant f) |= Suc f )

assume that

A1: len f > 1 and

A2: len g > 1 and

A3: Ant (Ant f) = Ant (Ant g) and

A4: 'not' (Suc (Ant f)) = Suc (Ant g) and

A5: Suc f = Suc g and

A6: Ant f |= Suc f and

A7: Ant g |= Suc g ; :: thesis: Ant (Ant f) |= Suc f

let A be non empty set ; :: according to CALCUL_1:def 15 :: thesis: for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= Ant (Ant f) holds

J,v |= Suc f

let J be interpretation of Al,A; :: thesis: for v being Element of Valuations_in (Al,A) st J,v |= Ant (Ant f) holds

J,v |= Suc f

let v be Element of Valuations_in (Al,A); :: thesis: ( J,v |= Ant (Ant f) implies J,v |= Suc f )

assume A8: J,v |= Ant (Ant f) ; :: thesis: J,v |= Suc f

A9: len (Ant g) > 0 by A2, Th4;

Ant (Ant f) |= Suc f

let f, g be FinSequence of CQC-WFF Al; :: thesis: ( len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & Ant f |= Suc f & Ant g |= Suc g implies Ant (Ant f) |= Suc f )

assume that

A1: len f > 1 and

A2: len g > 1 and

A3: Ant (Ant f) = Ant (Ant g) and

A4: 'not' (Suc (Ant f)) = Suc (Ant g) and

A5: Suc f = Suc g and

A6: Ant f |= Suc f and

A7: Ant g |= Suc g ; :: thesis: Ant (Ant f) |= Suc f

let A be non empty set ; :: according to CALCUL_1:def 15 :: thesis: for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= Ant (Ant f) holds

J,v |= Suc f

let J be interpretation of Al,A; :: thesis: for v being Element of Valuations_in (Al,A) st J,v |= Ant (Ant f) holds

J,v |= Suc f

let v be Element of Valuations_in (Al,A); :: thesis: ( J,v |= Ant (Ant f) implies J,v |= Suc f )

assume A8: J,v |= Ant (Ant f) ; :: thesis: J,v |= Suc f

A9: len (Ant g) > 0 by A2, Th4;

A10: now :: thesis: ( not J,v |= Suc (Ant f) implies J,v |= Suc f )

A11:
len (Ant f) > 0
by A1, Th4;assume
not J,v |= Suc (Ant f)
; :: thesis: J,v |= Suc f

then J,v |= Suc (Ant g) by A4, VALUAT_1:17;

then J,v |= Ant g by A3, A9, A8, Th17;

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

end;then J,v |= Suc (Ant g) by A4, VALUAT_1:17;

then J,v |= Ant g by A3, A9, A8, Th17;

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

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

hence
J,v |= Suc f
by A10; :: thesis: verumassume
J,v |= Suc (Ant f)
; :: thesis: J,v |= Suc f

then J,v |= Ant f by A11, A8, Th17;

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

end;then J,v |= Ant f by A11, A8, Th17;

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