let k be Nat; :: thesis: for S being non empty standard-ins homogeneous J/A-independent with_halt set

for I being Element of S st IncAddr (I,k) = halt S holds

I = halt S

let S be non empty standard-ins homogeneous J/A-independent with_halt set ; :: thesis: for I being Element of S st IncAddr (I,k) = halt S holds

I = halt S

let I be Element of S; :: thesis: ( IncAddr (I,k) = halt S implies I = halt S )

assume IncAddr (I,k) = halt S ; :: thesis: I = halt S

then IncAddr (I,k) = IncAddr ((halt S),k) by Th3;

hence I = halt S by Th5; :: thesis: verum

for I being Element of S st IncAddr (I,k) = halt S holds

I = halt S

let S be non empty standard-ins homogeneous J/A-independent with_halt set ; :: thesis: for I being Element of S st IncAddr (I,k) = halt S holds

I = halt S

let I be Element of S; :: thesis: ( IncAddr (I,k) = halt S implies I = halt S )

assume IncAddr (I,k) = halt S ; :: thesis: I = halt S

then IncAddr (I,k) = IncAddr ((halt S),k) by Th3;

hence I = halt S by Th5; :: thesis: verum