let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of IL,N
for p being pre-program of S
for F being PartFunc of (FinPartSt S),(FinPartSt S) st F = {} .--> (Result p) holds
p is Program of F
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of IL,N
for p being pre-program of S
for F being PartFunc of (FinPartSt S),(FinPartSt S) st F = {} .--> (Result p) holds
p is Program of F
let S be non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of IL,N; :: thesis: for p being pre-program of S
for F being PartFunc of (FinPartSt S),(FinPartSt S) st F = {} .--> (Result p) holds
p is Program of F
let p be pre-program of S; :: thesis: for F being PartFunc of (FinPartSt S),(FinPartSt S) st F = {} .--> (Result p) holds
p is Program of F
let F be PartFunc of (FinPartSt S),(FinPartSt S); :: thesis: ( F = {} .--> (Result p) implies p is Program of F )
assume A1: F = {} .--> (Result p) ; :: thesis: p is Program of F
hence F is computable by Th73; :: according to AMI_1:def 31 :: thesis: p computes F
thus p computes F by A1, Th69; :: thesis: verum