set I = [0 ,{} ,{} ];
let W be Instruction of SCM+FSA ; :: thesis: ( W is halting implies W = [0 ,{} ,{} ] )
assume A1: W is halting ; :: thesis: W = [0 ,{} ,{} ]
assume A2: [0 ,{} ,{} ] <> W ; :: thesis: contradiction
per cases ( W = [0 ,{} ,{} ] or ex a, b being Int-Location st W = a := b or ex a, b being Int-Location st W = AddTo a,b or ex a, b being Int-Location st W = SubFrom a,b or ex a, b being Int-Location st W = MultBy a,b or ex a, b being Int-Location st W = Divide a,b or ex la being Element of NAT st W = goto la or ex lb being Element of NAT ex da being Int-Location st W = da =0_goto lb or ex lb being Element of NAT ex da being Int-Location st W = da >0_goto lb or ex b, a being Int-Location ex fa being FinSeq-Location st W = a := fa,b or ex a, b being Int-Location ex fa being FinSeq-Location st W = fa,a := b or ex a being Int-Location ex f being FinSeq-Location st W = a :=len f or ex a being Int-Location ex f being FinSeq-Location st W = f :=<0,...,0> a ) by Th120;
suppose W = [0 ,{} ,{} ] ; :: thesis: contradiction
hence contradiction by A2; :: thesis: verum
end;
suppose ex a, b being Int-Location st W = a := b ; :: thesis: contradiction
hence contradiction by A1, Th105; :: thesis: verum
end;
suppose ex a, b being Int-Location st W = AddTo a,b ; :: thesis: contradiction
hence contradiction by A1, Th106; :: thesis: verum
end;
suppose ex a, b being Int-Location st W = SubFrom a,b ; :: thesis: contradiction
hence contradiction by A1, Th107; :: thesis: verum
end;
suppose ex a, b being Int-Location st W = MultBy a,b ; :: thesis: contradiction
hence contradiction by A1, Th108; :: thesis: verum
end;
suppose ex a, b being Int-Location st W = Divide a,b ; :: thesis: contradiction
hence contradiction by A1, Th109; :: thesis: verum
end;
suppose ex la being Element of NAT st W = goto la ; :: thesis: contradiction
hence contradiction by A1, Th110; :: thesis: verum
end;
suppose ex lb being Element of NAT ex da being Int-Location st W = da =0_goto lb ; :: thesis: contradiction
hence contradiction by A1, Th111; :: thesis: verum
end;
suppose ex lb being Element of NAT ex da being Int-Location st W = da >0_goto lb ; :: thesis: contradiction
hence contradiction by A1, Th112; :: thesis: verum
end;
suppose ex b, a being Int-Location ex fa being FinSeq-Location st W = a := fa,b ; :: thesis: contradiction
hence contradiction by A1, Th113; :: thesis: verum
end;
suppose ex a, b being Int-Location ex fa being FinSeq-Location st W = fa,a := b ; :: thesis: contradiction
hence contradiction by A1, Th114; :: thesis: verum
end;
suppose ex a being Int-Location ex f being FinSeq-Location st W = a :=len f ; :: thesis: contradiction
hence contradiction by A1, Th115; :: thesis: verum
end;
suppose ex a being Int-Location ex f being FinSeq-Location st W = f :=<0,...,0> a ; :: thesis: contradiction
hence contradiction by A1, Th116; :: thesis: verum
end;
end;