:: CALCUL_1 semantic presentation

registration

let g be FinSequence;
let N be set ;
cluster g | N -> FinSubsequence-like ;
coherence by FINSEQ_1:69;

end;

definition

let D be non empty set ;
let f be FinSequence of D;
func Ant f -> FinSequence of D means :Def1: :: CALCUL_1:def 1
for i being Element of NAT st len f = i + 1 holds
it = f | (Seg i) if len f > 0
otherwise it = {} ;
existence

proof end;

proof end;

consistency ;

end;

:: deftheorem Def1 defines Ant CALCUL_1:def 1 :

definition

let D be non empty set ;
let f be FinSequence of D;
assume A1: len f > 0 ;
func Suc f -> Element of D equals :Def2: :: CALCUL_1:def 2
f . (len f);
coherence

proof end;

end;

:: deftheorem Def2 defines Suc CALCUL_1:def 2 :

definition

let D be non empty set ;
let p be Element of D;
let f be FinSequence of D;
pred p is_tail_of f means :Def3: :: CALCUL_1:def 3
ex i being Element of NAT st
( i in dom f & f . i = p );

end;

:: deftheorem Def3 defines is_tail_of CALCUL_1:def 3 :

definition

let f, g be FinSequence of CQC-WFF ;
pred f is_Subsequence_of g means :Def4: :: CALCUL_1:def 4
ex N being Subset of NAT st f c= Seq (g | N);

end;

:: deftheorem Def4 defines is_Subsequence_of CALCUL_1:def 4 :

theorem Th1: :: CALCUL_1:1

for f, g being FinSequence of CQC-WFF st f is_Subsequence_of g holds
( rng f c= rng g & ex N being Subset of NAT st rng f c= rng (g | N) )

proof end;

theorem Th2: :: CALCUL_1:2

for f being FinSequence of CQC-WFF st len f > 0 holds
( (len (Ant f)) + 1 = len f & len (Ant f) < len f )

proof end;

theorem Th3: :: CALCUL_1:3

for f being FinSequence of CQC-WFF st len f > 0 holds
( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} )

proof end;

theorem Th4: :: CALCUL_1:4

for f being FinSequence of CQC-WFF st len f > 1 holds
len (Ant f) > 0

proof end;

theorem Th5: :: CALCUL_1:5

for p being Element of CQC-WFF
for f being FinSequence of CQC-WFF holds
( Suc (f ^ <*p*>) = p & Ant (f ^ <*p*>) = f )

proof end;

theorem Th6: :: CALCUL_1:6

for fin, fin1 being FinSequence holds
( len fin <= len (fin ^ fin1) & len fin1 <= len (fin ^ fin1) & ( fin <> {} implies ( 1 <= len fin & len fin1 < len (fin1 ^ fin) ) ) )

proof end;

theorem Th7: :: CALCUL_1:7

for f, g being FinSequence of CQC-WFF holds Seq ((f ^ g) | (dom f)) = (f ^ g) | (dom f)

proof end;

theorem Th8: :: CALCUL_1:8

for f, g being FinSequence of CQC-WFF holds f is_Subsequence_of f ^ g

proof end;

theorem Th9: :: CALCUL_1:9

for b, c being set
for fin being FinSequence holds 1 < len ((fin ^ <*b*>) ^ <*c*>)

proof end;

theorem Th10: :: CALCUL_1:10

for b being set
for fin being FinSequence holds
( 1 <= len (fin ^ <*b*>) & len (fin ^ <*b*>) in dom (fin ^ <*b*>) )

proof end;

theorem Th11: :: CALCUL_1:11

for m, n being Element of NAT st 0 < m holds
len (Sgm ((Seg n) \/ {(n + m)})) = n + 1

proof end;

theorem Th12: :: CALCUL_1:12

for m, n being Element of NAT st 0 < m holds
dom (Sgm ((Seg n) \/ {(n + m)})) = Seg (n + 1)

proof end;

theorem Th13: :: CALCUL_1:13

for f, g being FinSequence of CQC-WFF st 0 < len f holds
f is_Subsequence_of ((Ant f) ^ g) ^ <*(Suc f)*>

proof end;

theorem Th14: :: CALCUL_1:14

for c, d being set
for f being FinSequence of CQC-WFF holds
( 1 in dom <*c,d*> & 2 in dom <*c,d*> & (f ^ <*c,d*>) . ((len f) + 1) = c & (f ^ <*c,d*>) . ((len f) + 2) = d )

proof end;

definition

let f be FinSequence of CQC-WFF ;
func still_not-bound_in f -> Subset of bound_QC-variables means :Def5: :: CALCUL_1:def 5
for a being set holds
( a in it iff ex i being Element of NAT ex p being Element of CQC-WFF st
( i in dom f & p = f . i & a in still_not-bound_in p ) );
existence

proof end;

proof end;

end;

:: deftheorem Def5 defines still_not-bound_in CALCUL_1:def 5 :

definition

func set_of_CQC-WFF-seq -> set means :Def6: :: CALCUL_1:def 6
for a being set holds
( a in it iff a is FinSequence of CQC-WFF );
existence

proof end;

proof end;

end;

:: deftheorem Def6 defines set_of_CQC-WFF-seq CALCUL_1:def 6 :

definition

let PR be FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :];
let n be Element of NAT ;
pred PR,n is_a_correct_step means :Def7: :: CALCUL_1:def 7
ex f being FinSequence of CQC-WFF st
( Suc f is_tail_of Ant f & (PR . n) `1 = f ) if (PR . n) `2 = 0
ex f being FinSequence of CQC-WFF st (PR . n) `1 = f ^ <*VERUM *> if (PR . n) `2 = 1
ex i being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) if (PR . n) `2 = 2
ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) if (PR . n) `2 = 3
ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF ex p being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) if (PR . n) `2 = 4
ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) if (PR . n) `2 = 5
ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) if (PR . n) `2 = 6
ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) if (PR . n) `2 = 7
ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = All x,p & f = (PR . i) `1 & (Ant f) ^ <*(p . x,y)*> = (PR . n) `1 ) if (PR . n) `2 = 8
ex i being Element of NAT ex f being FinSequence of CQC-WFF ex p being Element of CQC-WFF ex x, y being bound_QC-variable st
( 1 <= i & i < n & Suc f = p . x,y & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All x,p) & f = (PR . i) `1 & (Ant f) ^ <*(All x,p)*> = (PR . n) `1 ) if (PR . n) `2 = 9
;
consistency