:: COMPUT_1 semantic presentation

definition

let c₁ be non empty set ;
let c₂ be Nat;
let c₃ be Element of c₂ -tuples_on c₁;
let c₄ be Nat;
let c₅ be Element of c₁;
redefine func +* as c₃ +* c₄,c₅ -> Element of a₂ -tuples_on a₁;
coherence

proof end;

end;

definition

let c₁ be Nat;
let c₂ be Element of c₁ -tuples_on NAT ;
let c₃ be Nat;
redefine func . as c₂ . c₃ -> Element of NAT ;
coherence

proof end;

end;

theorem Th1: :: COMPUT_1:1

canceled;

theorem Th2: :: COMPUT_1:2

canceled;

theorem Th3: :: COMPUT_1:3

for b₁, b₂, b₃ being set holds
( <*b₁,b₂*> +* 1,b₃ = <*b₃,b₂*> & <*b₁,b₂*> +* 2,b₃ = <*b₁,b₃*> )

proof end;

theorem Th4: :: COMPUT_1:4

canceled;

theorem Th5: :: COMPUT_1:5

for b₁, b₂, b₃, b₄ being set
for b₅, b₆ being Function st b₅ +* b₁,b₂ = b₆ +* b₁,b₃ holds
b₅ +* b₁,b₄ = b₆ +* b₁,b₄

proof end;

theorem Th6: :: COMPUT_1:6

for b₁ being Nat
for b₂ being set
for b₃ being FinSequence holds Del (b₃ +* b₁,b₂),b₁ = Del b₃,b₁

proof end;

theorem Th7: :: COMPUT_1:7

for b₁ being Nat
for b₂ being set
for b₃, b₄ being FinSequence st b₃ +* b₁,b₂ = b₄ +* b₁,b₂ holds
Del b₃,b₁ = Del b₄,b₁

proof end;

theorem Th8: :: COMPUT_1:8

for b₁ being set holds 0 -tuples_on b₁ = {{} }

proof end;

theorem Th9: :: COMPUT_1:9

for b₁ being Nat st b₁ <> 0 holds
b₁ -tuples_on {} = {}

proof end;

theorem Th10: :: COMPUT_1:10

for b₁ being Function st {} in rng b₁ holds
<:b₁:> = {}

proof end;

theorem Th11: :: COMPUT_1:11

for b₁ being non empty set
for b₂ being Function st rng b₂ = b₁ holds
rng <:<*b₂*>:> = 1 -tuples_on b₁

proof end;

theorem Th12: :: COMPUT_1:12

for b₁, b₂ being Nat
for b₃ being non empty set st 1 <= b₁ & b₁ <= b₂ + 1 holds
for b₄ being Element of (b₂ + 1) -tuples_on b₃ holds Del b₄,b₁ in b₂ -tuples_on b₃

proof end;

theorem Th13: :: COMPUT_1:13

for b₁ being set
for b₂ being FinSequenceSet of b₁ holds b₂ c= b₁ *

proof end;

definition

let c₁ be set ;
attr a₁ is compatible means :Def1: :: COMPUT_1:def 1
for b₁, b₂ being Function st b₁ in a₁ & b₂ in a₁ holds
b₁ tolerates b₂;

end;

:: deftheorem Def1 defines compatible COMPUT_1:def 1 :

registration

cluster non empty functional compatible set ;
existence

proof end;

end;

registration

let c₁ be functional compatible set ;
cluster union a₁ -> Relation-like Function-like ;
coherence

proof end;

end;

theorem Th14: :: COMPUT_1:14

for b₁ being set holds
( ( b₁ is functional & b₁ is compatible ) iff union b₁ is Function )

proof end;

registration

let c₁, c₂ be set ;
cluster compatible PartFunc-set of a₁,a₂;
existence

proof end;

end;

theorem Th15: :: COMPUT_1:15

for b₁ being non empty functional compatible set holds dom (union b₁) = union { (dom b₂) where B is Element of b₁ : verum }

proof end;

theorem Th16: :: COMPUT_1:16

for b₁ being functional compatible set
for b₂ being Function st b₂ in b₁ holds
( dom b₂ c= dom (union b₁) & ( for b₃ being set st b₃ in dom b₂ holds
(union b₁) . b₃ = b₂ . b₃ ) )

proof end;

theorem Th17: :: COMPUT_1:17

for b₁ being non empty functional compatible set holds rng (union b₁) = union { (rng b₂) where B is Element of b₁ : verum }

proof end;

registration

let c₁, c₂ be set ;
cluster -> functional PartFunc-set of a₁,a₂;
coherence

proof end;

end;

theorem Th18: :: COMPUT_1:18

for b₁, b₂ being set
for b₃ being compatible PFUNC_DOMAIN of b₁,b₂ holds union b₃ is PartFunc of b₁,b₂

proof end;

notation

let c₁ be Relation;
synonym to-naturals c₁ for natural-yielding c₁;

end;

definition

let c₁ be Relation;
attr a₁ is from-natural-fseqs means :Def2: :: COMPUT_1:def 2
dom a₁ c= NAT * ;

end;

:: deftheorem Def2 defines from-natural-fseqs COMPUT_1:def 2 :

registration

cluster to-naturals from-natural-fseqs set ;
existence

proof end;

end;

definition

let c₁ be from-natural-fseqs Relation;
attr a₁ is len-total means :Def3: :: COMPUT_1:def 3
for b₁, b₂ being FinSequence of NAT st len b₁ = len b₂ & b₁ in dom a₁ holds
b₂ in dom a₁;

end;

:: deftheorem Def3 defines len-total COMPUT_1:def 3 :

definition

let c₁ be Relation;
attr a₁ is homogeneous means :Def4: :: COMPUT_1:def 4
for b₁, b₂ being FinSequence st b₁ in dom a₁ & b₂ in dom a₁ holds
len b₁ = len b₂;

end;

:: deftheorem Def4 defines homogeneous COMPUT_1:def 4 :

theorem Th19: :: COMPUT_1:19

for b₁ being Nat
for b₂ being non empty set
for b₃ being Relation st dom b₃ c= b₁ -tuples_on b₂ holds
b₃ is homogeneous

proof end;

registration

cluster {} -> homogeneous ;
coherence

proof end;

end;

registration

let c₁ be FinSequence;
let c₂ be set ;
cluster K256({a₁},a₂) -> non empty homogeneous ;
coherence

proof end;

end;

registration

cluster non empty homogeneous set ;
existence

proof end;

end;

registration

let c₁ be homogeneous Function;
let c₂ be Function;
cluster a₁ * a₂ -> homogeneous ;
coherence

proof end;

end;

registration

let c₁, c₂ be set ;
cluster homogeneous Relation of a₁ * ,a₂;
existence

proof end;

end;

registration

let c₁, c₂ be non empty set ;
cluster non empty homogeneous Relation of a₁ * ,a₂;
existence

proof end;

end;

registration

let c₁ be non empty set ;
cluster non empty quasi_total homogeneous Relation of a₁ * ,a₁;
existence

proof end;

end;

registration

cluster non empty to-naturals from-natural-fseqs len-total homogeneous set ;
existence

proof end;

end;

registration

cluster -> to-naturals from-natural-fseqs Relation of NAT * , NAT ;
coherence

proof end;

end;

registration

cluster quasi_total -> to-naturals from-natural-fseqs len-total Relation of NAT * , NAT ;
coherence

proof end;

end;

theorem Th20: :: COMPUT_1:20

for b₁ being to-naturals from-natural-fseqs len-total Function holds b₁ is quasi_total PartFunc of NAT * , NAT

proof end;

definition

let c₁ be homogeneous Relation;
func arity c₁ -> Nat means :Def5: :: COMPUT_1:def 5
for b₁ being FinSequence st b₁ in dom a₁ holds
a₂ = len b₁ if ex b₁ being FinSequence st b₁ in dom a₁
otherwise a₂ = 0;
existence

proof end;

uniqueness

proof end;

correctness ;

end;

:: deftheorem Def5 defines arity COMPUT_1:def 5 :

theorem Th21: :: COMPUT_1:21

arity {} = 0

proof end;

theorem Th22: :: COMPUT_1:22

for b₁ being homogeneous Relation st dom b₁ = {{} } holds
arity b₁ = 0

proof end;

theorem Th23: :: COMPUT_1:23

for b₁, b₂ being set
for b₃ being homogeneous PartFunc of b₁ * ,b₂ holds dom b₃ c= (arity b₃) -tuples_on b₁

proof end;

theorem Th24: :: COMPUT_1:24

for b₁ being from-natural-fseqs homogeneous Function holds dom b₁ c= (arity b₁) -tuples_on NAT

proof end;

Lemma26: for b₁ being non empty set
for b₂ being homogeneous PartFunc of b₁ * ,b₁ holds
( ( b₂ is quasi_total & not b₂ is empty ) iff dom b₂ = (arity b₂) -tuples_on b₁ )

proof end;

theorem Th25: :: COMPUT_1:25

for b₁ being set
for b₂ being homogeneous PartFunc of b₁ * ,b₁ holds
( ( b₂ is quasi_total & not b₂ is empty ) iff dom b₂ = (arity b₂) -tuples_on b₁ )

proof end;

theorem Th26: :: COMPUT_1:26

for b₁ being to-naturals from-natural-fseqs homogeneous Function holds
( ( b₁ is len-total & not b₁ is empty ) iff dom b₁ = (arity b₁) -tuples_on NAT )

proof end;

theorem Th27: :: COMPUT_1:27

for b₁ being non empty set
for b₂ being non empty homogeneous PartFunc of b₁ * ,b₁
for b₃ being Nat st dom b₂ c= b₃ -tuples_on b₁ holds
arity b₂ = b₃

proof end;

theorem Th28: :: COMPUT_1:28

for b₁ being non empty set
for b₂ being homogeneous PartFunc of b₁ * ,b₁
for b₃ being Nat st dom b₂ = b₃ -tuples_on b₁ holds
arity b₂ = b₃

proof end;

definition

let c₁ be Relation;
attr a₁ is with_the_same_arity means :Def6: :: COMPUT_1:def 6
for b₁, b₂ being Function st b₁ in rng a₁ & b₂ in rng a₁ holds
( ( not b₁ is empty or b₂ is empty or dom b₂ = {{} } ) & ( not b₁ is empty & not b₂ is empty implies ex b₃ being Natex b₄ being non empty set st
( dom b₁ c= b₃ -tuples_on b₄ & dom b₂ c= b₃ -tuples_on b₄ ) ) );

end;

:: deftheorem Def6 defines with_the_same_arity COMPUT_1:def 6 :

registration

cluster {} -> homogeneous with_the_same_arity ;
coherence

proof end;

end;

registration

cluster with_the_same_arity set ;
existence

proof end;

let c₁ be set ;
cluster with_the_same_arity FinSequence of a₁;
existence

proof end;

cluster with_the_same_arity Element of a₁ * ;
existence

proof end;

end;

definition

let c₁ be with_the_same_arity Relation;
func arity c₁ -> Nat means :Def7: :: COMPUT_1:def 7
for b₁ being homogeneous Function st b₁ in rng a₁ holds
a₂ = arity b₁ if ex b₁ being homogeneous Function st b₁ in rng a₁
otherwise a₂ = 0;
existence

proof end;

uniqueness

proof end;

correctness ;

end;

:: deftheorem Def7 defines arity COMPUT_1:def 7 :

theorem Th29: :: COMPUT_1:29

for b₁ being with_the_same_arity FinSequence st len b₁ = 0 holds
arity b₁ = 0

proof end;

definition

let c₁ be set ;
func HFuncs c₁ -> PFUNC_DOMAIN of a₁ * ,a₁ equals :: COMPUT_1:def 8
{ b₁ where B is Element of PFuncs (a₁ * ),a₁ : b₁ is homogeneous } ;
coherence

proof end;

end;

:: deftheorem Def8 defines HFuncs COMPUT_1:def 8 :

theorem Th30: :: COMPUT_1:30

for b₁ being set holds {} in HFuncs b₁

proof end;

registration

let c₁ be non empty set ;
cluster non empty quasi_total homogeneous Element of HFuncs a₁;
existence

proof end;

end;

registration

let c₁ be set ;
cluster -> homogeneous Element of HFuncs a₁;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be non empty Subset of (HFuncs c₁);
cluster -> homogeneous Element of a₂;
coherence

proof end;

end;

theorem Th31: :: COMPUT_1:31

for b₁ being to-naturals from-natural-fseqs homogeneous Function holds b₁ is Element of HFuncs NAT

proof end;

theorem Th32: :: COMPUT_1:32

for b₁ being to-naturals from-natural-fseqs len-total homogeneous Function holds b₁ is quasi_total Element of HFuncs NAT

proof end;

theorem Th33: :: COMPUT_1:33

for b₁ being non empty set
for b₂ being Relation st rng b₂ c= HFuncs b₁ & ( for b₃, b₄ being homogeneous Function st b₃ in rng b₂ & b₄ in rng b₂ holds
arity b₃ = arity b₄ ) holds
b₂ is with_the_same_arity

proof end;

definition

let c₁, c₂ be Nat;
func c₁ const c₂ -> to-naturals from-natural-fseqs homogeneous Function equals :: COMPUT_1:def 9
(a₁ -tuples_on NAT ) --> a₂;
coherence

proof end;

end;

:: deftheorem Def9 defines const COMPUT_1:def 9 :

theorem Th34: :: COMPUT_1:34

for b₁, b₂ being Nat holds b₁ const b₂ in HFuncs NAT

proof end;

registration

let c₁, c₂ be Nat;
cluster a₁ const a₂ -> non empty to-naturals from-natural-fseqs len-total homogeneous ;
coherence

proof end;

end;

theorem Th35: :: COMPUT_1:35

for b₁, b₂ being Nat holds arity (b₁ const b₂) = b₁

proof end;

theorem Th36: :: COMPUT_1:36

for b₁, b₂ being Nat
for b₃ being Element of b₁ -tuples_on NAT holds (b₁ const b₂) . b₃ = b₂ by FUNCOP_1:13;

definition

let c₁, c₂ be Nat;
func c₁ succ c₂ -> to-naturals from-natural-fseqs homogeneous Function means :Def10: :: COMPUT_1:def 10
( dom a₃ = a₁ -tuples_on NAT & ( for b₁ being Element of a₁ -tuples_on NAT holds a₃ . b₁ = (b₁ /. a₂) + 1 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines succ COMPUT_1:def 10 :

theorem Th37: :: COMPUT_1:37

for b₁, b₂ being Nat holds b₁ succ b₂ in HFuncs NAT

proof end;

registration

let c₁, c₂ be Nat;
cluster a₁ succ a₂ -> non empty to-naturals from-natural-fseqs len-total homogeneous ;
coherence

proof end;

end;

theorem Th38: :: COMPUT_1:38

for b₁, b₂ being Nat holds arity (b₁ succ b₂) = b₁

proof end;

definition

let c₁, c₂ be Nat;
func c₁ proj c₂ -> to-naturals from-natural-fseqs homogeneous Function equals :: COMPUT_1:def 11
proj (a₁ |-> NAT ),a₂;
correctness

proof end;

end;

:: deftheorem Def11 defines proj COMPUT_1:def 11 :

theorem Th39: :: COMPUT_1:39

for b₁, b₂ being Nat holds b₁ proj b₂ in HFuncs NAT

proof end;

theorem Th40: :: COMPUT_1:40

for b₁, b₂ being Nat holds
( dom (b₁ proj b₂) = b₁ -tuples_on NAT & ( 1 <= b₂ & b₂ <= b₁ implies rng (b₁ proj b₂) = NAT ) )

proof end;

registration

let c₁, c₂ be Nat;
cluster a₁ proj a₂ -> non empty to-naturals from-natural-fseqs len-total homogeneous ;
coherence

proof end;

end;

theorem Th41: :: COMPUT_1:41

for b₁, b₂ being Nat holds arity (b₁ proj b₂) = b₁

proof end;

theorem Th42: :: COMPUT_1:42

for b₁, b₂ being Nat
for b₃ being Element of b₁ -tuples_on NAT holds (b₁ proj b₂) . b₃ = b₃ . b₂

proof end;

registration

let c₁ be set ;
cluster HFuncs a₁ -> functional ;
coherence ;

end;

theorem Th43: :: COMPUT_1:43

for b₁ being Nat
for b₂, b₃ being non empty set
for b₄ being Function of b₂, HFuncs b₃ st rng b₄ is compatible & ( for b₅ being Element of b₂ holds dom (b₄ . b₅) c= b₁ -tuples_on b₃ ) holds
ex b₅ being Element of HFuncs b₃ st
( b₅ = Union b₄ & dom b₅ c= b₁ -tuples_on b₃ )

proof end;

theorem Th44: :: COMPUT_1:44

for b₁ being non empty set
for b₂ being Function of NAT , HFuncs b₁ st ( for b₃ being Nat holds b₂ . b₃ c= b₂ . (b₃ + 1) ) holds
Union b₂ in HFuncs b₁

proof end;

theorem Th45: :: COMPUT_1:45

for b₁ being non empty set
for b₂ being with_the_same_arity FinSequence of HFuncs b₁ holds dom <:b₂:> c= (arity b₂) -tuples_on b₁

proof end;

registration

let c₁ be non empty set ;
let c₂ be with_the_same_arity FinSequence of HFuncs c₁;
cluster <:a₂:> -> homogeneous ;
coherence

proof end;

end;

theorem Th46: :: COMPUT_1:46

for b₁ being non empty set
for b₂ being Element of HFuncs b₁
for b₃ being with_the_same_arity FinSequence of HFuncs b₁ holds
( dom (b₂ * <:b₃:>) c= (arity b₃) -tuples_on b₁ & rng (b₂ * <:b₃:>) c= b₁ & b₂ * <:b₃:> in HFuncs b₁ )

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be PFUNC_DOMAIN of c₁,c₂;
let c₄ be non empty Subset of c₃;
redefine mode Element as Element of c₄ -> Element of a₃;
coherence

proof end;

end;

registration

let c₁ be from-natural-fseqs homogeneous Function;
cluster <*a₁*> -> with_the_same_arity ;
coherence

proof end;

end;

theorem Th47: :: COMPUT_1:47

for b₁ being to-naturals from-natural-fseqs homogeneous Function holds arity <*b₁*> = arity b₁

proof end;

theorem Th48: :: COMPUT_1:48

for b₁, b₂ being non empty Element of HFuncs NAT
for b₃ being with_the_same_arity FinSequence of HFuncs NAT st b₂ = b₁ * <:b₃:> holds
arity b₂ = arity b₃

proof end;

theorem Th49: :: COMPUT_1:49

for b₁ being non empty set
for b₂ being non empty quasi_total Element of HFuncs b₁
for b₃ being with_the_same_arity FinSequence of HFuncs b₁ st arity b₂ = len b₃ & not b₃ is empty & ( for b₄ being Element of HFuncs b₁ st b₄ in rng b₃ holds
( b₄ is quasi_total & not b₄ is empty ) ) holds
( b₂ * <:b₃:> is non empty quasi_total Element of HFuncs b₁ & dom (b₂ * <:b₃:>) = (arity b₃) -tuples_on b₁ )

proof end;

theorem Th50: :: COMPUT_1:50

for b₁ being non empty set
for b₂ being quasi_total Element of HFuncs b₁
for b₃ being with_the_same_arity FinSequence of HFuncs b₁ st arity b₂ = len b₃ & ( for b₄ being Element of HFuncs b₁ st b₄ in rng b₃ holds
b₄ is quasi_total ) holds
b₂ * <:b₃:> is quasi_total Element of HFuncs b₁

proof end;

theorem Th51: :: COMPUT_1:51

for b₁ being non empty set
for b₂, b₃ being non empty quasi_total Element of HFuncs b₁ st arity b₂ = 0 & arity b₃ = 0 & b₂ . {} = b₃ . {} holds
b₂ = b₃

proof end;

theorem Th52: :: COMPUT_1:52

for b₁, b₂ being non empty to-naturals from-natural-fseqs len-total homogeneous Function st arity b₁ = 0 & arity b₂ = 0 & b₁ . {} = b₂ . {} holds
b₁ = b₂

proof end;

definition

let c₁, c₂, c₃ be to-naturals from-natural-fseqs homogeneous Function;
let c₄ be Nat;
pred c₁ is_primitive-recursively_expressed_by c₂,c₃,c₄ means :Def12: :: COMPUT_1:def 12
ex b₁ being Nat st
( dom a₁ c= b₁ -tuples_on NAT & a₄ >= 1 & a₄ <= b₁ & (arity a₂) + 1 = b₁ & b₁ + 1 = arity a₃ & ( for b₂ being FinSequence of NAT st len b₂ = b₁ holds
( ( b₂ +* a₄,0 in dom a₁ implies Del b₂,a₄ in dom a₂ ) & ( Del b₂,a₄ in dom a₂ implies b₂ +* a₄,0 in dom a₁ ) & ( b₂ +* a₄,0 in dom a₁ implies a₁ . (b₂ +* a₄,0) = a₂ . (Del b₂,a₄) ) & ( for b₃ being Nat holds
( ( b₂ +* a₄,(b₃ + 1) in dom a₁ implies ( b₂ +* a₄,b₃ in dom a₁ & (b₂ +* a₄,b₃) ^ <*(a₁ . (b₂ +* a₄,b₃))*> in dom a₃ ) ) & ( b₂ +* a₄,b₃ in dom a₁ & (b₂ +* a₄,b₃) ^ <*(a₁ . (b₂ +* a₄,b₃))*> in dom a₃ implies b₂ +* a₄,(b₃ + 1) in dom a₁ ) & ( b₂ +* a₄,(b₃ + 1) in dom a₁ implies a₁ . (b₂ +* a₄,(b₃ + 1)) = a₃ . ((b₂ +* a₄,b₃) ^ <*(a₁ . (b₂ +* a₄,b₃))*>) ) ) ) ) ) );

end;

:: deftheorem Def12 defines is_primitive-recursively_expressed_by COMPUT_1:def 12 :

defpred S₁[ Nat, Element of HFuncs NAT , Element of HFuncs NAT , FinSequence of NAT , Nat, homogeneous Function] means ( ( a₅ in dom a₄ & a₄ +* a₅,a₁ in dom a₂ & (a₄ +* a₅,a₁) ^ <*(a₂ . (a₄ +* a₅,a₁))*> in dom a₆ implies a₃ = a₂ +* ({(a₄ +* a₅,(a₁ + 1))} --> (a₆ . ((a₄ +* a₅,a₁) ^ <*(a₂ . (a₄ +* a₅,a₁))*>))) ) & ( ( not a₅ in dom a₄ or not a₄ +* a₅,a₁ in dom a₂ or not (a₄ +* a₅,a₁) ^ <*(a₂ . (a₄ +* a₅,a₁))*> in dom a₆ ) implies a₃ = a₂ ) );

definition

let c₁, c₂ be to-naturals from-natural-fseqs homogeneous Function;
let c₃ be Nat;
let c₄ be FinSequence of NAT ;
func primrec c₁,c₂,c₃,c₄ -> Element of HFuncs NAT means :Def13: :: COMPUT_1:def 13
ex b₁ being Function of NAT , HFuncs NAT st
( a₅ = b₁ . (a₄ /. a₃) & ( a₃ in dom a₄ & Del a₄,a₃ in dom a₁ implies b₁ . 0 = {(a₄ +* a₃,0)} --> (a₁ . (Del a₄,a₃)) ) & ( ( not a₃ in dom a₄ or not Del a₄,a₃ in dom a₁ ) implies b₁ . 0 = {} ) & ( for b₂ being Nat holds
( ( a₃ in dom a₄ & a₄ +* a₃,b₂ in dom (b₁ . b₂) & (a₄ +* a₃,b₂) ^ <*((b₁ . b₂) . (a₄ +* a₃,b₂))*> in dom a₂ implies b₁ . (b₂ + 1) = (b₁ . b₂) +* ({(a₄ +* a₃,(b₂ + 1))} --> (a₂ . ((a₄ +* a₃,b₂) ^ <*((b₁ . b₂) . (a₄ +* a₃,b₂))*>))) ) & ( ( not a₃ in dom a₄ or not a₄ +* a₃,b₂ in dom (b₁ . b₂) or not (a₄ +* a₃,b₂) ^ <*((b₁ . b₂) . (a₄ +* a₃,b₂))*> in dom a₂ ) implies b₁ . (b₂ + 1) = b₁ . b₂ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines primrec COMPUT_1:def 13 :

theorem Th53: :: COMPUT_1:53

for b₁ being Nat
for b₂, b₃ being to-naturals from-natural-fseqs homogeneous Function
for b₄, b₅ being FinSequence of NAT st b₅ in dom (primrec b₂,b₃,b₁,b₄) holds
ex b₆ being Nat st b₅ = b₄ +* b₁,b₆

proof end;

theorem Th54: :: COMPUT_1:54

for b₁ being Nat
for b₂, b₃ being to-naturals from-natural-fseqs homogeneous Function
for b₄ being FinSequence of NAT st not b₁ in dom b₄ holds
primrec b₂,b₃,b₁,b₄ = {}

proof end;

theorem Th55: :: COMPUT_1:55

for b₁ being Nat
for b₂, b₃ being to-naturals from-natural-fseqs homogeneous Function
for b₄, b₅ being FinSequence of NAT holds primrec b₂,b₃,b₁,b₄ tolerates primrec b₂,b₃,b₁,b₅

proof end;

theorem Th56: :: COMPUT_1:56

for b₁ being Nat
for b₂, b₃ being to-naturals from-natural-fseqs homogeneous Function
for b₄ being FinSequence of NAT holds dom (primrec b₂,b₃,b₁,b₄) c= (1 + (arity b₂)) -tuples_on NAT

proof end;

theorem Th57: :: COMPUT_1:57

for b₁ being Nat
for b₂, b₃ being to-naturals from-natural-fseqs homogeneous Function
for b₄ being FinSequence of NAT st b₂ is empty holds
primrec b₂,b₃,b₁,b₄ is empty

proof end;

theorem Th58: :: COMPUT_1:58

for b₁ being Nat
for b₂, b₃ being non empty to-naturals from-natural-fseqs homogeneous Function
for b₄ being Element of ((arity b₂) + 1) -tuples_on NAT st b₂ is len-total & b₃ is len-total & (arity b₂) + 2 = arity b₃ & 1 <= b₁ & b₁ <= 1 + (arity b₂) holds
b₄ in dom (primrec b₂,b₃,b₁,b₄)

proof end;

definition

let c₁, c₂ be to-naturals from-natural-fseqs homogeneous Function;
let c₃ be Nat;
func primrec c₁,c₂,c₃ -> Element of HFuncs NAT means :Def14: :: COMPUT_1:def 14
ex b₁ being Function of ((arity a₁) + 1) -tuples_on NAT , HFuncs NAT st
( a₄ = Union b₁ & ( for b₂ being Element of ((arity a₁) + 1) -tuples_on NAT holds b₁ . b₂ = primrec a₁,a₂,a₃,b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines primrec COMPUT_1:def 14 :

theorem Th59: :: COMPUT_1:59

for b₁ being Nat
for b₂, b₃ being to-naturals from-natural-fseqs homogeneous Function st b₂ is empty holds
primrec b₂,b₃,b₁ is empty

proof end;

theorem Th60: :: COMPUT_1:60

for b₁ being Nat
for b₂, b₃ being non empty to-naturals from-natural-fseqs homogeneous Function holds dom (primrec b₂,b₃,b₁) c= ((arity b₂) + 1) -tuples_on NAT

proof end;

theorem Th61: :: COMPUT_1:61

for b₁ being Nat
for b₂, b₃ being non empty to-naturals from-natural-fseqs homogeneous Function st b₂ is len-total & b₃ is len-total & (arity b₂) + 2 = arity b₃ & 1 <= b₁ & b₁ <= 1 + (arity b₂) holds
( dom (primrec b₂,b₃,b₁) = ((arity b₂) + 1) -tuples_on NAT & arity (primrec b₂,b₃,b₁) = (arity b₂) + 1 )

proof end;

E66: now

let c₁, c₂ be non empty to-naturals from-natural-fseqs homogeneous Function;
let c₃ be Element of ((arity c₁) + 1) -tuples_on NAT ;
let c₄, c₅ be Nat;
set c₆ = c₃ +* c₄,(c₅ + 1);
set c₇ = c₃ +* c₄,c₅;
let c₈, c₉ be Function of NAT , HFuncs NAT ;
assume that
E67: ( ( c₄ in dom (c₃ +* c₄,(c₅ + 1)) & Del (c₃ +* c₄,(c₅ + 1)),c₄ in dom c₁ implies c₈ . 0 = {((c₃ +* c₄,(c₅ + 1)) +* c₄,0)} --> (c₁ . (Del (c₃ +* c₄,(c₅ + 1)),c₄)) ) & ( ( not c₄ in dom (c₃ +* c₄,(c₅ + 1)) or not Del (c₃ +* c₄,(c₅ + 1)),c₄ in dom c₁ ) implies c₈ . 0 = {} ) ) and
E68: for b₁ being Nat holds S₁[b₁,c₈ . b₁,c₈ . (b₁ + 1),c₃ +* c₄,(c₅ + 1),c₄,c₂] and
E69: ( ( c₄ in dom (c₃ +* c₄,c₅) & Del (c₃ +* c₄,c₅),c₄ in dom c₁ implies c₉ . 0 = {((c₃ +* c₄,c₅) +* c₄,0)} --> (c₁ . (Del (c₃ +* c₄,c₅),c₄)) ) & ( ( not c₄ in dom (c₃ +* c₄,c₅) or not Del (c₃ +* c₄,c₅),c₄ in dom c₁ ) implies c₉ . 0 = {} ) ) and
E70: for b₁ being Nat holds S₁[b₁,c₉ . b₁,c₉ . (b₁ + 1),c₃ +* c₄,c₅,c₄,c₂] ;
E71: ( dom c₃ = dom (c₃ +* c₄,c₅) & dom c₃ = dom (c₃ +* c₄,(c₅ + 1)) ) by FUNCT_7:32;
E72: (c₃ +* c₄,c₅) +* c₄,0 = c₃ +* c₄,0 by FUNCT_7:36
.= (c₃ +* c₄,(c₅ + 1)) +* c₄,0 by FUNCT_7:36 ;
E73: Del (c₃ +* c₄,c₅),c₄ = Del c₃,c₄ by Th6
.= Del (c₃ +* c₄,(c₅ + 1)),c₄ by Th6 ;
for b₁ being set st b₁ in NAT holds
c₉ . b₁ = c₈ . b₁

proof

defpred S₂[ Nat] means c₉ . a₁ = c₈ . a₁;
E74: S₂[0] by E67, E69, E71, E72, E73;
E75: for b₁ being Nat st S₂[b₁] holds
S₂[b₁ + 1]

proof

let c₁₀ be Nat;
assume E76: S₂[c₁₀] ;
E77: (c₃ +* c₄,c₅) +* c₄,c₁₀ = c₃ +* c₄,c₁₀ by FUNCT_7:36
.= (c₃ +* c₄,(c₅ + 1)) +* c₄,c₁₀ by FUNCT_7:36 ;
E78: (c₃ +* c₄,c₅) +* c₄,(c₁₀ + 1) = c₃ +* c₄,(c₁₀ + 1) by FUNCT_7:36
.= (c₃ +* c₄,(c₅ + 1)) +* c₄,(c₁₀ + 1) by FUNCT_7:36 ;

per cases ;

suppose E79: ( c₄ in dom (c₃ +* c₄,c₅) & (c₃ +* c₄,c₅) +* c₄,c₁₀ in dom (c₉ . c₁₀) & ((c₃ +* c₄,c₅) +* c₄,c₁₀) ^ <*((c₉ . c₁₀) . ((c₃ +* c₄,c₅) +* c₄,c₁₀))*> in dom c₂ ) ;

hence c₉ . (c₁₀ + 1) = (c₉ . c₁₀) +* ({((c₃ +* c₄,c₅) +* c₄,(c₁₀ + 1))} --> (c₂ . (((c₃ +* c₄,c₅) +* c₄,c₁₀) ^ <*((c₉ . c₁₀) . ((c₃ +* c₄,c₅) +* c₄,c₁₀))*>))) by E70
.= c₈ . (c₁₀ + 1) by E68, E71, E76, E77, E78, E79 ;

end;

suppose E79: ( not c₄ in dom (c₃ +* c₄,c₅) or not (c₃ +* c₄,c₅) +* c₄,c₁₀ in dom (c₉ . c₁₀) or not ((c₃ +* c₄,c₅) +* c₄,c₁₀) ^ <*((c₉ . c₁₀) . ((c₃ +* c₄,c₅) +* c₄,c₁₀))*> in dom c₂ ) ;

hence c₉ . (c₁₀ + 1) = c₉ . c₁₀ by E70
.= c₈ . (c₁₀ + 1) by E68, E71, E76, E77, E79 ;

end;

E76: for b₁ being Nat holds S₂[b₁] from NAT_1:sch 1(E74, E75);
let c₁₀ be set ;
assume c₁₀ in NAT ;
hence c₉ . c₁₀ = c₈ . c₁₀ by E76;

end;

hence c₈ = c₉ by FUNCT_2:18;

end;

E67: now

let c₁, c₂ be non empty to-naturals from-natural-fseqs homogeneous Function;
let c₃ be Element of ((arity c₁) + 1) -tuples_on NAT ;
let c₄, c₅ be Nat;
assume E68: c₄ in dom c₃ ;
set c₆ = c₃ +* c₄,c₅;
set c₇ = c₃ +* c₄,(c₅ + 1);
let c₈ be Function of NAT , HFuncs NAT ;
assume that
E69: ( ( c₄ in dom (c₃ +* c₄,(c₅ + 1)) & Del (c₃ +* c₄,(c₅ + 1)),c₄ in dom c₁ implies c₈ . 0 = {((c₃ +* c₄,(c₅ + 1)) +* c₄,0)} --> (c₁ . (Del (c₃ +* c₄,(c₅ + 1)),c₄)) ) & ( ( not c₄ in dom (c₃ +* c₄,(c₅ + 1)) or not Del (c₃ +* c₄,(c₅ + 1)),c₄ in dom c₁ ) implies c₈ . 0 = {} ) ) and
E70: for b₁ being Nat holds S₁[b₁,c₈ . b₁,c₈ . (b₁ + 1),c₃ +* c₄,(c₅ + 1),c₄,c₂] ;
thus (c₈ . (c₅ + 1)) . (c₃ +* c₄,c₅) = (c₈ . c₅) . (c₃ +* c₄,c₅)

proof

per cases ;

suppose ( c₄ in dom (c₃ +* c₄,(c₅ + 1)) & (c₃ +* c₄,(c₅ + 1)) +* c₄,c₅ in dom (c₈ . c₅) & ((c₃ +* c₄,(c₅ + 1)) +* c₄,c₅) ^ <*((c₈ . c₅) . ((c₃ +* c₄,(c₅ + 1)) +* c₄,c₅))*> in dom c₂ ) ;

then E71: c₈ . (c₅ + 1) = (c₈ . c₅) +* ({((c₃ +* c₄,(c₅ + 1)) +* c₄,(c₅ + 1))} --> (c₂ . (((c₃ +* c₄,(c₅ + 1)) +* c₄,c₅) ^ <*((c₈ . c₅) . ((c₃ +* c₄,(c₅ + 1)) +* c₄,c₅))*>))) by E70;
( (c₃ +* c₄,c₅) . c₄ = c₅ & (c₃ +* c₄,(c₅ + 1)) . c₄ = c₅ + 1 ) by E68, FUNCT_7:33;
then ( c₃ +* c₄,c₅ <> c₃ +* c₄,(c₅ + 1) & c₃ +* c₄,(c₅ + 1) = (c₃ +* c₄,(c₅ + 1)) +* c₄,(c₅ + 1) ) by FUNCT_7:36;
then not c₃ +* c₄,c₅ in {((c₃ +* c₄,(c₅ + 1)) +* c₄,(c₅ + 1))} by TARSKI:def 1;
then not c₃ +* c₄,c₅ in dom ({((c₃ +* c₄,(c₅ + 1)) +* c₄,(c₅ + 1))} --> (c₂ . (((c₃ +* c₄,(c₅ + 1)) +* c₄,c₅) ^ <*((c₈ . c₅) . ((c₃ +* c₄,(c₅ + 1)) +* c₄,c₅))*>))) by FUNCOP_1:19;
hence (c₈ . (c₅ + 1)) . (c₃ +* c₄,c₅) = (c₈ . c₅) . (c₃ +* c₄,c₅) by E71, FUNCT_4:12;

end;

suppose ( not c₄ in dom (c₃ +* c₄,(c₅ + 1)) or not (c₃ +* c₄,(c₅ + 1)) +* c₄,c₅ in dom (c₈ . c₅) or not ((c₃ +* c₄,(c₅ + 1)) +* c₄,c₅) ^ <*((c₈ . c₅) . ((c₃ +* c₄,(c₅ + 1)) +* c₄,c₅))*> in dom c₂ ) ;

hence (c₈ . (c₅ + 1)) . (c₃ +* c₄,c₅) = (c₈ . c₅) . (c₃ +* c₄,c₅) by E70;

end;

E71: for b₁, b₂ being Nat st c₃ +* c₄,b₂ in dom (c₈ . b₁) holds
b₂ <= b₁

proof

defpred S₂[ Nat] means for b₁ being Nat st c₃ +* c₄,b₁ in dom (c₈ . a₁) holds
b₁ <= a₁;
E72: S₂[0]

proof

let c₉ be Nat;
assume E73: c₃ +* c₄,c₉ in dom (c₈ . 0) ;

per cases ;

suppose ( c₄ in dom (c₃ +* c₄,(c₅ + 1)) & Del (c₃ +* c₄,(c₅ + 1)),c₄ in dom c₁ ) ;

then dom (c₈ . 0) = {((c₃ +* c₄,(c₅ + 1)) +* c₄,0)} by E69, FUNCOP_1:19;
then E74: c₃ +* c₄,c₉ = (c₃ +* c₄,(c₅ + 1)) +* c₄,0 by E73, TARSKI:def 1
.= c₃ +* c₄,0 by FUNCT_7:36 ;
c₉ = (c₃ +* c₄,c₉) . c₄ by E68, FUNCT_7:33
.= 0 by E68, E74, FUNCT_7:33 ;
hence c₉ <= 0 ;

end;

suppose ( not c₄ in dom (c₃ +* c₄,(c₅ + 1)) or not Del (c₃ +* c₄,(c₅ + 1)),c₄ in dom c₁ ) ;

hence c₉ <= 0 by E69, E73, RELAT_1:60;

end;

E73: for b₁ being Nat st S₂[b₁] holds
S₂[b₁ + 1]

proof

let c₉ be Nat;
assume E74: S₂[c₉] ;
let c₁₀ be Nat;
assume E75: c₃ +* c₄,c₁₀ in dom (c₈ . (c₉ + 1)) ;

per cases ;

suppose ( c₄ in dom (c₃ +* c₄,(c₅ + 1)) & (c₃ +* c₄,(c₅ + 1)) +* c₄,c₉ in dom (c₈ . c₉) & ((c₃ +* c₄,(c₅ + 1)) +* c₄,c₉) ^ <*((c₈ . c₉) . ((c₃ +* c₄,(c₅ + 1)) +* c₄,c₉))*> in dom c₂ ) ;

then c₈ . (c₉ + 1) = (c₈ . c₉) +* ({((c₃ +* c₄,(c₅ + 1)) +* c₄,(c₉ + 1))} --> (c₂ . (((c₃ +* c₄,(c₅ + 1)) +* c₄,c₉) ^ <*((c₈ . c₉) . ((c₃ +* c₄,(c₅ + 1)) +* c₄,c₉))*>))) by E70;
then dom (c₈ . (c₉ + 1)) = (dom (c₈ . c₉)) \/ (dom ({((c₃ +* c₄,(c₅ + 1)) +* c₄,(c₉ + 1))} --> (c₂ . (((c₃ +* c₄,(c₅ + 1)) +* c₄,c₉) ^ <*((c₈ . c₉) . ((c₃ +* c₄,(c₅ + 1)) +* c₄,c₉))*>)))) by FUNCT_4:def 1;
then E76: dom (c₈ . (c₉ + 1)) = (dom (c₈ . c₉)) \/ {((c₃ +* c₄,(c₅ + 1)) +* c₄,(c₉ + 1))} by FUNCOP_1:19;
thus c₁₀ <= c₉ + 1

proof

per cases by E75, E76, XBOOLE_0:def 2;

suppose c₃ +* c₄,c₁₀ in dom (c₈ . c₉) ;

then ( c₁₀ <= c₉ & c₉ <= c₉ + 1 ) by E74, NAT_1:29;
hence c₁₀ <= c₉ + 1 by XREAL_1:2;

end;

suppose c₃ +* c₄,c₁₀ in {((c₃ +* c₄,(c₅ + 1)) +* c₄,(c₉ + 1))} ;

then E77: c₃ +* c₄,c₁₀ = (c₃ +* c₄,(c₅ + 1)) +* c₄,(c₉ + 1) by TARSKI:def 1
.= c₃ +* c₄,(c₉ + 1) by FUNCT_7:36 ;
c₁₀ = (c₃ +* c₄,c₁₀) . c₄ by E68, FUNCT_7:33
.= c₉ + 1 by E68, E77, FUNCT_7:33 ;
hence c₁₀ <= c₉ + 1 ;

end;

suppose ( not c₄ in dom (c₃ +* c₄,(c₅ + 1)) or not (c₃ +* c₄,(c₅ + 1)) +* c₄,c₉ in dom (c₈ . c₉) or not ((c₃ +* c₄,(c₅ + 1)) +* c₄,c₉) ^ <*((c₈ . c₉) . ((c₃ +* c₄,(c₅ + 1)) +* c₄,c₉))*> in dom c₂ ) ;

then c₈ . (c₉ + 1) = c₈ . c₉ by E70;
then ( c₁₀ <= c₉ & c₉ <= c₉ + 1 ) by E74, E75, NAT_1:29;
hence c₁₀ <= c₉ + 1 by XREAL_1:2;

end;

thus for b₁ being Nat holds S₂[b₁] from NAT_1:sch 1(E72, E73);

end;

thus not c₃ +* c₄,(c₅ + 1) in dom (c₈ . c₅)

proof

assume c₃ +* c₄,(c₅ + 1) in dom (c₈ . c₅) ;
then c₅ + 1 <= c₅ by E71;
hence contradiction by NAT_1:38;

end;

E68: now

let c₁, c₂ be non empty to-naturals from-natural-fseqs homogeneous Function;
let c₃ be Element of ((arity c₁) + 1) -tuples_on NAT ;
let c₄, c₅ be Nat;
assume E69: c₄ in dom c₃ ;
let c₆ be Function of ((arity c₁) + 1) -tuples_on NAT , HFuncs NAT ;
assume E70: for b₁ being Element of ((arity c₁) + 1) -tuples_on NAT holds c₆ . b₁ = primrec c₁,c₂,c₄,b₁ ;
thus for b₁, b₂ being Nat holds dom (c₆ . (c₃ +* c₄,b₁)) c= dom (c₆ . (c₃ +* c₄,(b₁ + b₂)))

proof

let c₇ be Nat;
set c₈ = c₃ +* c₄,c₇;
defpred S₂[ Nat] means dom (c₆ . (c₃ +* c₄,c₇)) c= dom (c₆ . (c₃ +* c₄,(c₇ + a₁)));
E71: S₂[0] ;

E72: now

let c₉ be Nat;
assume E73: S₂[c₉] ;
set c₁₀ = c₃ +* c₄,(c₇ + c₉);
set c₁₁ = c₃ +* c₄,((c₇ + c₉) + 1);
set c₁₂ = c₇ + c₉;
consider c₁₃ being Function of NAT , HFuncs NAT such that
E74: primrec c₁,c₂,c₄,(c₃ +* c₄,(c₇ + c₉)) = c₁₃ . ((c₃ +* c₄,(c₇ + c₉)) /. c₄) and
E75: ( ( c₄ in dom (c₃ +* c₄,(c₇ + c₉)) & Del (c₃ +* c₄,(c₇ + c₉)),c₄ in dom c₁ implies c₁₃ . 0 = {((c₃ +* c₄,(c₇ + c₉)) +* c₄,0)} --> (c₁ . (Del (c₃ +* c₄,(c₇ + c₉)),c₄)) ) & ( ( not c₄ in dom (c₃ +* c₄,(c₇ + c₉)) or not Del (c₃ +* c₄,(c₇ + c₉)),c₄ in dom c₁ ) implies c₁₃ . 0 = {} ) ) and
E76: for b₁ being Nat holds S₁[b₁,c₁₃ . b₁,c₁₃ . (b₁ + 1),c₃ +* c₄,(c₇ + c₉),c₄,c₂] by Def13;
consider c₁₄ being Function of NAT , HFuncs NAT such that
E77: primrec c₁,c₂,c₄,(c₃ +* c₄,((c₇ + c₉) + 1)) = c₁₄ . ((c₃ +* c₄,((c₇ + c₉) + 1)) /. c₄) and
E78: ( ( c₄ in dom (c₃ +* c₄,((c₇ + c₉) + 1)) & Del (c₃ +* c₄,((c₇ + c₉) + 1)),c₄ in dom c₁ implies c₁₄ . 0 = {((c₃ +* c₄,((c₇ + c₉) + 1)) +* c₄,0)} --> (c₁ . (Del (c₃ +* c₄,((c₇ + c₉) + 1)),c₄)) ) & ( ( not c₄ in dom (c₃ +* c₄,((c₇ + c₉) + 1)) or not Del (c₃ +* c₄,((c₇ + c₉) + 1)),c₄ in dom c₁ ) implies c₁₄ . 0 = {} ) ) and
E79: for b₁ being Nat holds S₁[b₁,c₁₄ . b₁,c₁₄ . (b₁ + 1),c₃ +* c₄,((c₇ + c₉) + 1),c₄,c₂] by Def13;
E80: c₁₄ = c₁₃ by E75, E76, E78, E79, Lemma66;
E81: ( dom c₃ = dom (c₃ +* c₄,c₇) & dom c₃ = dom (c₃ +* c₄,((c₇ + c₉) + 1)) & dom c₃ = dom (c₃ +* c₄,(c₇ + c₉)) ) by FUNCT_7:32;
then E82: (c₃ +* c₄,((c₇ + c₉) + 1)) /. c₄ = (c₃ +* c₄,((c₇ + c₉) + 1)) . c₄ by E69, FINSEQ_4:def 4
.= (c₇ + c₉) + 1 by E69, FUNCT_7:33 ;
E83: (c₃ +* c₄,(c₇ + c₉)) /. c₄ = (c₃ +* c₄,(c₇ + c₉)) . c₄ by E69, E81, FINSEQ_4:def 4
.= c₇ + c₉ by E69, FUNCT_7:33 ;
E84: c₆ . (c₃ +* c₄,(c₇ + (c₉ + 1))) = c₁₃ . ((c₇ + c₉) + 1) by E70, E77, E80, E82;
E85: c₆ . (c₃ +* c₄,(c₇ + c₉)) = c₁₃ . (c₇ + c₉) by E70, E74, E83;

per cases ;

suppose ( c₄ in dom (c₃ +* c₄,(c₇ + c₉)) & (c₃ +* c₄,(c₇ + c₉)) +* c₄,(c₇ + c₉) in dom (c₁₃ . (c₇ + c₉)) & ((c₃ +* c₄,(c₇ + c₉)) +* c₄,(c₇ + c₉)) ^ <*((c₁₃ . (c₇ + c₉)) . ((c₃ +* c₄,(c₇ + c₉)) +* c₄,(c₇ + c₉)))*> in dom c₂ ) ;

end;

suppose ( not c₄ in dom (c₃ +* c₄,(c₇ + c₉)) or not (c₃ +* c₄,(c₇ + c₉)) +* c₄,(c₇ + c₉) in dom (c₁₃ . (c₇ + c₉)) or not ((c₃ +* c₄,(c₇ + c₉)) +* c₄,(c₇ + c₉)) ^ <*((c₁₃ . (c₇ + c₉)) . ((c₃ +* c₄,(c₇ + c₉)) +* c₄,(c₇ + c₉)))*> in dom c₂ ) ;

hence S₂[c₉ + 1] by E73, E76, E84, E85;

end;

thus for b₁ being Nat holds S₂[b₁] from NAT_1:sch 1(E71, E72);

end;

E69: now

let c₁, c₂ be non empty to-naturals from-natural-fseqs homogeneous Function;
let c₃ be Element of ((arity c₁) + 1) -tuples_on NAT ;
let c₄, c₅ be Nat;
assume E70: c₄ in dom c₃ ;
let c₆ be Function of ((arity c₁) + 1) -tuples_on NAT , HFuncs NAT ;
assume E71: for b₁ being Element of ((arity c₁) + 1) -tuples_on NAT holds c₆ . b₁ = primrec c₁,c₂,c₄,b₁ ;
thus for b₁, b₂ being Nat st not c₃ +* c₄,b₁ in dom (c₆ . (c₃ +* c₄,b₁)) holds
not c₃ +* c₄,b₁ in dom (c₆ . (c₃ +* c₄,(b₁ + b₂)))

proof

let c₇ be Nat;
set c₈ = c₃ +* c₄,c₇;
defpred S₂[ Nat] means ( not c₃ +* c₄,c₇ in dom (c₆ . (c₃ +* c₄,c₇)) implies not c₃ +* c₄,c₇ in dom (c₆ . (c₃ +* c₄,(c₇ + a₁))) );
E72: S₂[0] ;
E73: for b₁ being Nat st S₂[b₁] holds
S₂[b₁ + 1]

proof

let c₉ be Nat;
assume that
E74: S₂[c₉] and
E75: not c₃ +* c₄,c₇ in dom (c₆ . (c₃ +* c₄,c₇)) ;
set c₁₀ = c₃ +* c₄,(c₇ + c₉);
set c₁₁ = c₃ +* c₄,((c₇ + c₉) + 1);
set c₁₂ = c₇ + c₉;
consider c₁₃ being Function of NAT , HFuncs NAT such that
E76: primrec c₁,c₂,c₄,(c₃ +* c₄,(c₇ + c₉)) = c₁₃ . ((c₃ +* c₄,(c₇ + c₉)) /. c₄) and
E77: ( ( c₄ in dom (c₃ +* c₄,(c₇ + c₉)) & Del (c₃ +* c₄,(c₇ + c₉)),c₄ in dom c₁ implies c₁₃ . 0 = {((c₃ +* c₄,(c₇ + c₉)) +* c₄,0)} --> (c₁ . (Del (c₃ +* c₄,(c₇ + c₉)),c₄)) ) & ( ( not c₄ in dom (c₃ +* c₄,(c₇ + c₉)) or not Del (c₃ +* c₄,(c₇ + c₉)),c₄ in dom c₁ ) implies c₁₃ . 0 = {} ) ) and
E78: for b₁ being Nat holds S₁[b₁,c₁₃ . b₁,c₁₃ . (b₁ + 1),c₃ +* c₄,(c₇ + c₉),c₄,c₂] by Def13;
consider c₁₄ being Function of NAT , HFuncs NAT such that
E79: primrec c₁,c₂,c₄,(c₃ +* c₄,((c₇ + c₉) + 1)) = c₁₄ . ((c₃ +* c₄,((c₇ + c₉) + 1)) /. c₄) and
E80: ( ( c₄ in dom (c₃ +* c₄,((c₇ + c₉) + 1)) & Del (c₃ +* c₄,((c₇ + c₉) + 1)),c₄ in dom c₁ implies c₁₄ . 0 = {((c₃ +* c₄,((c₇ + c₉) + 1)) +* c₄,0)} --> (c₁ . (Del (c₃ +* c₄,((c₇ + c₉) + 1)),c₄)) ) & ( ( not c₄ in dom (c₃ +* c₄,((c₇ + c₉) + 1)) or not Del (c₃ +* c₄,((c₇ + c₉) + 1)),c₄ in dom c₁ ) implies c₁₄ . 0 = {} ) ) and
E81: for b₁ being Nat holds S₁[b₁,c₁₄ . b₁,c₁₄ . (b₁ + 1),c₃ +* c₄,((c₇ + c₉) + 1),c₄,c₂] by Def13;
E82: c₁₄ = c₁₃ by E77, E78, E80, E81, Lemma66;
E83: ( dom c₃ = dom (c₃ +* c₄,c₇) & dom c₃ = dom (c₃ +* c₄,((c₇ + c₉) + 1)) & dom c₃ = dom (c₃ +* c₄,(c₇ + c₉)) ) by FUNCT_7:32;
then E84: (c₃ +* c₄,((c₇ + c₉) + 1)) /. c₄ = (c₃ +* c₄,((c₇ + c₉) + 1)) . c₄ by E70, FINSEQ_4:def 4
.= (c₇ + c₉) + 1 by E70, FUNCT_7:33 ;
(c₃ +* c₄,(c₇ + c₉)) /. c₄ = (c₃ +* c₄,(c₇ + c₉)) . c₄ by E70, E83, FINSEQ_4:def 4
.= c₇ + c₉ by E70, FUNCT_7:33 ;
then E85: not c₃ +* c₄,c₇ in dom (c₁₃ . (c₇ + c₉)) by E71, E74, E75, E76;
E86: c₆ . (c₃ +* c₄,(c₇ + (c₉ + 1))) = c₁₃ . ((c₇ + c₉) + 1) by E71, E79, E82, E84;

per cases ;

then c₁₃ . ((c₇ + c₉) + 1) = (c₁₃ . (c₇ + c₉)) +* ({((c₃ +* c₄,(c₇ + c₉)) +* c₄,((c₇ + c₉) + 1))} --> (c₂ . (((c₃ +* c₄,(c₇ + c₉)) +* c₄,(c₇ + c₉)) ^ <*((c₁₃ . (c₇ + c₉)) . ((c₃ +* c₄,(c₇ + c₉)) +* c₄,(c₇ + c₉)))*>))) by E78;
then dom (c₁₃ . ((c₇ + c₉) + 1)) = (dom (c₁₃ . (c₇ + c₉))) \/ (dom ({((c₃ +* c₄,(c₇ + c₉)) +* c₄,((c₇ + c₉) + 1))} --> (c₂ . (((c₃ +* c₄,(c₇ + c₉)) +* c₄,(c₇ + c₉)) ^ <*((c₁₃ . (c₇ + c₉)) . ((c₃ +* c₄,(c₇ + c₉)) +* c₄,(c₇ + c₉)))*>)))) by FUNCT_4:def 1;
then E87: dom (c₁₃ . ((c₇ + c₉) + 1)) = (dom (c₁₃ . (c₇ + c₉))) \/ {((c₃ +* c₄,(c₇ + c₉)) +* c₄,((c₇ + c₉) + 1))} by FUNCOP_1:19;
c₇ <= c₇ + c₉ by NAT_1:29;
then E88: c₇ <> (c₇ + c₉) + 1 by NAT_1:38;
( (c₃ +* c₄,c₇) . c₄ = c₇ & ((c₃ +* c₄,(c₇ + c₉)) +* c₄,((c₇ + c₉) + 1)) . c₄ = (c₇ + c₉) + 1 ) by E70, E83, FUNCT_7:33;
then not c₃ +* c₄,c₇ in {((c₃ +* c₄,(c₇ + c₉)) +* c₄,((c₇ + c₉) + 1))} by E88, TARSKI:def 1;
hence not c₃ +* c₄,c₇ in dom (c₆ . (c₃ +* c₄,(c₇ + (c₉ + 1)))) by E85, E86, E87, XBOOLE_0:def 2;

end;

hence not c₃ +* c₄,c₇ in dom (c₆ . (c₃ +* c₄,(c₇ + (c₉ + 1)))) by E78, E85, E86;

end;

thus for b₁ being Nat holds S₂[b₁] from NAT_1:sch 1(E72, E73);

end;

Lemma70: for b₁, b₂ being Nat
for b₃, b₄ being non empty to-naturals from-natural-fseqs homogeneous Function
for b₅ being Element of ((arity b₃) + 1) -tuples_on NAT st b₁ in dom b₅ holds
( ( b₅ +* b₁,0 in dom (primrec b₃,b₄,b₁) implies Del b₅,b₁ in dom b₃ ) & ( Del b₅,b₁ in dom b₃ implies b₅ +* b₁,0 in dom (primrec b₃,b₄,b₁) ) & ( b₅ +* b₁,0 in dom (primrec b₃,b₄,b₁) implies (primrec b₃,b₄,b₁) . (b₅ +* b₁,0) = b₃ . (Del b₅,b₁) ) & ( b₅ +* b₁,(b₂ + 1) in dom (primrec b₃,b₄,b₁) implies ( b₅ +* b₁,b₂ in dom (primrec b₃,b₄,b₁) & (b₅ +* b₁,b₂) ^ <*((primrec b₃,b₄,b₁) . (b₅ +* b₁,b₂))*> in dom b₄ ) ) & ( b₅ +* b₁,b₂ in dom (primrec b₃,b₄,b₁) & (b₅ +* b₁,b₂) ^ <*((primrec b₃,b₄,b₁) . (b₅ +* b₁,b₂))*> in dom b₄ implies b₅ +* b₁,(b₂ + 1) in dom (primrec b₃,b₄,b₁) ) & ( b₅ +* b₁,(b₂ + 1) in dom (primrec b₃,b₄,b₁) implies (primrec b₃,b₄,b₁) . (b₅ +* b₁,(b₂ + 1)) = b₄ . ((b₅ +* b₁,b₂) ^ <*((primrec b₃,b₄,b₁) . (b₅ +* b₁,b₂))*>) ) )

proof end;

theorem Th62: :: COMPUT_1:62

for b₁ being Nat
for b₂, b₃ being non empty to-naturals from-natural-fseqs homogeneous Function
for b₄ being Element of ((arity b₂) + 1) -tuples_on NAT st b₁ in dom b₄ holds
( b₄ +* b₁,0 in dom (primrec b₂,b₃,b₁) iff Del b₄,b₁ in dom b₂ ) by Lemma70;

theorem Th63: :: COMPUT_1:63

for b₁ being Nat
for b₂, b₃ being non empty to-naturals from-natural-fseqs homogeneous Function
for b₄ being Element of ((arity b₂) + 1) -tuples_on NAT st b₁ in dom b₄ & b₄ +* b₁,0 in dom (primrec b₂,b₃,b₁) holds
(primrec b₂,b₃,b₁) . (b₄ +* b₁,0) = b₂ . (Del b₄,b₁) by Lemma70;

theorem Th64: :: COMPUT_1:64

for b₁ being Nat
for b₂, b₃ being non empty to-naturals from-natural-fseqs homogeneous Function
for b₄ being Element of ((arity b₂) + 1) -tuples_on NAT st b₁ in dom b₄ & b₂ is len-total holds
(primrec b₂,b₃,b₁) . (b₄ +* b₁,0) = b₂ . (Del b₄,b₁)

proof end;

theorem Th65: :: COMPUT_1:65

for b₁, b₂ being Nat
for b₃, b₄ being non empty to-naturals from-natural-fseqs homogeneous Function
for b₅ being Element of ((arity b₃) + 1) -tuples_on NAT st b₁ in dom b₅ holds
( b₅ +* b₁,(b₂ + 1) in dom (primrec b₃,b₄,b₁) iff ( b₅ +* b₁,b₂ in dom (primrec b₃,b₄,b₁) & (b₅ +* b₁,b₂) ^ <*((primrec b₃,b₄,b₁) . (b₅ +* b₁,b₂))*> in dom b₄ ) ) by Lemma70;

theorem Th66: :: COMPUT_1:66

for b₁, b₂ being Nat
for b₃, b₄ being non empty to-naturals from-natural-fseqs homogeneous Function
for b₅ being Element of ((arity b₃) + 1) -tuples_on NAT st b₁ in dom b₅ & b₅ +* b₁,(b₂ + 1) in dom (primrec b₃,b₄,b₁) holds
(primrec b₃,b₄,b₁) . (b₅ +* b₁,(b₂ + 1)) = b₄ . ((b₅ +* b₁,b₂) ^ <*((primrec b₃,b₄,b₁) . (b₅ +* b₁,b₂))*>) by Lemma70;

theorem Th67: :: COMPUT_1:67

for b₁, b₂ being Nat
for b₃, b₄ being non empty to-naturals from-natural-fseqs homogeneous Function
for b₅ being Element of ((arity b₃) + 1) -tuples_on NAT st b₃ is len-total & b₄ is len-total & (arity b₃) + 2 = arity b₄ & 1 <= b₁ & b₁ <= 1 + (arity b₃) holds
(primrec b₃,b₄,b₁) . (b₅ +* b₁,(b₂ + 1)) = b₄ . ((b₅ +* b₁,b₂) ^ <*((primrec b₃,b₄,b₁) . (b₅ +* b₁,b₂))*>)

proof end;

theorem Th68: :: COMPUT_1:68

for b₁ being Nat
for b₂, b₃ being non empty to-naturals from-natural-fseqs homogeneous Function st (arity b₂) + 2 = arity b₃ & 1 <= b₁ & b₁ <= (arity b₂) + 1 holds
primrec b₂,b₃,b₁ is_primitive-recursively_expressed_by b₂,b₃,b₁

proof end;

theorem Th69: :: COMPUT_1:69

for b₁ being Nat
for b₂, b₃ being non empty to-naturals from-natural-fseqs homogeneous Function st 1 <= b₁ & b₁ <= (arity b₂) + 1 holds
for b₄ being Element of HFuncs NAT st b₄ is_primitive-recursively_expressed_by b₂,b₃,b₁ holds
b₄ = primrec b₂,b₃,b₁

proof end;

definition

let c₁ be set ;
attr a₁ is composition_closed means :Def15: :: COMPUT_1:def 15
for b₁ being Element of HFuncs NAT
for b₂ being with_the_same_arity FinSequence of HFuncs NAT st b₁ in a₁ & arity b₁ = len b₂ & rng b₂ c= a₁ holds
b₁ * <:b₂:> in a₁;
attr a₁ is primitive-recursion_closed means :Def16: :: COMPUT_1:def 16
for b₁, b₂, b₃ being Element of HFuncs NAT
for b₄ being Nat st b₁ is_primitive-recursively_expressed_by b₂,b₃,b₄ & b₂ in a₁ & b₃ in a₁ holds
b₁ in a₁;

end;

:: deftheorem Def15 defines composition_closed COMPUT_1:def 15 :

:: deftheorem Def16 defines primitive-recursion_closed COMPUT_1:def 16 :

definition

let c₁ be set ;
attr a₁ is primitive-recursively_closed means :Def17: :: COMPUT_1:def 17
( 0 const 0 in a₁ & 1 succ 1 in a₁ & ( for b₁, b₂ being Nat st 1 <= b₂ & b₂ <= b₁ holds
b₁ proj b₂ in a₁ ) & a₁ is composition_closed & a₁ is primitive-recursion_closed );

end;

:: deftheorem Def17 defines primitive-recursively_closed COMPUT_1:def 17 :

theorem Th70: :: COMPUT_1:70

HFuncs NAT is primitive-recursively_closed

proof end;

registration

cluster non empty primitive-recursively_closed Element of bool (HFuncs NAT );
existence

proof end;

end;

Lemma78: for b₁ being non empty set
for b₂, b₃ being Nat st 1 <= b₃ & b₃ <= b₂ holds
for b₄ being Element of b₁
for b₅ being Element of b₂ -tuples_on b₁ holds b₅ +* b₃,b₄ in b₂ -tuples_on b₁
;

theorem Th71: :: COMPUT_1:71

for b₁ being Nat
for b₂, b₃ being to-naturals from-natural-fseqs homogeneous Function
for b₄ being Element of HFuncs NAT st b₂ = {} & b₄ is_primitive-recursively_expressed_by b₂,b₃,b₁ holds
b₄ = {}

proof end;

theorem Th72: :: COMPUT_1:72

for b₁ being Element of HFuncs NAT
for b₂, b₃ being quasi_total Element of HFuncs NAT
for b₄ being Nat st b₁ is_primitive-recursively_expressed_by b₂,b₃,b₄ holds
( b₁ is quasi_total & ( not b₂ is empty implies not b₁ is empty ) )

proof end;

theorem Th73: :: COMPUT_1:73

for b₁, b₂ being Nat
for b₃ being non empty primitive-recursively_closed Subset of (HFuncs NAT ) holds b₁ const b₂ in b₃

proof end;

theorem Th74: :: COMPUT_1:74

for b₁, b₂ being Nat
for b₃ being non empty primitive-recursively_closed Subset of (HFuncs NAT ) st 1 <= b₁ & b₁ <= b₂ holds
b₂ succ b₁ in b₃

proof end;

theorem Th75: :: COMPUT_1:75

for b₁ being non empty primitive-recursively_closed Subset of (HFuncs NAT ) holds {} in b₁

proof end;

theorem Th76: :: COMPUT_1:76

for b₁ being non empty primitive-recursively_closed Subset of (HFuncs NAT )
for b₂ being Element of b₁
for b₃ being with_the_same_arity FinSequence of b₁ st arity b₂ = len b₃ holds
b₂ * <:b₃:> in b₁

proof end;

theorem Th77: :: COMPUT_1:77

for b₁ being non empty primitive-recursively_closed Subset of (HFuncs NAT )
for b₂, b₃ being Element of b₁ st (arity b₂) + 2 = arity b₃ holds
for b₄ being Nat st 1 <= b₄ & b₄ <= (arity b₂) + 1 holds
primrec b₂,b₃,b₄ in b₁

proof end;

definition

func PrimRec -> Subset of (HFuncs NAT ) equals :: COMPUT_1:def 18
meet { b₁ where B is Subset of (HFuncs NAT ) : b₁ is primitive-recursively_closed } ;
coherence

proof end;

end;

:: deftheorem Def18 defines PrimRec COMPUT_1:def 18 :

theorem Th78: :: COMPUT_1:78

for b₁ being Subset of (HFuncs NAT ) st b₁ is primitive-recursively_closed holds
PrimRec c= b₁

proof end;

registration

cluster PrimRec -> non empty primitive-recursively_closed ;
coherence

proof end;

end;

registration

cluster -> homogeneous Element of PrimRec ;
coherence ;

end;

definition

let c₁ be set ;
attr a₁ is primitive-recursive means :Def19: :: COMPUT_1:def 19
a₁ in PrimRec ;

end;

:: deftheorem Def19 defines primitive-recursive COMPUT_1:def 19 :

registration

cluster primitive-recursive -> Relation-like Function-like set ;
coherence

proof end;

end;

registration

cluster primitive-recursive -> to-naturals from-natural-fseqs homogeneous set ;
coherence

proof end;

end;

registration

cluster -> Relation-like Function-like to-naturals from-natural-fseqs homogeneous primitive-recursive Element of PrimRec ;
coherence by Def19;

end;

registration

cluster to-naturals from-natural-fseqs homogeneous primitive-recursive set ;
existence

proof end;

cluster to-naturals from-natural-fseqs homogeneous primitive-recursive Element of HFuncs NAT ;
existence

proof end;

end;

definition

func initial-funcs -> Subset of (HFuncs NAT ) equals :: COMPUT_1:def 20
{(0 const 0),(1 succ 1)} \/ { (b₁ proj b₂) where B is Nat, B is Nat : ( 1 <= b₂ & b₂ <= b₁ ) } ;
coherence

proof end;

let c₁ be Subset of (HFuncs NAT );
func PR-closure c₁ -> Subset of (HFuncs NAT ) equals :: COMPUT_1:def 21
a₁ \/ { b₁ where B is Element of HFuncs NAT : ex b₁, b₂ being Element of HFuncs NAT ex b₃ being Nat st
( b₂ in a₁ & b₃ in a₁ & b₁ is_primitive-recursively_expressed_by b₂,b₃,b₄ ) } ;
coherence

proof end;

func composition-closure c₁ -> Subset of (HFuncs NAT ) equals :: COMPUT_1:def 22
a₁ \/ { (b₁ * <:b₂:>) where B is Element of HFuncs NAT , B is with_the_same_arity Element of (HFuncs NAT ) * : ( b₁ in a₁ & arity b₁ = len b₂ & rng b₂ c= a₁ ) } ;
coherence

proof end;

end;

:: deftheorem Def20 defines initial-funcs COMPUT_1:def 20 :

:: deftheorem Def21 defines PR-closure COMPUT_1:def 21 :

:: deftheorem Def22 defines composition-closure COMPUT_1:def 22 :

definition

func PrimRec-Approximation -> Function of NAT , bool (HFuncs NAT ) means :Def23: :: COMPUT_1:def 23
( a₁ . 0 = initial-funcs & ( for b₁ being Nat holds a₁ . (b₁ + 1) = (PR-closure (a₁ . b₁)) \/ (composition-closure (a₁ . b₁)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def23 defines PrimRec-Approximation COMPUT_1:def 23 :

theorem Th79: :: COMPUT_1:79

for b₁, b₂ being Nat st b₁ <= b₂ holds
PrimRec-Approximation . b₁ c= PrimRec-Approximation . b₂

proof end;

theorem Th80: :: COMPUT_1:80

Union PrimRec-Approximation is primitive-recursively_closed

proof end;

theorem Th81: :: COMPUT_1:81

PrimRec = Union PrimRec-Approximation

proof end;

theorem Th82: :: COMPUT_1:82

for b₁ being Nat
for b₂ being Element of HFuncs NAT st b₂ in PrimRec-Approximation . b₁ holds
b₂ is quasi_total

proof end;

registration

cluster -> Relation-like Function-like quasi_total to-naturals from-natural-fseqs homogeneous primitive-recursive Element of PrimRec ;
coherence

proof end;

end;

registration

cluster primitive-recursive -> quasi_total homogeneous Element of HFuncs NAT ;
coherence

proof end;

end;

registration

cluster from-natural-fseqs primitive-recursive -> from-natural-fseqs len-total set ;
coherence

proof end;

cluster non empty quasi_total to-naturals from-natural-fseqs len-total homogeneous primitive-recursive Element of PrimRec ;
existence

proof end;

end;

definition

let c₁ be homogeneous Relation;
attr a₁ is nullary means :Def24: :: COMPUT_1:def 24
arity a₁ = 0;
attr a₁ is unary means :Def25: :: COMPUT_1:def 25
arity a₁ = 1;
attr a₁ is binary means :Def26: :: COMPUT_1:def 26
arity a₁ = 2;
attr a₁ is 3-ary means :Def27: :: COMPUT_1:def 27
arity a₁ = 3;

end;

:: deftheorem Def24 defines nullary COMPUT_1:def 24 :

:: deftheorem Def25 defines unary COMPUT_1:def 25 :

:: deftheorem Def26 defines binary COMPUT_1:def 26 :

:: deftheorem Def27 defines 3-ary COMPUT_1:def 27 :

registration

cluster homogeneous unary -> non empty homogeneous set ;
coherence

proof end;

cluster homogeneous binary -> non empty homogeneous set ;
coherence

proof end;

cluster homogeneous 3-ary -> non empty homogeneous set ;
coherence

proof end;

end;

registration

cluster 1 proj 1 -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive ;
coherence

proof end;

cluster 2 proj 1 -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive ;
coherence

proof end;

cluster 2 proj 2 -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive ;
coherence

proof end;

cluster 1 succ 1 -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive ;
coherence

proof end;

cluster 3 succ 3 -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive ;
coherence

proof end;

let c₁ be Nat;
cluster 0 const a₁ -> non empty to-naturals from-natural-fseqs len-total homogeneous nullary ;
coherence

proof end;

cluster 1 const a₁ -> non empty to-naturals from-natural-fseqs len-total homogeneous unary ;
coherence

proof end;

cluster 2 const a₁ -> non empty to-naturals from-natural-fseqs len-total homogeneous binary ;
coherence

proof end;

cluster 3 const a₁ -> non empty to-naturals from-natural-fseqs len-total homogeneous 3-ary ;
coherence

proof end;

cluster 1 proj a₁ -> non empty to-naturals from-natural-fseqs len-total homogeneous unary ;
coherence

proof end;

cluster 2 proj a₁ -> non empty to-naturals from-natural-fseqs len-total homogeneous binary ;
coherence

proof end;

cluster 3 proj a₁ -> non empty to-naturals from-natural-fseqs len-total homogeneous 3-ary ;
coherence

proof end;

cluster 1 succ a₁ -> non empty to-naturals from-natural-fseqs len-total homogeneous unary ;
coherence

proof end;

cluster 2 succ a₁ -> non empty to-naturals from-natural-fseqs len-total homogeneous binary ;
coherence

proof end;

cluster 3 succ a₁ -> non empty to-naturals from-natural-fseqs len-total homogeneous 3-ary ;
coherence

proof end;

let c₂ be Nat;
cluster a₁ const a₂ -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive ;
coherence

proof end;

end;

registration

cluster non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive nullary set ;
existence by Def17;
cluster non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive unary set ;
existence by Def17;
cluster non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive binary set ;
existence

proof end;

cluster non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive 3-ary set ;
existence

proof end;

end;

registration

cluster non empty to-naturals from-natural-fseqs len-total homogeneous nullary set ;
existence

proof end;

cluster non empty to-naturals from-natural-fseqs len-total homogeneous unary set ;
existence

proof end;

cluster non empty to-naturals from-natural-fseqs len-total homogeneous binary set ;
existence

proof end;

cluster non empty to-naturals from-natural-fseqs len-total homogeneous 3-ary set ;
existence

proof end;

end;

registration

let c₁ be non empty primitive-recursive nullary Function;
let c₂ be primitive-recursive binary Function;
cluster primrec a₁,a₂,1 -> non empty quasi_total to-naturals from-natural-fseqs len-total homogeneous primitive-recursive unary ;
coherence

proof end;

end;

registration

let c₁ be primitive-recursive unary Function;
let c₂ be primitive-recursive 3-ary Function;
cluster primrec a₁,a₂,1 -> non empty quasi_total to-naturals from-natural-fseqs len-total homogeneous primitive-recursive binary ;
coherence

proof end;

cluster primrec a₁,a₂,2 -> non empty quasi_total to-naturals from-natural-fseqs len-total homogeneous primitive-recursive binary ;
coherence

proof end;

end;

theorem Th83: :: COMPUT_1:83

for b₁ being Nat
for b₂ being to-naturals from-natural-fseqs len-total homogeneous unary Function
for b₃ being non empty to-naturals from-natural-fseqs homogeneous Function holds (primrec b₂,b₃,2) . <*b₁,0*> = b₂ . <*b₁*>

proof end;

theorem Th84: :: COMPUT_1:84

for b₁, b₂ being non empty to-naturals from-natural-fseqs homogeneous Function st b₁ is len-total & arity b₁ = 0 holds
(primrec b₁,b₂,1) . <*0*> = b₁ . {}

proof end;

theorem Th85: :: COMPUT_1:85

for b₁, b₂ being Nat
for b₃ being to-naturals from-natural-fseqs len-total homogeneous unary Function
for b₄ being to-naturals from-natural-fseqs len-total homogeneous 3-ary Function holds (primrec b₃,b₄,2) . <*b₁,(b₂ + 1)*> = b₄ . <*b₁,b₂,((primrec b₃,b₄,2) . <*b₁,b₂*>)*>

proof end;

theorem Th86: :: COMPUT_1:86

for b₁ being Nat
for b₂, b₃ being non empty to-naturals from-natural-fseqs homogeneous Function st b₂ is len-total & b₃ is len-total & arity b₂ = 0 & arity b₃ = 2 holds
(primrec b₂,b₃,1) . <*(b₁ + 1)*> = b₃ . <*b₁,((primrec b₂,b₃,1) . <*b₁*>)*>

proof end;

E101: now

let c₁ be non empty quasi_total homogeneous PartFunc of NAT * , NAT ;
assume E102: arity c₁ = 2 ;
thus E103: dom <:<*(3 proj 1),(3 proj 3)*>:> = (dom (3 proj 1)) /\ (dom (3 proj 3)) by FUNCT_6:62;
hence E104: dom <:<*(3 proj 1),(3 proj 3)*>:> = (3 -tuples_on NAT ) /\ (dom (3 proj 3)) by Th40
.= (3 -tuples_on NAT ) /\ (3 -tuples_on NAT ) by Th40
.= 3 -tuples_on NAT ;

reconsider c₂ = <*0,0,0*> as FinSequence of NAT ;
len c₂ = 3 by FINSEQ_1:62;
then E105: c₂ is Element of 3 -tuples_on NAT by FINSEQ_2:110;
E106: dom c₁ = 2 -tuples_on NAT by E102, Th25;
set c₃ = c₁ * <:<*(3 proj 1),(3 proj 3)*>:>;

now

let c₄ be set ;
set c₅ = <*(3 proj 1),(3 proj 3)*>;
set c₆ = <:<*(3 proj 1),(3 proj 3)*>:>;
E107: product (rngs <*(3 proj 1),(3 proj 3)*>) = product <*(rng (3 proj 1)),(rng (3 proj 3))*> by FUNCT_6:34
.= product <*NAT ,(rng (3 proj 3))*> by Th40
.= product <*NAT ,NAT *> by Th40
.= 2 -tuples_on NAT by FUNCT_6:6 ;

hereby

assume E108: c₄ in rng <:<*(3 proj 1),(3 proj 3)*>:> ;
rng <:<*(3 proj 1),(3 proj 3)*>:> c= product (rngs <*(3 proj 1),(3 proj 3)*>) by FUNCT_6:49;
hence c₄ in dom c₁ by E106, E107, E108;

end;

assume c₄ in dom c₁ ;
then consider c₇, c₈ being Nat such that
E108: c₄ = <*c₇,c₈*> by E106, FINSEQ_2:120;
reconsider c₉ = <*c₇,0,c₈*> as Element of 3 -tuples_on NAT by FINSEQ_2:124;
<:<*(3 proj 1),(3 proj 3)*>:> . c₉ = <*((3 proj 1) . c₉),((3 proj 3) . c₉)*> by E103, E104, FUNCT_6:62
.= <*(c₉ . 1),((3 proj 3) . c₉)*> by Th42
.= <*(c₉ . 1),(c₉ . 3)*> by Th42
.= <*c₇,(c₉ . 3)*> by FINSEQ_1:62
.= c₄ by E108, FINSEQ_1:62 ;
hence c₄ in rng <:<*(3 proj 1),(3 proj 3)*>:> by E104, FUNCT_1:def 5;

end;

then E107: rng <:<*(3 proj 1),(3 proj 3)*>:> = dom c₁ by TARSKI:2;
hence E108: dom (c₁ * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT by E104, RELAT_1:46;
then E109: dom (c₁ * <:<*(3 proj 1),(3 proj 3)*>:>) c= NAT * by MSUALG_1:12;
rng c₁ c= NAT by RELSET_1:12;
then rng (c₁ * <:<*(3 proj 1),(3 proj 3)*>:>) c= NAT by E107, RELAT_1:47;
then reconsider c₄ = c₁ * <:<*(3 proj 1),(3 proj 3)*>:> as PartFunc of NAT * , NAT by E109, RELSET_1:11;

now

let c₅, c₆ be FinSequence;
assume ( c₅ in dom c₄ & c₆ in dom c₄ ) ;
then ( 3 = len c₅ & 3 = len c₆ ) by E108, FINSEQ_2:109;
hence len c₅ = len c₆ ;

end;

then reconsider c₅ = c₄ as homogeneous PartFunc of NAT * , NAT by Def4;
take c₆ = c₅;
thus c₆ = c₁ * <:<*(3 proj 1),(3 proj 3)*>:> ;
c₆ is Element of PFuncs (NAT * ),NAT by PARTFUN1:119;
then c₆ in HFuncs NAT ;
hence c₆ is Element of HFuncs NAT ;
for b₁ being FinSequence st b₁ in dom c₆ holds
3 = len b₁ by E108, FINSEQ_2:109;
hence arity c₆ = 3 by E105, E108, Def5;
hence ( c₆ is quasi_total & not c₆ is empty ) by E108, Th25;

end;

definition

let c₁ be Function;
func (1,2)->(1,?,2) c₁ -> Function equals :: COMPUT_1:def 28
a₁ * <:<*(3 proj 1),(3 proj 3)*>:>;
coherence ;

end;

:: deftheorem Def28 defines (1,2)->(1,?,2) COMPUT_1:def 28 :

registration

let c₁ be to-naturals from-natural-fseqs Function;
cluster (1,2)->(1,?,2) a₁ -> to-naturals from-natural-fseqs ;
coherence

proof end;

end;

registration

let c₁ be homogeneous Function;
cluster (1,2)->(1,?,2) a₁ -> homogeneous ;
coherence

proof end;

end;

registration

let c₁ be to-naturals from-natural-fseqs len-total homogeneous binary Function;
cluster (1,2)->(1,?,2) a₁ -> non empty to-naturals from-natural-fseqs len-total homogeneous 3-ary ;
coherence

proof end;

end;

theorem Th87: :: COMPUT_1:87

for b₁, b₂, b₃ being Nat
for b₄ being to-naturals from-natural-fseqs len-total homogeneous binary Function holds ((1,2)->(1,?,2) b₄) . <*b₁,b₂,b₃*> = b₄ . <*b₁,b₃*>

proof end;

theorem Th88: :: COMPUT_1:88

for b₁ being primitive-recursive binary Function holds (1,2)->(1,?,2) b₁ in PrimRec

proof end;

registration

let c₁ be homogeneous primitive-recursive binary Function;
cluster (1,2)->(1,?,2) a₁ -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive 3-ary ;
coherence

proof end;

end;

definition

func [+] -> primitive-recursive binary Function equals :: COMPUT_1:def 29
primrec (1 proj 1),(3 succ 3),2;
coherence ;

end;

:: deftheorem Def29 defines [+] COMPUT_1:def 29 :

theorem Th89: :: COMPUT_1:89

for b₁, b₂ being Nat holds [+] . <*b₁,b₂*> = b₁ + b₂

proof end;

definition

func [*] -> primitive-recursive binary Function equals :: COMPUT_1:def 30
primrec (1 const 0),((1,2)->(1,?,2) [+] ),2;
coherence ;

end;

:: deftheorem Def30 defines [*] COMPUT_1:def 30 :

theorem Th90: :: COMPUT_1:90

for b₁, b₂ being Nat holds [*] . <*b₁,b₂*> = b₁ * b₂

proof end;

registration

let c₁, c₂ be homogeneous primitive-recursive binary Function;
cluster <*a₁,a₂*> -> with_the_same_arity ;
coherence

proof end;

end;

registration

let c₁, c₂, c₃ be primitive-recursive binary Function;
cluster <:<*a₂,a₃*>:> * a₁ -> to-naturals from-natural-fseqs len-total homogeneous primitive-recursive ;
coherence

proof end;

end;

registration

let c₁, c₂, c₃ be primitive-recursive binary Function;
cluster <:<*a₂,a₃*>:> * a₁ -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive binary ;
coherence

proof end;

end;

registration

let c₁ be primitive-recursive unary Function;
let c₂ be primitive-recursive Function;
cluster <:<*a₂*>:> * a₁ -> to-naturals from-natural-fseqs len-total homogeneous primitive-recursive ;
coherence

proof end;

end;

registration

let c₁ be primitive-recursive unary Function;
let c₂ be primitive-recursive binary Function;
cluster <:<*a₂*>:> * a₁ -> non empty to-naturals from-natural-fseqs len-total homogeneous primitive-recursive binary ;
coherence

proof end;

end;

definition

func [!] -> primitive-recursive unary Function equals :: COMPUT_1:def 31
primrec (0 const 1),([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>),1;
coherence ;

end;

:: deftheorem Def31 defines [!] COMPUT_1:def 31 :

scheme :: COMPUT_1:sch 1
s1{ F₁() -> to-naturals from-natural-fseqs len-total homogeneous unary Function, F₂() -> to-naturals from-natural-fseqs len-total homogeneous binary Function, F₃( set ) -> Nat, F₄( set , set ) -> Nat } :

for b₁, b₂ being Nat holds (F₁() * <:<*F₂()*>:>) . <*b₁,b₂*> = F₃(F₄(b₁,b₂))

provided

E106: for b₁ being Nat holds F₁() . <*b₁*> = F₃(b₁) and
E107: for b₁, b₂ being Nat holds F₂() . <*b₁,b₂*> = F₄(b₁,b₂)

proof end;

scheme :: COMPUT_1:sch 2
s2{ F₁() -> to-naturals from-natural-fseqs len-total homogeneous binary Function, F₂() -> to-naturals from-natural-fseqs len-total homogeneous binary Function, F₃() -> to-naturals from-natural-fseqs len-total homogeneous binary Function, F₄( set , set ) -> Nat, F₅( set , set ) -> Nat, F₆( set , set ) -> Nat } :

for b₁, b₂ being Nat holds (F₁() * <:<*F₂(),F₃()*>:>) . <*b₁,b₂*> = F₄(F₅(b₁,b₂),F₆(b₁,b₂))

provided

E106: for b₁, b₂ being Nat holds F₁() . <*b₁,b₂*> = F₄(b₁,b₂) and
E107: for b₁, b₂ being Nat holds F₂() . <*b₁,b₂*> = F₅(b₁,b₂) and
E108: for b₁, b₂ being Nat holds F₃() . <*b₁,b₂*> = F₆(b₁,b₂)

proof end;

theorem Th91: :: COMPUT_1:91

for b₁ being Nat holds [!] . <*b₁*> = b₁ !

proof end;

definition

func [^] -> primitive-recursive binary Function equals :: COMPUT_1:def 32
primrec (1 const 1),((1,2)->(1,?,2) [*] ),2;
coherence ;

end;

:: deftheorem Def32 defines [^] COMPUT_1:def 32 :

theorem Th92: :: COMPUT_1:92

for b₁, b₂ being Nat holds [^] . <*b₁,b₂*> = b₁ |^ b₂

proof end;

definition

func [pred] -> primitive-recursive unary Function equals :: COMPUT_1:def 33
primrec (0 const 0),(2 proj 1),1;
coherence ;

end;

:: deftheorem Def33 defines [pred] COMPUT_1:def 33 :

theorem Th93: :: COMPUT_1:93

for b₁ being Nat holds
( [pred] . <*0*> = 0 & [pred] . <*(b₁ + 1)*> = b₁ )

proof end;

definition

func [-] -> primitive-recursive binary Function equals :: COMPUT_1:def 34
primrec (1 proj 1),((1,2)->(1,?,2) ([pred] * <:<*(2 proj 2)*>:>)),2;
coherence ;

end;

:: deftheorem Def34 defines [-] COMPUT_1:def 34 :

theorem Th94: :: COMPUT_1:94

for b₁, b₂ being Nat holds [-] . <*b₁,b₂*> = b₁ -' b₂

proof end;